cert
plain-language theorem explainer
A concrete certificate packing three domain-cost facts into the W-boson mass RS4 structure: diagonal vanishing, nonnegativity for positive masses/energies, and a strictly positive canonical threshold. Anyone citing the structural W-boson mass package in RS units uses this witness. The body is a pure field assembly of three already-proved sibling lemmas.
Claim. There is a witness for the W-boson mass RS4 package: for every nonzero real $r$, the domain cost satisfies $\mathrm{domainCost}(r,r)=0$; for all positive $m,e$, $\mathrm{domainCost}(m,e)\ge 0$; and the canonical threshold is strictly positive.
background
This module is the RS physics foundation layer marked as a structural theorem package (zero sorry, zero axioms). The local object is a structure that packages the cost-theoretic side conditions needed for a W-boson mass statement in RS-native units.
Domain cost is the recognition cost assigned to a mass/energy pair; on the diagonal it must vanish (perfect match costs nothing), and off-diagonal it must stay nonnegative. That nonnegativity is the continuum shadow of the upstream fact that every recognition event has nonnegative J-cost: "The cost of any recognition event is non-negative," proved from $J$-cost nonnegativity at positive state.
The canonical threshold is the positive cutoff against which the cost comparison is judged. The three fields of the structure are exactly those three arithmetic claims.
proof idea
One-line structure inhabitant. Each field is filled by a named sibling lemma already in the module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
This is the explicit certificate named in the module header (WBosonMassRS4Cert). It turns the abstract W-boson mass RS4 interface into an inhabited object inside the zero-sorry foundation session. Downstream consumers that need a term of that structure type can point here rather than re-proving the three cost axioms. In the broader RS chain it sits under the cost layer forced by T5 J-uniqueness and the Recognition Composition Law, supplying the nonnegativity and threshold positivity that any mass-ladder comparison (yardstick times a phi-power) must respect. No used-by edges are recorded yet; the immediate sibling cert_inhabited is the natural next citation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.