Uniform bounds for the collar data extracted from CKS tensor fields

Let $K$ be a compact set of matrix three-jets with invertible value matrices and let $B\ge 0$. There are $R_0\ge 1$ and $C\ge 0$ such that, for all tensor fields $f$ in logarithmic radial coordinates and points $x$ with $e^{x_0}\ge R_0$, if $f$ is regular at $x$, its logarithmic metric is positive definite near $x$, the three-jet of the angular metric $\sigma$ at $x$ lies in $K$, and the component bounds LogComponentBound B hold at $x$, then the collar data sourceCollarData f satisfy BoundedAt C at $x$. The log component bounds have the CKS decay weights, for example the error of the angular metric is $O(e^{-2x_0})$, the shift is $O(e^{-3x_0})$ and the radial error is $O(e^{-6x_0})$.

Formal statement. In the scope of the preamble:

theorem cks_sourceCollarData_bounded {K : Set MatrixThreeJet} (hK : IsCompact K)
    (hreg : ∀ q ∈ K, determinant (fun i k => (q i k).1.1) ≠ 0)
    {B : ℝ} (hB : 0 ≤ B) :
    ∃ R₀ : ℝ, 1 ≤ R₀ ∧ ∃ C : ℝ, 0 ≤ C ∧ ∀ f : TensorFields, ∀ x : Point,
      R₀ ≤ Real.exp (x 0) → f.RegularAt x →
      (∀ᶠ y in 𝓝 x, (logMetric f.base y).PosDef) → matrixThreeJets f.base.sigma x ∈ K →
      f.LogComponentBound B x → (sourceCollarData f).BoundedAt C x

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