Physics Higgs Mass Score Card

Higgs mass scorecard

The Higgs boson, discovered in 2012, has a measured mass of about 125.2 GeV, a value that determines how other particles acquire mass through the Standard Model. In plain terms, the Higgs mass is a fundamental input to physics: it sets the scale for electroweak symmetry breaking, the process that gives the W and Z bosons their masses. The measured value comes from the Particle Data Group, the international collaboration that compiles particle physics results.

Recognition Science, a framework that derives physical constants from a forced cost function, offers a scorecard for this mass. The framework's prediction for the Higgs mass is m_H = v × sqrt(sin²θ_W × 17/16), where v = 246 GeV is the electroweak scale and sin²θ_W = (3 − φ)/6, with φ the golden ratio. This formula is a model, a definitional choice within the framework, not a derived theorem. The framework's library, a machine-checked collection of formal theorems, proves two things about this prediction: it falls in the interval (120, 130) GeV, and it lies within 5 percent of the observed 125.2 GeV.

The scorecard itself is a certificate: a formal structure that bundles these two proved facts. The theorem higgsMassScoreCardCert_holds states that the certificate exists, with no unproved assumptions and no new axioms added to the underlying logic. This means a reader can trust the arithmetic: the interval and the 5 percent proximity are checked by the machine, not asserted by hand.

What the scorecard does not do is pin down the exact mass. The central value 125.2 GeV is an input from measurement, not a framework output. The prediction lands within the window, but the precise number remains open. The framework's honest claim is a range, not a point. A future measurement outside (120, 130) GeV would falsify the prediction, provided the framework's inputs stay in their proved bands.

For a reader, the scorecard is a concrete example of how the framework handles empirical checks: it states a prediction, proves a bounded proximity to observation, and names the condition that would break it. The Higgs mass is not derived exactly, but its rough scale is shown to be consistent with the framework's structure.

theorem row_mH_pred_interval :
    120 < mH_rs_level3 ∧ mH_rs_level3 < 130 := mH_prediction_in_interval

theorem row_mH_within_five_percent :
    |mH_rs_level3 - row_mH_codata| / row_mH_codata < 0.05 := by
  simpa [row_mH_codata] using mH_within_5_percent_of_observed

theorem higgsMassScoreCardCert_holds : Nonempty HiggsMassScoreCardCert :=
  ⟨{ mass_interval := row_mH_pred_interval
     five_percent := mH_within_5_percent_of_observed }⟩

What this page does not claim

The exact Higgs mass is not derived; the central value 125.2 GeV is an external measurement. The prediction formula for m_H is a model, not a proved theorem. The framework does not prove that the Higgs mass must be 125 GeV, only that it lies in a window.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/HiggsMassScoreCard.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: