row_sin2_thetaW_codata_bracket
The observed PDG-style value of sin²θ_W satisfies the strict numerical bounds 0.22 < sin²θ_W < 0.23. Researchers auditing the Recognition Science electroweak scorecard cite this bracket to place the codata inside the reference interval used for the (3-φ)/6 prediction. The proof is a one-line wrapper that unfolds the codata alias and invokes the bound theorem from the WeinbergAngle module.
claim$0.22 < sin^2 θ_W^{obs} < 0.23$, where $sin^2 θ_W^{obs}$ is the observed Weinberg angle squared sine from the PDG-style reference.
background
In the WeinbergAngleScoreCard module the codata row_sin2_thetaW_codata is defined as the observed sin²θ_W value imported from the StandardModel.WeinbergAngle module. The local theoretical setting is Phase 2 of the Recognition Science electroweak scorecard, which compares the RS-native prediction sin²θ_W = (3-φ)/6 against the observed datum ≈0.2229. The upstream theorem sin2_theta_bounds states that sin²(θ_W) lies between 0.22 and 0.23 and proves it by unfolding the observed constant followed by constructor and norm_num.
proof idea
This is a one-line wrapper. The simpa tactic unfolds the codata definition row_sin2_thetaW_codata and directly applies the sin2_theta_bounds theorem from the WeinbergAngle module.
why it matters in Recognition Science
The bracket supplies the codata_in_ref_band field required by the downstream theorem weinbergAngleScoreCardCert_holds, which assembles the full scorecard certificate containing the codata band, the RS bracket, and the one-cent match. It thereby certifies the partial numerical bridge between the φ-based formula and the observed datum inside the Recognition Science framework. The residual open question remains rung-normalization and scheme dependence of the Weinberg angle.
scope and limits
- Does not prove equality between the RS prediction and the observed value.
- Does not address renormalization-scheme dependence of sin²θ_W.
- Does not incorporate higher-order radiative corrections.
- Does not derive the (3-φ)/6 formula from the forcing chain.
Lean usage
have codata_bound : (0.22 : ℝ) < row_sin2_thetaW_codata ∧ row_sin2_thetaW_codata < (0.23 : ℝ) := row_sin2_thetaW_codata_bracketformal statement (Lean)
34theorem row_sin2_thetaW_codata_bracket :
35 (0.22 : ℝ) < row_sin2_thetaW_codata ∧ row_sin2_thetaW_codata < (0.23 : ℝ) := by
proof body
One-line wrapper that applies simpa.
36 simpa [row_sin2_thetaW_codata] using WeinbergAngle.sin2_theta_bounds
37