sin2_theta_W
plain-language theorem explainer
The definition supplies the on-shell weak mixing angle as sin²θ_W = 0.23122 for electroweak calculations. RS modelers and particle physicists cite it to anchor W and Z mass ratios against measured values. It is introduced as a bare numerical assignment with no derivation or lemma steps.
Claim. The on-shell weak mixing angle satisfies $sin^2 θ_W = 0.23122$.
background
The module treats electroweak symmetry breaking as the Higgs VEV acquiring a J-cost minimum that reduces SU(2)_L × U(1)_Y to U(1)_EM. The weak mixing angle θ_W then relates the gauge couplings, with the mass relation m_Z = m_W / cos θ_W following from the embedding geometry. Upstream, PrimitiveDistinction.from supplies the seven axioms that yield the four structural conditions plus three definitional facts used throughout the framework; Constants.phi supplies the self-similar fixed point that fixes the phi-ladder rung for the electroweak scale.
proof idea
The declaration is a direct numerical definition. No lemmas or tactics are applied; the body simply assigns the constant 0.23122.
why it matters
It anchors the electroweak sector by supplying the input value that feeds BosonVerificationCert, cos2_theta_W, sin2_theta_W_bounds, and wz_ratio_eq_cos2. These in turn verify the RS predictions m_W ≈ 80.38 GeV, m_Z ≈ 91.19 GeV and the relation wz_mass_ratio_sq = cos2_theta_W. The definition connects to T5 J-uniqueness and the gauge-group geometry at the eight-tick octave, while leaving open the question of deriving the precise digit from the Recognition Composition Law without external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.