RSCosmo004Cert
plain-language theorem explainer
Certificate structure bundling three structural facts for RS Cosmology Module 4 (the n_s = 1 - 2/45 prediction): domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the module's structural side uses the inhabited instance. Pure structure definition; no proof body.
Claim. A certificate of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
RS Cosmology Module 4 records the scalar spectral index prediction $n_s = 1 - 2/45 \approx 0.9556$ against Planck $0.9649$ (about $2.2\sigma$ tension). The module is marked OPEN on the observational comparison and STRUCTURAL THEOREM on the Lean side (zero sorry, zero axiom).
Domain cost is the local cost functional used in this module (via the Cost and Constants imports). The canonical threshold is the positive cutoff paired with that cost. Upstream, ObserverForcing proves that the cost of any recognition event is nonnegative, by reduction to nonnegativity of the J-cost on positive states. This certificate packages the three Prop-level facts the module needs as a single bundle.
proof idea
Pure structure definition with empty proof body. The three fields are proposition-valued requirements, not constructed data. Downstream, a concrete inhabitant is assembled by supplying the diagonal-vanishing lemma for domain cost, the nonnegativity lemma for positive arguments, and the positivity proof for the canonical threshold; Nonempty then follows by pairing that inhabitant.
why it matters
Supplies the type inhabited by the module's concrete certificate and by the Nonempty theorem that closes the structural side of Cosmology Module 4. Downstream uses wire the three field proofs into one bundle so later cosmology arguments can assume diagonal vanishing, cost nonnegativity, and a positive threshold together. The observational $n_s$ comparison remains OPEN; this declaration only locks the cost-geometry side. It sits on the same J-cost nonnegativity strand that feeds T5 (uniqueness of $J$) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.