module module high

`IndisputableMonolith.StandardModel.HiggsRungAssignment`

This module defines the Higgs vacuum expectation value v ≈ 246 GeV and supporting electroweak observables for use in Recognition Science mass predictions. It supplies canonical inputs drawn from the Q₃ symmetry-breaking pattern and the φ-derived Weinberg angle. The module contains only definitions and positivity checks with no theorems.

claimThe Higgs vacuum expectation value satisfies $v ≈ 246$ GeV at the electroweak scale, together with observed masses $m_W ≈ 80.4$ GeV, $m_Z ≈ 91.2$ GeV, $m_H ≈ 125.2$ GeV and the level-3 RS prediction $m_{H,rs,3} = v √(sin²θ_W ⋅ 17/16)$ where sin²θ_W = (3-φ)/6.

background

The module sits inside the Standard Model sector and imports the RS time quantum τ₀ = 1 tick, the quaternion group Q₃ representations that encode spin-0 versus spin-1 Casimir eigenvalues for electroweak symmetry breaking, and the Weinberg angle θ_W derived from φ-structure with sin²θ_W ≈ 0.2229. The Higgs VEV marks the scale at which the Q₃ mechanism triggers symmetry breaking. Sibling definitions supply observed masses and positivity assertions for the RS-corrected Higgs mass at successive ladder levels.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the electroweak inputs required by the Higgs mass scorecard in IndisputableMonolith.Physics.HiggsMassScoreCard. It provides v and the φ-derived sin²θ_W for the explicit prediction mH_rs_level3 = v * sqrt(sin²θ_W * 17/16) that is compared with the PDG value 125.2 GeV. The definitions close the chain from RS φ-structure to concrete Standard Model mass numbers.

scope and limits

Does not derive the numerical value of v from the forcing chain or J-uniqueness.
Does not incorporate loop corrections or running of the masses.
Does not address neutrino masses or extensions beyond the basic Higgs sector.
Does not compute the full Q₃ representation spectrum or Casimir eigenvalues.

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