RSForcingChain011Cert
plain-language theorem explainer
Certificate structure for Foundation module 11 (phi-rung spacing) bundling three facts: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code cites the inhabited instance rather than the bare structure. Pure definition with no proof body; inhabitation is separate.
Claim. A module-11 certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is 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 11 of the RS forcing chain is about rung spacing: consecutive rungs on the $\varphi$-ladder are separated by the golden-ratio factor $\varphi=(1+\sqrt{5})/2$. Status is structural (zero sorry, zero axiom).
The domain cost is the local cost used to score a mismatch between a measured scale and an expected scale. The canonical threshold is the positive cutoff against which those costs are compared in this module. Both appear as sibling definitions that the certificate fields quantify over.
Upstream, ObserverForcing already records that every recognition event has nonnegative cost, via the J-cost nonnegativity lemma. The present structure lifts that nonnegativity pattern to domain cost and adds diagonal vanishing plus threshold positivity as the package module 11 will inhabit.
proof idea
Pure structure definition: no proof body and no tactics. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on positive arguments, positivity of the canonical threshold). Inhabitation is discharged later by the sibling cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to those fields, and by cert_inhabited, which wraps that assignment as Nonempty.
why it matters
Packages the cost and threshold facts that module 11 needs before any rung-spacing argument can run. Downstream, cert builds a concrete inhabitant and cert_inhabited records that the type is nonempty, closing the structural obligation for this module (0 sorry, 0 axiom).
In the broader forcing chain this sits next to T6 ($\varphi$ as the self-similar fixed point) and the mass formula on the $\varphi$-ladder (yardstick times $\varphi$ to a rung offset). The certificate itself does not force spacing by $\varphi$; it only freezes the cost/threshold interface those spacing claims depend on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.