cert_inhabited
plain-language theorem explainer
The certificate bundle for RS Cosmology Module 2 is inhabited: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy, and the canonical threshold is positive. Cosmologists citing the structural Lambda ell_P^2 pass use this existence fact. Proof is a one-line term witness packaging the already-built cert.
Claim. There exists a certificate asserting: (i) the domain cost of any nonzero real $r$ against itself is zero; (ii) for all positive $m,e$, the domain cost of $m$ against $e$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
RS Cosmology Module 2 packages a structural claim about the dimensionless combination $\Lambda \ell_P^2$. The module doc records the RS prediction $8\phi^5/45$ in the band $(1.88,2.03)\times 10^{-122}$, against the Planck value $\approx 1.99\times 10^{-122}$, and marks the module RS_PASS with zero sorry and zero axioms.
The certificate structure collects three elementary properties of the local domain cost and threshold: diagonal vanishing for nonzero arguments, nonnegativity on the positive quadrant, and positivity of the canonical threshold. Domain cost is the module-local cost functional imported from the Cost layer (with Constants supplying $\phi$). These are bookkeeping hypotheses, not the numerical band itself.
Upstream, the structure RSCosmo002Cert is exactly that triple of propositions; the present theorem only asserts the type is nonempty.
proof idea
One-line term proof. The module already defines a concrete value cert : RSCosmo002Cert. The theorem is the standard Nonempty introduction ⟨cert⟩, i.e. the pair constructor that turns an element into a proof of inhabitation. No tactics, no lemmas beyond the packaged cert.
why it matters
In the Recognition framework this is the inhabitation seal for Cosmology Module 2's structural certificate. The module targets the dimensionless cosmological constant $\Lambda \ell_P^2$ via the RS-native combination involving $\phi^5$ (linked to the forcing chain's $\phi$ fixed point and the constants layer $G=\phi^5/\pi$, $\hbar=\phi^{-5}$). Downstream use list is empty in the graph, so the theorem presently serves as the module-level existence flag rather than a lemma consumed by a larger chain step. It closes the STRUCTURAL THEOREM status advertised in the module doc: the certificate type is not vacuous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.