RSCosmo012Cert
plain-language theorem explainer
Certificate structure for Cosmology module 12 (Li-7 Spite plateau) packing three domain-cost properties: diagonal vanishing, nonnegativity on positive arguments, and a strictly positive canonical threshold. Downstream code cites it via the concrete inhabitant `cert` and the Nonempty witness. Pure structural packing: field types only, no proof body.
Claim. A Li-7 Spite-plateau certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the matched 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 12 sits in the RS cosmology stack and targets the lithium-7 Spite plateau. The module doc records an RS prediction band $(4.69,4.86)\times 10^{-10}$ against the observed window $(4.0,5.2)\times 10^{-10}$, marked RS_PASS, with status structural (zero sorry, zero axiom).
The certificate is built from a local domain cost on pairs of positive reals (siblings domainCost, domainCost_at_eq, domainCost_nonneg) and a positive scalar threshold (canonicalThreshold, canonicalThreshold_pos). Nonnegativity of recognition cost is the ambient prior: upstream cost_nonneg states that every recognition event has nonnegative cost, via Jcost_nonneg on a positive state.
In RS units the cost landscape is the unique J-cost forced at T5, $J(x)=(x+x^{-1})/2-1$, minimized at the identity $x=1$. The diagonal-vanishing field encodes that matched mass/energy ratios sit at that minimum.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements on domainCost and canonicalThreshold. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, then wrapped by the Nonempty theorem.
why it matters
Gives the typed interface that module 12 must satisfy before the Spite-plateau claim is treated as certified. Downstream cert is the concrete record inhabitant; cert_inhabited promotes it to Nonempty RSCosmo012Cert, the usual RS pattern for structural module certificates.
The module ties a nuclear-abundance observable (Li-7 plateau) to the same cost nonnegativity and threshold positivity used elsewhere in the forcing chain. It does not itself re-derive T5–T8 or the mass ladder; it packages the local cost axioms so the cosmology layer can report RS_PASS against the observed band without axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.