row_mH_codata
plain-language theorem explainer
The observed Higgs boson mass of 125.2 GeV is supplied as the fixed experimental anchor for scorecard comparisons in the Recognition Science Higgs mass prediction. Researchers validating electroweak symmetry breaking relations or phi-ladder mass formulas would cite this value when checking the five-percent proximity to the RS prediction. The definition is a direct noncomputable alias to the PDG input with no algebraic reduction or lemmas applied.
Claim. Define the observed Higgs mass row by the real number 125.2 GeV, where this value is taken directly from the PDG measurement of the Higgs boson mass.
background
The Higgs mass scorecard module compares an RS-derived prediction mH_rs_level3 = v * sqrt(sin²θ_W * 17/16), with v = 246 GeV and sin²θ_W = (3 - φ)/6, against the experimental value. The upstream constant supplies the observed Higgs mass in GeV as the PDG figure 125.2. This anchors the partial theorem status for the (120, 130) GeV window and the five-percent agreement claim documented in the module.
proof idea
The definition is a direct alias to the upstream observed mass constant. No tactics or lemmas are invoked beyond the assignment itself.
why it matters
This supplies the experimental input for the downstream theorems establishing positivity of the observed mass and that the RS prediction lies within five percent. It completes the P2-HIGGS scorecard setup, linking the phi-based mass formula to the measured value. The relevant framework landmark is the Higgs mass on the phi-ladder; the open question remains the exact RS derivation of the 246 GeV vacuum expectation value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.