cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single certificate for RS forcing-chain module 10: equal arguments give zero cost, the cost is nonnegative on positive reals, and the canonical threshold is positive. Calibration workers cite it when wiring E_coh as the free parameter fixed by the electron at rung 3. The body is a structure instance that assigns three already-proved sibling lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of $(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 10 of the RS forcing chain treats calibration: the coherence energy $E_{\mathrm{coh}}$ is the single free parameter, fixed by the electron mass at rung 3 on the $\varphi$-ladder. The module is marked structural (zero sorry, zero axiom).
The certificate structure bundles three Prop fields about a real-valued domain cost and a canonical threshold. Domain cost is the local cost functional on pairs of positive reals used in this calibration layer; equal nonzero arguments must sit at the J-cost minimum (value zero), and the cost must stay nonnegative off the diagonal. The canonical threshold is the positive cutoff against which calibrated comparisons are made.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states. The three sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the structure fields pointwise.
proof idea
Pure structure construction. The definition is noncomputable only because the ambient cost infrastructure is; the body fills the three fields of RSForcingChain010Cert by direct assignment of the sibling lemmas that already prove vanishing on the diagonal, nonnegativity for positive arguments, and positivity of the canonical threshold. No extra tactics or algebraic work.
why it matters
Gives a single named inhabitant of the module-10 certificate so downstream calibration code can demand one object rather than three separate hypotheses. In the forcing-chain architecture this sits under the structural layer that fixes $E_{\mathrm{coh}}$ from the electron at rung 3, consistent with the mass formula on the $\varphi$-ladder and the T5–T6 uniqueness of $J$ and $\varphi$. No used_by edges are recorded yet; the companion cert_inhabited lemma is the natural next consumer. Closes the local certificate interface with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.