row_mH_codata_pos
plain-language theorem explainer
The declaration proves positivity of the codata row holding the observed Higgs mass. Physicists verifying the Recognition Science Higgs scorecard inputs would cite it to confirm the numerical anchor satisfies the required inequality before interval claims. The proof is a term-mode wrapper that unfolds the definition to the constant 125.2 and applies norm_num.
Claim. $0 < m_{H,obs}$ where $m_{H,obs} := 125.2$ GeV is the observed Higgs boson mass.
background
The HiggsMassScoreCard module implements Phase 2 of the Recognition Science framework for the Higgs mass, comparing the predicted value $m_{H,rs} = v sqrt(sin^2 theta_W * 17/16)$ (with $v=246$ GeV and $sin^2 theta_W = (3-phi)/6$) against the PDG observation. row_mH_codata is defined directly as the observed mass mH_obs. The upstream result mH_obs supplies the concrete value 125.2 GeV as the Higgs observed mass in GeV.
proof idea
The term proof unfolds row_mH_codata to mH_obs and then to the literal constant 125.2, after which norm_num discharges the inequality 0 < 125.2.
why it matters
The result anchors positivity of the observed-mass input inside the Higgs mass scorecard. It supports the PARTIAL_THEOREM status of the module, which establishes the (120,130) GeV window while leaving the RS prediction comparison open. In the wider framework it supplies the numerical base for later proximity checks against the phi-ladder and eight-tick structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.