cert
plain-language theorem explainer
Packages three structural facts about the W-boson domain cost into one inhabited certificate: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Anyone citing Module 12's W-mass match (M_W ≈ φ^13 · 0.154) uses this bundle as the formal witness. The body is a pure structure instance wiring three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 12 records the W-boson mass match $M_W = 80.4,\mathrm{GeV} \sim \varphi^{13}\cdot 0.154 = 80.3,\mathrm{GeV}$ as a structural theorem (zero sorry, zero axiom). The local cost is a domain-level specialization of the Recognition 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 properties of that domain cost: it is zero on the diagonal away from zero, it stays nonnegative for positive mass and energy arguments, and a fixed positive threshold (the module's acceptance gate) is available. Upstream, ObserverForcing already proves that every recognition event has nonnegative cost via $J$-cost nonnegativity.
proof idea
One-line structure instance. The three fields of RSPhysics012Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no extra tactic work or algebraic reduction occurs here.
why it matters
Gives Module 12 a single named witness that the W-sector cost geometry is well-formed before any numerical mass comparison is trusted. In the RS forcing chain this sits downstream of T5 (J-uniqueness) and the phi-ladder mass formula (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), of which the W rung is a concrete instance. No downstream consumers are wired yet in the graph; the natural parent is any global physics-certificate aggregator that requires per-module cost hygiene. Closes the structural side of the W-mass MATCH claim without touching the numerical fit itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.