cert
plain-language theorem explainer
Packages three structural facts about the cosmology domain cost into a single certificate for the Li-7 Spite plateau module: the cost vanishes on the diagonal, stays nonnegative for positive model and evidence, and the canonical threshold is positive. Cosmology auditors cite it as the inhabited witness that Module 12 meets its cost axioms. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of matching $r$ against itself is zero; (ii) for all positive reals $m,e$, the domain cost of model $m$ against evidence $e$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_Cosmo_Module_012 treats the lithium-7 Spite plateau as a Recognition Science cosmology check. The reported RS band is $(4.69,4.86)\times 10^{-10}$ against the observed window $(4.0,5.2)\times 10^{-10}$, marked RS_PASS, and the file is a structural theorem package (zero sorry, zero axiom).
The certificate type bundles three cost axioms used throughout the module. Domain cost is the local discrepancy functional between a model value and an evidence value; its diagonal vanishing and nonnegativity mirror the global J-cost properties from the foundation layer (the cost of any recognition event is nonnegative, and the identity event sits at the J-cost minimum $x=1$). The canonical threshold is the positive cutoff against which the plateau band is judged.
Upstream, cost_nonneg in ObserverForcing already guarantees $0\le e.\mathrm{cost}$ via Jcost_nonneg on positive states. The siblings domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize those facts to this cosmology domain.
proof idea
One-line structure construction. The three fields of RSCosmo012Cert are filled by the corresponding sibling lemmas: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No extra algebra or case splits occur at this site.
why it matters
Gives Module 12 a single named witness that its domain cost obeys the Recognition cost axioms required for the Spite-plateau band check. In the broader RS stack this is the cosmology-side counterpart of the foundation nonnegativity of J-cost (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), specialized to lithium-7 abundance comparison. No downstream consumers are wired yet; the sibling cert_inhabited is the natural next use. The declaration does not itself derive the numerical band $(4.69,4.86)\times 10^{-10}$; it only certifies the cost scaffolding those numbers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.