cert
plain-language theorem explainer
Packages three structural facts about the RS domain cost and canonical threshold into a single certificate for Standard Model structural module 8 (rung spacing by φ). Anyone citing the φ-ladder spacing package or the module's zero-sorry status would use this. The definition is a pure structure assembly: it wires three already-proved sibling lemmas into the certificate fields.
Claim. There is a certificate whose fields assert: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ vanishes; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 8 of the RS Standard Model structural layer records rung spacing: adjacent mass rungs differ by the golden ratio $\phi \approx 1.618$, forced earlier in the T5–T6 uniqueness chain for the J-cost $J(x)=(x+x^{-1})/2-1$. Status is structural theorem (zero sorry, zero axiom).
The certificate structure bundles three properties of a domain cost functional on pairs of reals (mass/energy style arguments) together with a positive canonical threshold. Domain cost is the local cost used to compare rung placements; it is required to vanish on the diagonal (equal arguments) and stay nonnegative off it, mirroring the global fact that recognition cost is nonnegative (ObserverForcing: "The cost of any recognition event is non-negative").
Sibling lemmas already establish diagonal vanishing, nonnegativity for positive arguments, and positivity of the canonical threshold. This declaration only packages them.
proof idea
One-line structure construction. The three fields of RSSTDStructural008Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass and energy), and canonicalThreshold_pos (strict positivity of the threshold). No new arithmetic is performed; the definition is pure assembly of prior proofs.
why it matters
Gives the inhabited certificate object for RS structural module 8, so downstream code can treat rung-spacing-by-$\phi$ as a single certified package rather than three loose lemmas. The module doc marks the whole file as a structural theorem with zero sorry and zero axiom; this definition is the concrete witness that the three cost/threshold obligations hold.
It sits on the Standard Model side of the forcing chain: T5 uniqueness of $J$, T6 forcing of $\phi$ as the self-similar fixed point, and the mass formula on the $\phi$-ladder (yardstick times $\phi$ to a rung offset). No parent theorems are listed yet in the use graph; the natural consumers are any later SM packing or mass-ladder theorems that require a single certificate rather than ad-hoc appeals to the three siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.