cert
plain-language theorem explainer
Packages three structural facts for RS cosmology rung spacing by φ: domain cost vanishes on the diagonal, stays non-negative for positive mass/energy arguments, and the canonical threshold is strictly positive. Cosmologists citing the φ-ladder spacing module would reach for this certificate. It is a structure inhabitant that wires three already-proved sibling lemmas; no new argument.
Claim. There is a certificate recording that the domain cost satisfies $C(r,r)=0$ for every $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
Module RS_COS_Structural_008 treats RS rung spacing: adjacent rungs on the recognition ladder are separated by the golden ratio $\phi\approx 1.618$. Status is structural (zero sorry, zero axiom).
The certificate structure demands three properties of a domain cost $C$ and a canonical threshold $T$. Diagonal vanishing ($C(r,r)=0$ for $r\neq 0$) says matched mass/energy pairs carry zero recognition cost. Non-negativity for positive arguments is the cost axiom inherited from the J-cost framework: upstream, ObserverForcing records that "the cost of any recognition event is non-negative" via $J$-cost non-negativity. Positivity of $T$ supplies a strict cutoff used when comparing rung separations to the $\phi$ factor.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos already discharge those three obligations; this definition only assembles them.
proof idea
One-line structure inhabitant. The three fields of RSCOSStructural008Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity on positive reals), and canonicalThreshold_pos (strict positivity of the threshold). No tactic proof and no new algebra; pure packaging of prior results.
why it matters
Gives a single named witness that the structural cost and threshold facts for Module 8 hold, so downstream cosmology developments can depend on one object rather than three separate lemmas. The module frames RS rung spacing by $\phi$, which sits on the forcing chain after T6 ($\phi$ as self-similar fixed point) and feeds the mass formula on the $\phi$-ladder (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). No downstream uses are recorded yet; the companion cert_inhabited likely only asserts non-emptiness of the certificate type. Closes the structural packaging step for this cosmology module without opening new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.