RSForcingChain010Cert
plain-language theorem explainer
A certificate bundling three calibration facts for RS Module 10: diagonal domain cost vanishes, domain cost is nonnegative for positive arguments, and the canonical threshold is positive. Calibration and forcing-chain consumers cite it to discharge the structural side conditions of the E_coh rung-3 setup. It is a pure structure definition; inhabitance is supplied separately by packing three sibling lemmas.
Claim. A certificate consists of 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 10 of the RS forcing chain treats calibration: $E_{\mathrm{coh}}$ is the single free parameter, fixed by the electron mass at rung 3. The module is marked structural (zero sorry, zero axiom).
Domain cost is the real-valued cost assigned to a mass/energy pair in this calibration layer. The diagonal identity (cost of $(r,r)$ vanishes for $r\neq 0$) encodes that matched recognition carries no excess cost. Nonnegativity for positive arguments is the continuous analogue of the observer-level fact that every recognition event has nonnegative cost (via $J$-cost nonnegativity on positive states).
The canonical threshold is the positive cutoff used to separate calibrated regimes in the same module. Upstream, cost_nonneg on recognition events states: "The cost of any recognition event is non-negative," proved from $J$-cost nonnegativity.
proof idea
No proof body: this is a structure definition with three fields. Inhabitance is not proved here. The sibling definition cert packs domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos into the three fields; cert_inhabited then wraps that packing as Nonempty.
why it matters
Gives Module 10 a single named certificate type for the three structural side conditions of RS calibration (diagonal vanishing, cost nonnegativity, positive threshold). Downstream, cert inhabits it and cert_inhabited records nonemptiness, so later forcing-chain steps can assume the bundle rather than re-prove each lemma.
In the broader framework this sits under the forcing chain and cost calculus: nonnegativity traces to $J$-cost (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), while the calibration story fixes $E_{\mathrm{coh}}$ from the electron at rung 3 on the $\varphi$-ladder. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only packages the local cost/threshold facts those later steps rely on when reading Module 10.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.