cert
plain-language theorem explainer
Packages a structural certificate for RS rung spacing: domain cost vanishes on equal arguments, stays nonnegative for positive mass/energy, and the canonical threshold is strictly positive. Anyone citing the phi-ladder spacing module uses this bundle. The definition is a three-field structure instance wiring sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(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. Adjacent rungs on the RS ladder are separated by the factor $\varphi\approx 1.618$.
background
Module 8 of the RS physics structural layer records that adjacent rungs on the recognition ladder differ by the golden-ratio factor $\varphi$. The local cost is a domain cost on pairs of positive reals (mass/energy-like arguments), built from the Recognition Science $J$-cost $J(x)=(x+x^{-1})/2-1$, which is nonnegative and vanishes only at the identity $x=1$.
The certificate structure demands three facts: diagonal vanishing of domain cost, nonnegativity off the diagonal for positive arguments, and positivity of a canonical threshold used as a spacing or acceptance cutoff. Upstream, the foundation layer already proves that every recognition event has nonnegative cost via $J$-cost nonnegativity.
Status is structural: zero sorry, zero axioms. The certificate is the single object that packages those three properties for downstream physics modules.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site; the definition only assembles already-proved facts into RSPHYStructural008Cert.
why it matters
Gives a single named witness that the rung-spacing structural claims hold: zero self-cost, nonnegative domain cost, and a positive threshold consistent with $\varphi$-ladder geometry. In the Recognition framework this sits under the structural physics layer that supports the mass formula on the $\varphi$-ladder (yardstick times $\varphi$ to a rung offset) and the forcing chain landmarks T5 ($J$-uniqueness) and T6 ($\varphi$ as self-similar fixed point).
No downstream consumers are recorded yet in the graph; the companion cert_inhabited likely only shows the type is nonempty. The module claims full structural closure (0 sorry, 0 axiom), so this definition is the export handle for that closure rather than a new derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.