mW_obs
plain-language theorem explainer
The declaration supplies the observed W-boson mass 80.4 GeV as the fixed reference for phi-ladder rung calculations in the Standard Model sector. Workers on the Recognition Science mass table cite it when normalizing the Higgs prediction against the W yardstick to obtain the fractional rung offset. The definition is a direct numerical assignment with no reduction or lemmas.
Claim. $m_W^{obs} = 80.4$ (GeV)
background
This definition sits inside the Higgs Mass Rung Assignment module, whose MODULE_DOC states that the Higgs mass is derived from the φ-ladder via Q₃ geometry to complete the RS particle mass table. The module treats observed masses as anchors for logarithmic offsets once the vev and Weinberg angle sin²θ_W = (3-φ)/6 are fixed. The upstream Z map from Anchor converts sector and charge data into integers that label the phi-ladder rungs, but mW_obs itself supplies the empirical W input used by the rung-offset formulas.
proof idea
The definition is a one-line constant assignment of the literal 80.4 to the real number mW_obs. No tactics or lemmas are invoked; the body simply returns the hardcoded value for use in downstream arithmetic.
why it matters
mW_obs anchors the W-boson at rung 21 so that higgs_rung_from_prediction can compute 21 + log_φ(m_H / m_W) and higgs_rung_in_range can prove the result lies in (21,22). It thereby supplies the empirical yardstick required by the mass formula yardstick · φ^(rung-8+gap(Z)) and supports the module's closure of the (120,130) GeV Higgs interval hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.