row_sin2_thetaW_codata
This definition supplies the PDG-style reference value 0.2229 for sin²θ_W at the Z mass in the MS-bar scheme. Scorecard proofs and the certification structure cite it to bound the observed value and to test the one-cent match against the RS prediction. The body is a direct alias to the upstream constant sin2ThetaW_observed.
claimLet $s_W^2$ denote the observed value of the Weinberg angle squared at the Z-boson mass scale in the MS-bar scheme, with numerical value $0.2229$.
background
The module implements Phase 2 of the electroweak scorecard, comparing the RS core prediction sin²θ_W = (3-φ)/6 against a PDG-style reference. The upstream definition sin2ThetaW_observed supplies the numerical anchor 0.2229 together with a note on its uncertainty. This observed constant is the codata input that the scorecard uses to certify the partial bridge between the phi-derived formula and experiment.
proof idea
The definition is a one-line alias to the upstream constant sin2ThetaW_observed. No tactics or reductions are applied.
why it matters in Recognition Science
It supplies the codata field to the WeinbergAngleScoreCardCert structure and is referenced by the bracket theorem and the best-prediction match theorem. The declaration anchors the observed side of the |bestPrediction - observed| < 0.01 test that forms the partial bridge in the electroweak sector. It touches the open question of scheme dependence and rung normalization left unresolved by the current reference number.
scope and limits
- Does not derive the numerical value from the RS forcing chain or J-cost.
- Does not resolve renormalization-scheme or scale ambiguities.
- Does not incorporate higher-order radiative corrections.
- Does not claim exact numerical equality to the RS prediction (3-φ)/6.
formal statement (Lean)
32def row_sin2_thetaW_codata : ℝ := WeinbergAngle.sin2ThetaW_observed
proof body
Definition body.
33