m_W_exp
plain-language theorem explainer
The declaration supplies the PDG 2024 experimental W-boson mass of 80377 MeV as a numeric constant for electroweak verification. Researchers comparing Recognition Science phi-ladder predictions to measured boson masses cite this value when checking ratios against the Weinberg angle relation. It is introduced through a direct numeric assignment with no derivation or computation steps.
Claim. The experimental mass of the W boson is defined by the constant equation $m_W^{exp} = 80377$ in units of MeV.
background
In the Recognition Science electroweak sector the boson masses sit on a phi-ladder whose rung integers are fixed for each particle. The module documentation states that experimental values are imported constants, not derived from RS, and gives the mass formula $m(EW,r)=2×φ^{50+r}/10^6$ MeV for B_pow=1 and r0=55. The Weinberg angle is fixed by sin²θ_W=(3-φ)/6, which enforces the relation M_Z=M_W/cos(θ_W). This definition supplies the rounded PDG 2024 central value 80377 MeV, distinct from the 80369.2 figure appearing in the upstream ElectroweakMasses module.
proof idea
The definition is a direct numeric assignment of the integer 80377 with no lemmas or tactics applied.
why it matters
The constant is used by the downstream theorem wz_ratio_exp_comparison, which confirms that the squared experimental ratio lies inside (0.7765,0.7775). It thereby anchors numerical checks of the theoretical electroweak relation derived from the phi-ladder and the eight-tick octave structure. The value matches the PDG 2024 entry quoted in the module documentation and closes the verification loop for the electroweak sector parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.