RSCosmo002Cert
plain-language theorem explainer
A certificate packing three structural facts for Cosmology Module 2: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cosmology and constants auditors cite it to discharge the module's structural obligations around the RS prediction for Λℓ_P². The structure itself is pure data; inhabitance is supplied by the sibling `cert` assembly.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(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 Module 2 targets the dimensionless product $\Lambda \ell_P^2$. Recognition Science predicts $8\varphi^5/45$, which lands in $(1.88,2.03)\times 10^{-122}$ against the Planck value $\approx 1.99\times 10^{-122}$. The module is marked structural (zero sorry, zero axiom).
The domain cost is the local cost functional on pairs of positive reals used in this cosmology layer; it is the specialization of the global $J$-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$) to the module's mass/energy-style arguments. The canonical threshold is the positive cutoff against which that cost is compared in the module's pass criteria.
Upstream, nonnegativity of recognition-event cost is already established in ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The certificate reuses that pattern at the domain-cost level.
proof idea
No proof body: this is a structure declaration, not a theorem. It packages three Prop-valued fields. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty witness built from that inhabitant.
why it matters
The certificate is the typed obligation bundle for RS Cosmology Module 2. Downstream, cert assembles a concrete inhabitant from the three sibling lemmas, and cert_inhabited records Nonempty of the structure, closing the module's structural theorem status.
In the broader framework this sits under the cosmology constants track: the forced golden ratio $\varphi$ (T6) and the $J$-cost uniqueness (T5) feed the numerical band $8\varphi^5/45$ for $\Lambda\ell_P^2$. The certificate does not itself compute that band; it guarantees the cost and threshold scaffolding the module uses when claiming RS_PASS against the Planck figure.
Parent consumers are only the local cert / cert_inhabited pair; external modules import the inhabited certificate rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.