sin2ThetaW_observed
The declaration supplies the measured value of the weak mixing angle squared equal to 0.2229 at the Z mass scale in the MS-bar scheme. Particle physicists and Recognition Science model builders cite it when comparing phi-derived predictions against electroweak data. It is introduced as a direct numeric definition without further computation.
claimThe observed value of $sin^2 theta_W$ at the Z-boson mass scale in the MS-bar scheme equals 0.2229.
background
Recognition Science derives the Weinberg angle from eight-tick phase geometry, where electroweak mixing arises as an embedding angle optimized by the self-similar fixed point phi. The module targets this value to fix the relative strengths of electromagnetic and weak forces via the phi-ladder structure.
proof idea
The definition is a direct numeric assignment of the constant 0.2229. No lemmas are applied.
why it matters in Recognition Science
This definition anchors experimental comparison in the WeinbergAngle module. It feeds the theorem best_prediction_close_to_observed, which verifies the best phi-based prediction lies within 0.01, and the bounds theorem establishing the interval 0.22 to 0.23. It realizes the SM-004 target of obtaining the weak mixing angle from phi-structure and the eight-tick octave.
scope and limits
- Does not derive the numerical value from the Recognition functional equation.
- Does not attach an uncertainty interval using the Uncertainty type.
- Does not specify renormalization details beyond the module context.
- Does not connect to J-cost, defectDist, or mass-ladder formulas.
Lean usage
theorem bounds_check : sin2ThetaW_observed > 0.22 ∧ sin2ThetaW_observed < 0.23 := by unfold sin2ThetaW_observed; constructor <;> norm_numformal statement (Lean)
39noncomputable def sin2ThetaW_observed : ℝ := 0.2229
proof body
Definition body.
40
41/-- Uncertainty in sin²(θ_W). -/