pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Physics.HiggsMassScoreCard

show as:
view Lean formalization →

This module assembles a scorecard for the Higgs boson mass prediction in Recognition Science. It imports the rung assignment to define codata rows, a prediction interval in (120, 130) GeV, and a certification theorem verifying agreement within five percent of the observed value. The structure consists of explicit row definitions followed by interval checks and a final holds theorem. A physicist working on the RS mass table would cite it to confirm the Higgs entry closes the particle spectrum.

claimThe Higgs mass scorecard certifies that the predicted interval $m_H^pred$ derived from the φ-ladder rung satisfies $m_H^pred ∈ (120, 130)$ GeV and $|m_H^pred - m_H^obs| / m_H^obs < 0.05$.

background

Recognition Science assigns particle masses via the φ-ladder, where each rung scales a base yardstick by φ raised to an integer power adjusted by gap(Z). The upstream HiggsRungAssignment module uses Q₃ geometry to place the Higgs on its rung, producing the core hypothesis that m_H lies in (120, 130) GeV. This scorecard module builds directly on that assignment by introducing codata rows for the prediction and the within-five-percent predicate.

proof idea

This is a definition module with supporting theorems. It first defines the codata row and positive codata row for the Higgs mass, then constructs the prediction interval from the rung value, and finally proves the within-five-percent condition by direct comparison of the interval bounds to the observed mass.

why it matters in Recognition Science

The module completes the Higgs entry in the RS particle mass table. It supplies the certification that feeds the overall verification of the Standard Model spectrum, linking the φ-ladder mass formula to experimental agreement. The certification closes the chain from the J-uniqueness and self-similar fixed point to an observable boson mass.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)