m_H_exp
plain-language theorem explainer
The declaration supplies the PDG 2024 experimental Higgs boson mass of 125250 MeV as a numeric constant for verification against Recognition Science electroweak predictions. Researchers comparing phi-ladder rung assignments for the Higgs to observed data would reference it when checking the formula m(EW, r) = 2 × φ^{50+r} / 10^6 MeV. It is introduced as a direct numeric definition with no derivation or computational steps.
Claim. The experimental Higgs boson mass is taken as the constant 125250 MeV.
background
In the electroweak sector, Recognition Science places boson masses on the phi-ladder via the formula m(EW, r) = 2 × φ^{50+r} / 10^6 MeV for B_pow = 1 and r0 = 55. The module treats experimental values as imported constants rather than internally derived quantities, with the Higgs occupying a specific rung alongside W and Z. The Weinberg angle enters as sin²θ_W = (3 − φ)/6 ≈ 0.2303, linking the masses through M_Z = M_W / cos(θ_W).
proof idea
The definition is a direct numeric assignment of the constant 125250 with no lemmas applied.
why it matters
This definition supplies the experimental anchor referenced by the ElectroweakMasses module for comparing RS phi-ladder predictions to PDG data. It supports verification of the mass formula and the eight-tick octave structure within the T0-T8 forcing chain. It touches the open question of alignment precision between imported constants and the derived RS values without providing a derivation from the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.