cert_inhabited
plain-language theorem explainer
The theorem establishes that the certificate structure encoding RS predictions for stellar elemental abundances is non-empty by supplying an explicit witness. Cosmochemists comparing phi-ladder models to solar abundance data would cite it to confirm simultaneous satisfaction of the ratio and cost conditions. The proof is a direct term construction that applies the cert witness to the Nonempty constructor.
Claim. The structure encoding stellar abundance predictions is inhabited: there exists a certificate $C$ such that the even-odd abundance ratio $r$ satisfies $1 < r$ and $1.5 < r < 3.0$, together with the condition that abundance cost vanishes on the diagonal, i.e., abundanceCost$(a,a)=0$ for all $a≠0$.
background
The module treats stellar elemental abundances as consequences of the phi-ladder on nuclear binding energies, reproducing the Oddo-Harkins even-odd oscillation. StellarAbundanceCert is the record structure whose fields are the three required properties: ratio greater than one, ratio inside the interval (1.5,3.0), and vanishing cost when both arguments are equal. The local setting is the structural theorem that the RS J-cost function on the phi-ladder forces the observed abundance pattern without extra parameters.
proof idea
The proof is a one-line term that constructs an element of Nonempty StellarAbundanceCert by supplying the explicit cert witness to the Nonempty constructor.
why it matters
This existence result closes the consistency check for the abundance certificate inside the cosmochemistry module, confirming that the phi-ladder predictions are non-vacuous. It supports the module claim that the even-odd ratio lies in the predicted band for iron-peak elements and aligns with the broader Recognition Science derivation of abundances from the J-cost structure. No downstream theorems are recorded, so the declaration functions as a terminal existence statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.