row_sin2_thetaW_RS_bracket
plain-language theorem explainer
row_sin2_thetaW_RS_bracket supplies the numerical interval confirming that the Recognition Science prediction sin²θ_W = (3-φ)/6 lies strictly between 0.228 and 0.232. Electroweak precision analysts cite it when checking consistency between the RS-derived Weinberg angle and PDG-style references near 0.23. The proof is a one-line wrapper that invokes the upstream approximation theorem sin2ThetaW_RS_approx.
Claim. $0.228 < (3 - φ)/6 < 0.232$, where φ denotes the golden ratio.
background
The module Physics.WeinbergAngleScoreCard compares the RS prediction for the Weinberg angle against observed electroweak data. MODULE_DOC states the core formula sin²θ_W = (3-φ)/6 (aliased as sin2ThetaW_RS) and notes the observed reference ≈0.2229, with a falsifier if future measurements shift by more than 0.01 without changes to φ/α bounds. Upstream in Q3Representations, sin2ThetaW_RS is defined as (3 - phi)/6 and sin2ThetaW_RS_approx proves the stated bracket by unfolding the definition and applying phi bounds.
proof idea
This is a one-line wrapper that directly invokes the theorem sin2ThetaW_RS_approx from Q3Representations.
why it matters
The result feeds the certificate weinbergAngleScoreCardCert_holds, which packages the RS bracket together with codata and best-prediction match rows. It realizes the partial bridge described in MODULE_DOC between the leading RS formula and the reference value 0.2229, leaving rung-normalization and scheme dependence as residual open questions. The declaration sits inside the T5-T6 forcing chain that fixes φ as the self-similar point and generates the electroweak parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.