row_sin2_thetaW_codata_bracket
plain-language theorem explainer
The theorem establishes that the observed Weinberg angle squared lies strictly between 0.22 and 0.23. Electroweak precision analysts would cite this interval when anchoring Recognition Science predictions against PDG-style references. The proof is a one-line simpa wrapper that unfolds the codata alias and invokes the bounds theorem from the WeinbergAngle module.
Claim. $0.22 < sin^2 theta_W^{observed} < 0.23$ where the observed value is the PDG-style reference sin2ThetaW_observed.
background
The WeinbergAngleScoreCard module develops a scorecard for the electroweak Weinberg angle in Phase 2. It contrasts the RS core prediction sin²θ_W = (3-φ)/6 against the observed value sin2ThetaW_observed ≈ 0.2229. The upstream theorem sin2_theta_bounds asserts that this observed quantity lies strictly between 0.22 and 0.23, established by unfolding the definition and applying norm_num.
proof idea
The proof is a one-line wrapper. It invokes simpa with the unfolding of row_sin2_thetaW_codata and directly applies the sin2_theta_bounds theorem from the WeinbergAngle module.
why it matters
This bound populates the codata_in_ref_band field inside weinbergAngleScoreCardCert_holds, which certifies the full scorecard. It realizes the partial bridge described in the module documentation for the P2-θW phase. In the Recognition Science framework, the interval anchors comparisons of the phi-derived electroweak prediction to experimental data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.