RSCosmo001Cert
plain-language theorem explainer
A certificate packing three structural facts for Cosmology Module 1: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cosmology and constants auditors cite it as the typed interface that Module 1 must inhabit. It is a pure structure definition; inhabitance is discharged later by wiring the sibling lemmas.
Claim. A certificate for RS Cosmology Module 1 is a record of three properties: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Cosmology RS Module 1 targets the dark-energy density parameter via the closed form $\Omega_\Lambda = 11/16 - \alpha/\pi \approx 0.685$, matching Planck at $0.665\sigma$. The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom).
The domain cost is the local cost functional on pairs of positive reals used in this cosmology layer; its diagonal vanishing and nonnegativity mirror the global recognition cost $J$, which is nonnegative on recognition events (ObserverForcing: "The cost of any recognition event is non-negative"). The canonical threshold is the positive cutoff against which that cost is compared in the module's pass criterion.
This structure does not compute $\Omega_\Lambda$; it only packages the cost and threshold side-conditions that the module's certificate must satisfy.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive mass/energy arguments, positivity of the canonical threshold). Inhabitation is supplied by the sibling definition cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos fieldwise, and by cert_inhabited, which wraps that witness as Nonempty.
why it matters
Gives Cosmology Module 1 a single typed certificate rather than three free-floating lemmas. Downstream, cert builds a concrete inhabitant and cert_inhabited records that the type is nonempty, closing the structural obligation for the $\Omega_\Lambda = 11/16 - \alpha/\pi$ claim.
In the Recognition framework this sits under the cosmology domain that consumes the forced constants ($\alpha$ band, $J$-cost nonnegativity from the forcing chain). It does not itself derive $\Omega_\Lambda$ or the eight-tick/D=3 landmarks; it only certifies the cost-threshold interface those derivations rely on when the module is audited as RS_PASS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.