sin2thetaW_band
plain-language theorem explainer
Recognition Science predicts the Weinberg angle squared in the narrow band 0.228 to 0.232 via the expression (3 - φ)/6. Electroweak precision tests in particle physics would cite this interval to validate the RS mass formulas against measured values. The proof reduces the claim to linear inequalities on the golden ratio using its established bounds 1.61 < φ < 1.62.
Claim. $0.228 < (3 - φ)/6 < 0.232$, where φ denotes the golden ratio.
background
The module defines the RS Weinberg angle as sin²θ_W_RS = (3 - φ)/6, paired with the mass ratio m_Z/m_W = 6/(3 + φ). These expressions arise from the phi-ladder construction in Recognition Science, where φ is the self-similar fixed point. Upstream results supply the numerical bounds 1.61 < φ < 1.62, described as 'Even tighter lower bound: φ > 1.61' and 'Tighter upper bound: φ < 1.62', derived from square-root comparisons in the Constants module.
proof idea
The proof unfolds sin2thetaW_RS to (3 - phi)/6. It invokes the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo. A constructor splits the conjunction, and each side applies div_lt_div_of_pos_right followed by linarith to compare the expressions against the numerical bounds.
why it matters
This theorem supplies the sin2theta_band field in the GaugeBosonMassCert definition, which certifies the RS predictions for gauge boson masses. It aligns with the T6 phi fixed point in the forcing chain, anchoring the alpha inverse near 137. The result supports numerical agreement with PDG data as seen in the related rs_near_pdg theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.