module module high

`IndisputableMonolith.StandardModel.HiggsRungAssignment`

The HiggsRungAssignment module supplies the electroweak vacuum expectation value together with level-2 and level-3 Higgs mass expressions that incorporate Q3 corrections and the RS-derived Weinberg angle. Researchers building the Higgs mass scorecard or testing phi-ladder predictions against the 125 GeV observation cite these definitions. The module is a set of numerical assignments and interval checks with no deductive proofs.

claim$v = 246$ GeV sets the electroweak scale. The level-3 RS Higgs mass is $m_{H,rs,level3} = v sqrt(sin^2 theta_W * 17/16)$ with $sin^2 theta_W = (3 - phi)/6$.

background

This module sits inside the StandardModel domain and imports the RS time quantum tau_0 = 1 tick, the quaternion group Q3 representations that distinguish spin-0 versus spin-1 Casimir eigenvalues, and the Weinberg angle derived from phi-structure. The Q3 module states that the quaternion group Q3 = {±1, ±i, ±j, ±k} appears in RS as the structure for electroweak symmetry breaking. The WeinbergAngle module targets sin^2(theta_W) ≈ 0.2229 at the M_Z scale.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

These definitions are imported by the HiggsMassScoreCard module, which computes the phase-2 prediction mH_rs_level3 = v * sqrt(sin^2 theta_W * 17/16) and compares it to the PDG value m_H ≈ 125.2 GeV. The module supplies the electroweak inputs required for that scorecard. No open question is stated in the supplied doc-comment.

scope and limits

Does not derive the numerical value of v from RS primitives.
Does not prove the Q3 representation assignments for the Higgs.
Does not compute or justify the Weinberg angle expression.
Does not address higher-order radiative corrections beyond level 3.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.HiggsMassScoreCard module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.StandardModel.Q3Representations module_import
IndisputableMonolith.StandardModel.WeinbergAngle module_import

declarations in this module (17)

def vev L60
def mW_obs L63
def mZ_obs L66
def mH_obs L69
theorem vev_pos L72
def mH_naive L78
def mH_rs_level2 L82
theorem mH_rs_level2_in_range L86
def mH_rs_level3 L109
theorem q3_correction_pos L113
theorem mH_rs_level3_pos L117
theorem mH_prediction_in_interval L126
def higgs_rung_from_prediction L158
theorem higgs_rung_in_range L162
theorem mH_within_5_percent_of_observed L187
structure HiggsRungCert L196
theorem higgsRungCert L209