Pith. sign in
module module moderate

IndisputableMonolith.Physics.HiggsMassScoreCard

show as:
view Lean formalization →

The HiggsMassScoreCard module certifies the Higgs boson mass prediction obtained from the φ-ladder. It assembles codata rows, positivity checks, and an interval comparison to confirm the derived value lies within five percent of the experimental range. The module structure consists of supporting definitions followed by a top-level certification that applies the upstream rung assignment directly.

claimThe predicted Higgs mass $m_H$ from the φ-ladder satisfies $m_H \in (120,130)$ GeV and lies within five percent of the observed value.

background

This module sits in the Recognition Science treatment of Standard Model masses. It imports the HiggsRungAssignment module whose core claim is that the Higgs mass satisfies $m_H otin (120,130)$ GeV derived from the φ-ladder using Q₃ geometry and thereby completes the RS particle mass table.

Sibling definitions supply row_mH_codata for the mass data, row_mH_codata_pos for positivity, row_mH_pred_interval for the derived range, and row_mH_within_five_percent for the closeness test. The final objects HiggsMassScoreCardCert and higgsMassScoreCardCert_holds package the scorecard result.

proof idea

This is a definition module, no proofs. It assembles the codata rows and interval predicates imported from HiggsRungAssignment, then states the certification as a top-level proposition.

why it matters in Recognition Science

The module supplies the certification step that closes the Higgs entry in the RS particle mass table. It directly consumes the rung-assignment hypothesis and thereby supports the overall claim that all Standard Model masses are fixed by the φ-ladder construction. No downstream uses are recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)