cert
plain-language theorem explainer
Packages three elementary facts about the domain cost used for RS rung spacing: zero cost on the diagonal, nonnegativity off the diagonal, and a strictly positive canonical threshold. Anyone citing the structural rung-spacing module can point at this single certificate rather than the three lemmas separately. The definition is a pure structure inhabitant wiring those three proofs into the certificate fields.
Claim. There is a certificate recording that (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, and (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_008 treats Recognition Science rung spacing: adjacent rungs on the mass ladder differ by the golden-ratio factor $\varphi\approx 1.618$. The module is marked structural (zero sorry, zero axiom).
The local cost is a real-valued domain cost on pairs of positive reals (mass/energy style arguments). Its diagonal vanishes and it is nonnegative off the diagonal; those two facts, together with positivity of a fixed canonical threshold, are the three fields of the certificate structure RSMTHStructural008Cert.
Upstream, nonnegativity of recognition cost is already known in ObserverForcing: "The cost of any recognition event is non-negative," proved via the standard $J$-cost nonnegativity lemma. The present certificate is the module-local packaging of the analogous domain-cost statements plus the threshold positivity fact.
proof idea
One-line structure inhabitant. The three certificate fields are filled by the already-proved sibling lemmas: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No additional tactic work.
why it matters
Gives a single named certificate for the three elementary cost/threshold facts that underwrite RS rung spacing by factor $\varphi$. Downstream consumers of the structural module can assume the certificate rather than re-import the three lemmas. In the broader framework this sits under the $\varphi$-ladder mass formula (yardstick times $\varphi$ to a rung offset) and the T6 forcing of $\varphi$ as the self-similar fixed point; the module itself claims structural status with no sorry and no axiom. No used-by edges are recorded yet, so the certificate is presently a local export rather than an input to a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.