RSCOSStructural008Cert
plain-language theorem explainer
Certificate bundle for Cosmology Structural Module 8 (phi rung spacing). It packages three facts: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code cites it via a concrete inhabitant and a Nonempty proof. Pure structure definition; no proof body.
Claim. A structural certificate is a triple of properties: (1) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
Module RS_COS_Structural_008 treats Recognition Science rung spacing in cosmology: adjacent rungs differ by the golden ratio $\phi \approx 1.618$, the self-similar fixed point forced in the T0–T8 chain. Status is structural (zero sorry, zero axiom).
The certificate refers to a domain cost on pairs of positive reals (mass/energy or rung coordinates in the cosmology layer) and a canonical positive threshold used as a cutoff. Upstream, ObserverForcing records that every recognition-event cost is nonnegative via $J$-cost nonnegativity: "The cost of any recognition event is non-negative." The same nonnegativity pattern is lifted here to the cosmology domain cost.
Sibling lemmas in the module discharge the three fields: diagonal vanishing, nonnegativity for positive arguments, and positivity of the threshold.
proof idea
No proof: this is a structure declaration. It only names three Prop fields that any inhabitant must supply. The concrete packing lives in the sibling cert, which fills the fields from domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Inhabitation is then one constructor application.
why it matters
Gives a single named type for the structural obligations of Cosmology Module 8 so downstream code can demand "a certificate" rather than three loose lemmas. Parents are the concrete cert packing and cert_inhabited (Nonempty). That pattern matches other RS structural modules: bundle the local algebraic facts, then prove the bundle is inhabited.
Framework link: rung factor $\phi$ is the T6 fixed point; nonnegativity of cost traces to the T5 $J$-cost ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. The certificate does not itself derive $\phi$ or $D=3$; it only locks the cost and threshold hygiene needed when spacing cosmological rungs by $\phi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.