The dominant energy condition for the bent outer data

Here $f_0$ is a smooth function on the unit sphere $S^2$, $m$ a real number, and $R$ the replacement radius. There is $R_0\ge 12$ such that, for all $R\ge R_0$ and chart points with $r\ge 3R$ and $\sin\theta\ne 0$, the outer metric jet and tensor jet built from the lapse with mass $F=$ outerMass f₀ m R and bending profile $v_R=$ bendingV R, with second tensor determined by the normal entry $v_R'+\beta_R/r^2$, the trace part $v_R/r$ and the corrected components of $a,b$, satisfy the local inequality DEC.

Formal statement. In the scope of the preamble:

theorem constructed_outer_DEC (f₀ : C(Sphere,ℝ)) (hf₀ : SmoothSphere f₀) (m : ℝ) :
    ∃ R₀ : ℝ, 12 ≤ R₀ ∧ ∀ R : ℝ, R₀ ≤ R → ∀ x : Point,
    3*R ≤ x 0 → Real.sin (x 1) ≠ 0 →
    DEC (metricJet (lapse (outerMass f₀ m R) (bendingV R)) x)
      (tensorJet (lapse (outerMass f₀ m R) (bendingV R)) (bendingV R)
        (radial (normalEntry (bendingV R) (bendingBeta R)))
        (correctedComponent (bendingV R) (outerA f₀ R))
        (correctedComponent (bendingV R) (outerPhi f₀ R)) x)

Formalization Note The statement is verbatim from lean/OAI/Geometry/Relativity/CKS/OuterRealization.lean, lines 11-45, 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.