row_mH_codata_pos
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 in Recognition Science
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.
scope and limits
- Does not derive the Higgs mass from the forcing chain or Recognition Composition Law.
- Does not incorporate measurement uncertainties or PDG error bars.
- Does not establish proximity of 125.2 GeV to the RS prediction formula.
formal statement (Lean)
32theorem row_mH_codata_pos : 0 < row_mH_codata := by
proof body
Term-mode proof.
33 unfold row_mH_codata mH_obs
34 norm_num
35