RSFDNStructural008Cert
plain-language theorem explainer
Certificate type packaging three structural facts for foundation module 8 (phi rung spacing): domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code cites the inhabited instance to discharge the module's structural obligations. As a structure definition it only declares the three Prop fields; no proof body.
Claim. A structural certificate comprises three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 8 of the RS foundation structural series treats rung spacing on the Recognition ladder: adjacent rungs differ by the golden ratio $\phi \approx 1.618$, the self-similar fixed point forced at T6. Status is structural (zero sorry, zero axiom).
The domain cost is a real-valued comparison of two positive scales (measure versus expectation, or analogous pair). Its diagonal vanishing and nonnegativity mirror the J-cost minimum at identity and the global nonnegativity of recognition cost. Upstream, ObserverForcing records that every recognition event has nonnegative cost via Jcost_nonneg on a positive state.
The canonical threshold is the positive cutoff used when deciding whether a rung-scale mismatch is admissible; positivity keeps the decision region nonempty.
proof idea
No proof body: this is a structure declaration whose three fields are propositions. Inhabitation is supplied later by the sibling definition cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The nonempty theorem is then the one-line constructor application ⟨cert⟩.
why it matters
Gives the typed obligation bundle for structural module 8 so that rung-spacing facts can be discharged uniformly. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty of the certificate type, closing the module's structural claim.
In the broader forcing chain this sits under T6 ($\phi$ as self-similar fixed point) and the phi-ladder mass formula (yardstick times $\phi$ to a rung offset). Packaging diagonal vanishing, cost nonnegativity, and a positive threshold keeps the ladder comparison well-posed before mass or coupling numerics are attached. No open scaffold remains in this file; the certificate is fully inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.