Constraint estimates for bounded raw null inputs

Let $K$ be a compact set of $2\times 2$ scalar jet matrices with invertible values, and let $B\in\mathbb R$, $A\ge 0$. There are $R_0\ge 1$ and $C,D\ge 0$ such that for every raw null input $p$ with metric jet in $K$ and $\|p\|\le B$, and $r\ge R_0$ with $z(p)=1/r$, weight $w=$ rwgt $\ge 0$ and $|p_i|\le Aw$ for $i\ne 0$, writing $Q,Q_0$ for coordinateQ of the deformed and original input, $Z,Z_0$ for coordinateZ, and $E,E_0$ for the corresponding coordinate energies:

The added quantity is controlled by the weight $w$ itself, so the estimate keeps its force where the activation weight is small.

Formal statement. In the scope of the preamble:

theorem bounded_raw_CQ {K : Set MatrixScalarJet} (hK : IsCompact K)
    (hreg : ∀ q ∈ K, determinant (fun i k => (q i k).1) ≠ 0) (B A : ℝ) (hA : 0 ≤ A) :
    ∃ R₀ : ℝ, 1 ≤ R₀ ∧ ∃ C D : ℝ, 0 ≤ C ∧ 0 ≤ D ∧
      ∀ p : RawNullInput, rmat p.1 0 ∈ K → ‖p‖ ≤ B →
      ∀ r : ℝ, R₀ ≤ r → rz p.1=1/r → 0 ≤ rwgt p.1 →
      (∀ i, i ≠ 0 → |p.1.1 i| ≤ A*rwgt p.1) →
      |coordinateQ (rawMomentumInput (rawOriginal p.1))| ≤ D/r^3 ∧
      |coordinateQ (rawMomentumInput p.1)-coordinateQ (rawMomentumInput (rawOriginal p.1))-
        2*rwgt p.1/r^2| ≤ C*rwgt p.1/r^3 ∧
      |(coordinateEnergy (rawNullMap p) r-coordinateEnergy (rawNullMap (rawNullOriginal p)) r)-
          (coordinateQ (rawMomentumInput p.1)-coordinateQ (rawMomentumInput (rawOriginal p.1)))-
        2*rwgt p.1/(r^3*Real.sqrt r)| ≤ C*rwgt p.1/r^4 ∧
      (∀ a, |coordinateZ (rawMomentumInput (rawOriginal p.1)) a| ≤ D/r^2) ∧
      (∀ a, |coordinateZ (rawMomentumInput p.1) a-
        coordinateZ (rawMomentumInput (rawOriginal p.1)) a| ≤ C*rwgt p.1/r^2)

Formalization Note The statement is verbatim from lean/OAI/Geometry/Relativity/CKS/CollarConstraintBounded.lean, lines 16-60, in OpenAI's openai/math at commit adc7f12 (Apache-2.0), formalizing part of the construction in the preprint Area-controlled end replacement and the Bondi–Penrose inequality in the CKS class (OpenAI, September 27, 2026). It is a supporting lemma for OAI.CKSSourceExterior.area_controlled_end_replacement. The definitions it mentions are those of Definitions.Def_CKSBondiPenrose and Definitions.Def_CKSEndReplacementSupport.