RSMTHStructural008Cert
plain-language theorem explainer
Certificate structure packaging three structural facts for RS module 8 (phi rung spacing): domain cost vanishes on the diagonal, is nonnegative on positive arguments, and the canonical threshold is strictly positive. Downstream code cites it via the inhabited `cert` value. Pure definitional bundle; no proof body.
Claim. A certificate record asserting three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_008 treats Recognition Science rung spacing: adjacent rungs on the mass/scale ladder differ by the golden ratio $\phi \approx 1.618$. Status is structural (zero sorry, zero axiom).
The certificate fields refer to two local objects. Domain cost is a real-valued cost on pairs $(m,e)$ (measurement versus expectation style arguments), built from the RS $J$-cost. The canonical threshold is a fixed positive real used as a comparison scale in the same module.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative, via $J$-cost nonnegativity on positive states. The present structure lifts the analogous nonnegativity (and diagonal vanishing) into an explicit certificate type for the mathematics layer.
proof idea
No proof: this is a structure declaration whose three fields are propositions. Inhabitation is supplied separately by the noncomputable definition cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The companion theorem cert_inhabited then wraps that value as Nonempty.
why it matters
Gives a single named type for the structural obligations of Mathematics module 8 (phi-spaced rungs). Downstream, cert is the concrete inhabitant and cert_inhabited proves the type is nonempty, so later developments can assume the package without re-proving diagonal vanishing, cost nonnegativity, or threshold positivity.
In the broader RS chain this sits under the phi-forced self-similar scale (T6) and the phi-ladder mass formula. It does not itself force $\phi$ or the eight-tick octave; it only certifies cost and threshold hygiene used when talking about adjacent-rung separation by $\phi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.