RSCosmo010Cert
plain-language theorem explainer
Certificate bundle for Cosmology Module 10 (solar metallicity): diagonal domain-cost vanishes, domain-cost is nonnegative on positive arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabited instance from the three sibling lemmas. Pure structure definition; no proof body.
Claim. A certificate is a triple of 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
Module 10 of the RS cosmology stack targets solar metallicity: $J(\varphi)^2 \approx 0.01393$ against $Z_\odot \approx 0.014$, reported as a structural match (zero sorry, zero axiom). The local cost on pairs of positive reals is the domain cost; the diagonal identity and nonnegativity of that cost, together with positivity of a canonical threshold, are the three structural gates packaged here.
Upstream, recognition-event cost is already known to be nonnegative: any recognition event has cost $0 \le e.\mathrm{cost}$ by nonnegativity of the $J$-cost on positive states. That global fact is the conceptual parent of the domain-cost nonnegativity field in this certificate.
proof idea
No proof: this is a structure whose three fields are propositions. 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 theorem that wraps that instance.
why it matters
Gives Module 10 a single named certificate type so the solar-metallicity structural claim can be discharged by inhabitation rather than by ad-hoc lemmas at each use site. Immediate consumers are the concrete certificate instance and the nonempty theorem in the same module. In the broader RS stack this sits under the cosmology domain and inherits the $J$-cost nonnegativity story from observer forcing; it does not itself restate the $J(\varphi)^2 \sim Z_\odot$ numerics, only the cost/threshold scaffolding those numerics rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.