module module high

`IndisputableMonolith.StandardModel.HiggsRungAssignment`

This module supplies the Higgs vacuum expectation value v ≈ 246 GeV together with auxiliary observables and rung assignments for electroweak-scale mass predictions inside Recognition Science. It assembles inputs from the RS time quantum, Q3 quaternion representations, and the φ-derived Weinberg angle to support the Higgs mass scorecard. The module consists entirely of definitions with no proofs.

claim$v \approx 246$ GeV (Higgs vacuum expectation value at the electroweak scale), together with $m_W$, $m_Z$, $m_H$ observables and the level-2/level-3 rung assignments that incorporate the Q$_3$ correction and $\sin^2\theta_W = (3-\phi)/6$.

background

The module sits inside the Standard Model section of Recognition Science and imports the RS time quantum $\tau_0 = 1$ tick from Constants, the quaternion group Q$3$ representation theory that governs electroweak symmetry breaking from Q3Representations, and the derivation of the weak mixing angle from the golden-ratio fixed point $\phi$ in WeinbergAngle. The supplied doc-comment states the central object: Higgs VEV $v \approx 246$ GeV. Sibling definitions include vev, mW_obs, mZ_obs, mH_obs, mH_naive, mH_rs_level2, mH_rs_level3 and the positivity and interval predicates that prepare the mass formula $mH{rs_level3} = v \sqrt{\sin^2\theta_W \cdot 17/16}$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the electroweak inputs required by the downstream Higgs mass scorecard in IndisputableMonolith.Physics.HiggsMassScoreCard. That scorecard computes the RS-predicted $m_H$ at level 3 and compares it with the PDG value 125.2 GeV, using the exact expression $mH_{rs_level3} = v \sqrt{\sin^2\theta_W \cdot 17/16}$ with $v = 246$ GeV and $\sin^2\theta_W = (3-\phi)/6$. It therefore closes the chain from the T5–T8 forcing steps through Q3 representations to a concrete, falsifiable particle-mass prediction.

scope and limits

Does not derive the numerical value of v from the RS forcing chain.
Does not perform loop corrections or running of couplings.
Does not address neutrino masses or flavor mixing.
Does not claim uniqueness of the Q3 representation assignment.

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