w_rung
plain-language theorem explainer
The definition assigns the integer 21 to the W-boson position on the Recognition Science phi-ladder via the mass formula with zero gap for W±. Modelers of electroweak symmetry breaking and Higgs mass ratios cite this constant when deriving predictions from Q3 Casimir eigenvalues of spin-0 and spin-1 sectors. The declaration is a direct constant assignment with no lemmas or computation.
Claim. The W-boson rung on the phi-ladder is defined as the integer 21.
background
The Q3 Representations module formalizes the quaternion group Q3 as the symmetry of the eight-tick cycle in the Recognition operator. Under electroweak breaking, the Higgs doublet splits into three Goldstone modes and one physical spin-0 Higgs, with mass ratios fixed by Casimir eigenvalues. The module states that the W-boson sits at rung 21 from the mass law with gap(W±) = 0, using the phi-ladder formula yardstick * phi^(rung - 8 + gap(Z)). Upstream rung definitions from Constants and Astrophysics modules establish the discrete tier structure for physical quantities such as nuclear densities and spectral peaks.
proof idea
One-line constant definition that directly assigns the integer 21, with no lemmas applied from upstream results such as rung or ledger factorization structures.
why it matters
This supplies the base rung for Higgs mass calculations. It feeds higgs_rung_from_prediction and HiggsRungCert in the HiggsRungAssignment module, where the latter certifies that the predicted m_H lies within 5% of the observed 125.2 GeV. The assignment instantiates the phi-ladder at the electroweak scale, consistent with the T7 eight-tick octave and the forced J-uniqueness from the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.