cert
plain-language theorem explainer
Packages three structural facts on the domain cost and the canonical threshold into one certificate for RS structural module 8 (adjacent rungs spaced by φ). Anyone citing the rung-spacing structural theorem uses this bundle. The definition is a pure structure instance: it wires three already-proved lemmas into the certificate fields.
Claim. There is a certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive arguments, $0\le\mathrm{domainCost}(m,e)$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_008 records the structural theorem that adjacent rungs on the Recognition ladder are separated by the golden ratio $\phi\approx 1.618$, with status zero sorry and zero axiom. The certificate type collects the cost and threshold side-conditions that make that spacing statement well-posed.
Domain cost is the local cost functional on pairs of positive reals used to compare measured and expected rung values; it is required to vanish when the two arguments agree and to stay nonnegative off the diagonal. The canonical threshold is the positive cutoff against which cost is compared when deciding whether a rung transition is admissible.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The present certificate lifts that style of positivity to the domain-cost pair used for rung spacing.
proof idea
One-line structure instance. The three fields of RSFDNStructural008Cert 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 new arithmetic is performed; the definition only assembles those proofs into the certificate record.
why it matters
This certificate is the packaged witness that the cost/threshold infrastructure for structural module 8 is inhabited. The module's stated content is RS rung spacing by factor $\phi$, which sits on the forcing-chain landmark T6 ($\phi$ as the self-similar fixed point) and feeds the mass ladder (yardstick times $\phi$ to a rung offset). Without diagonal vanishing and nonnegativity of domain cost, and without a positive threshold, the spacing claim would not be a well-typed structural theorem.
No downstream consumers are recorded in the graph yet; the natural parent is any theorem that assumes an RSFDNStructural008Cert (including the sibling inhabitedness fact). The declaration closes the local certificate interface rather than proving new physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.