cert_inhabited
plain-language theorem explainer
The solar-metallicity certificate bundle for Cosmology Module 10 is nonempty: there is a concrete witness packing diagonal vanishing of the domain cost, its nonnegativity off the axes, and positivity of the canonical threshold. Cosmologists citing the RS Z_sun match use this as the existence gate. The proof is a one-line term that packages the prebuilt cert instance.
Claim. The type of certificates asserting (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) $\mathrm{canonicalThreshold}>0$, is inhabited.
background
Module 10 of the RS cosmology stack targets solar metallicity: the structural claim is that $J(\varphi)^2\approx 0.01393$ matches the observed $Z_\odot\approx 0.014$. Here $J$ is the unique cost functional forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$, and $\varphi$ is the self-similar fixed point from the forcing chain (T5–T6).
The certificate structure packages three elementary properties of the module’s domain cost and threshold: the cost vanishes on the diagonal away from zero, stays nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive. Those three fields are exactly the hypotheses a downstream consumer needs before quoting the numerical match.
No external axioms are used; the module is marked structural (zero sorry, zero axiom).
proof idea
One-line term proof. The sibling value cert already inhabits the structure, so ⟨cert⟩ is a witness for Nonempty RSCosmo010Cert. No tactics, no further lemmas.
why it matters
Existence of the certificate is the formal gate that lets Module 10 advertise a clean structural theorem for the solar-metallicity match $J(\varphi)^2\sim Z_\odot$. In the broader RS stack this sits under the cosmology domain and inherits the forced $J$ and $\varphi$ from T5–T6; the eight-tick and $D=3$ landmarks are not directly invoked here. No downstream consumers are recorded yet, so the declaration presently closes the module’s own inhabitance obligation rather than feeding a larger parent theorem. It touches no open scaffold: the claim status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.