cert
plain-language theorem explainer
Packages three elementary domain-cost facts into the RS Cosmology Module 4 certificate: diagonal vanishing, nonnegativity for positive arguments, and positivity of the canonical threshold. Cosmologists citing the structural side of the n_s = 1 - 2/45 claim use this bundle. The definition is a pure structure inhabitant wiring three sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $\tau$ obeys $\tau>0$.
background
Module RS_Cosmo_Module_004 is the structural layer for the scalar spectral index claim $n_s = 1 - 2/45 = 0.9556$, set against the Planck value $0.9649$ (about $2.2\sigma$ tension) and marked OPEN on the physics side. The module status is structural theorem: zero sorry, zero axiom.
The certificate type RSCosmo004Cert is a triple of propositions about a domain cost $C$ (built from the Recognition Science $J$-cost) and a canonical threshold $\tau$. The first field demands $C$ vanish on the diagonal away from zero; the second demands nonnegativity for positive mass and energy arguments; the third demands $\tau>0$. Upstream, the foundation lemma that every recognition-event cost is nonnegative (via $J\ge 0$ for positive state) supplies the cost-positivity pattern this module mirrors at the domain level.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional rewriting or case analysis occurs; the definition is pure packaging of already-proved facts.
why it matters
Gives a single named inhabitant that any later cosmology lemma can require instead of re-stating the three domain-cost axioms. In the Recognition framework this is the structural gate for Module 4: before one argues about the eight-tick octave, $\phi$-ladder rungs, or the forced $n_s = 1-2/45$ band, the cost geometry must be certified nonnegative, diagonal-zero, and threshold-positive. The physics comparison to Planck remains OPEN; this declaration only closes the Lean-side structural bundle. No downstream theorems currently depend on it, so it is the root certificate for the module rather than an intermediate step in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.