cert_inhabited
plain-language theorem explainer
The Li-7 Spite-plateau certificate type is inhabited: there exists a packed witness that domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Cosmology auditors of RS Module 12 cite this for structural completeness. The proof is a one-line term introducing the concrete `cert` instance into `Nonempty`.
Claim. There exists a certificate packing three facts: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$ the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
RS Cosmology Module 12 treats the lithium-7 Spite plateau. The module claims an RS prediction band $(4.69,4.86)\times 10^{-10}$ lying inside the observed window $(4.0,5.2)\times 10^{-10}$, and records status RS_PASS as a structural theorem (zero sorry, zero axiom).
The certificate structure bundles three elementary properties of the local cost: diagonal vanishing (domainCost r r = 0 for $r\neq 0$), nonnegativity for positive arguments, and positivity of a fixed canonical threshold. Domain cost is the module's specialization of the Recognition J-cost to the cosmology comparison variables; the threshold is the positive cutoff used to gate the band claim.
Upstream, the structure itself is only a Prop-packing record. Inhabitation is what turns the record into a usable witness that the three cost lemmas have been discharged inside the module.
proof idea
Term-mode one-liner. The proof supplies the already-constructed value cert (the concrete inhabitant of the certificate structure) as the witness for Nonempty, via the standard constructor ⟨cert⟩. No tactics, no further lemmas.
why it matters
Closes the structural side of Cosmology Module 12: once the certificate type is known to be inhabited, downstream cosmology exports can assume the three cost facts without re-proving them. The module doc frames this as part of the Li-7 Spite-plateau RS_PASS package. No further used-by edges are recorded yet; the lemma is the terminal inhabitance stamp for the module's certificate. It does not itself derive the numerical band from the forcing chain (T5 J-uniqueness, T6 phi, etc.); it only certifies that the local cost interface is consistent and nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.