sin2thetaW
plain-language theorem explainer
RS supplies the Weinberg angle via the definition sin²θ_W := (3 - φ)/6. Researchers comparing RS predictions to electroweak data would reference this expression when checking agreement with the measured value near 0.231. The definition is introduced directly without further reduction or lemmas.
Claim. The square of the Weinberg angle is given by $sin^2 θ_W = (3 - φ)/6$, where φ is the golden ratio.
background
The module derives the Weinberg angle from the phi-ladder in the context of A1 SM Depth. It states: 'From §XXIII.D and GaugeBosonSpectrum: sin²θ_W = (3−φ)/6 ≈ 0.230'. The (3,2,1) rank decomposition yields sin²θ_W = g'²/(g² + g'²) = (rank-1)/(rank-1 + rank-2) with RS corrections leading to the phi expression. Phi is the self-similar fixed point from the forcing chain.
proof idea
This is a direct definition with no proof body beyond the assignment (3 - phi)/6. Downstream results unfold it to apply bounds on phi.
why it matters
It serves as the input to the certification structure SineSqThetaWCert and the theorems rs_near_pdg and sin2thetaW_band that quantify agreement with PDG data. The expression originates from the rank decomposition in the gauge boson spectrum, consistent with the Recognition Science derivation of D=3 and the eight-tick octave. It addresses the precision of SM parameter predictions within the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.