curvature_bounded_at_R0
plain-language theorem explainer
The theorem establishes that the curvature scalar at the recognition origin R0 satisfies |R| ≤ 1 in RS-native units. Inflation modelers cite this bound when assembling the full InflationCert for phi-driven cosmology. The proof is a one-line simplification that unfolds the definition of ell0 as unity.
Claim. In RS-native units the curvature at the recognition origin obeys $|R| ≤ 1/ℓ₀² = 1$.
background
The Gravity.Inflation module formalizes RS inflationary predictions with the α-attractor parameter equal to φ² from cost-functional self-similarity. The fundamental length ℓ₀ is the voxel scale in native units, defined as 1 and derived upstream as c τ₀ where τ₀² = ℏG/(π c⁵). The doc-comment states the bound |R| ≤ 1/λ_rec² = 1 at the recognition event R0.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of ell0, which reduces directly to the equality 1/1² = 1.
why it matters
This result is collected inside inflation_cert, which bundles the α-attractor, spectral index, tensor-to-scalar ratio, and modulation frequency for the phi-inflation model. It supplies the curvature normalization at R0 consistent with the forcing chain (T5–T8) and the Recognition Composition Law. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.