Standard Model Weinberg Angle

The Weinberg angle

The Weinberg angle, written θ_W, is the parameter in the standard model of particle physics that fixes how the weak nuclear force and electromagnetism mix. It is not a directly measured quantity like a mass; it is extracted from experiments that compare the rates of weak and electromagnetic processes. The commonly quoted value is sin²(θ_W) ≈ 0.2229 at the Z boson mass scale, with a measurement error of about 0.0003, according to the Particle Data Group. The angle is fundamental because it determines the relative strengths of the two forces, and it runs, or changes slightly, with the energy at which it is measured. At very high energies, in grand unified theories, the value is predicted to be exactly 3/8, a simple rational number.

The standard model does not derive sin²(θ_W) from a deeper principle; it is an input parameter fixed by experiment. Recognition Science (RS) attempts to change that. The framework's machine-checked library of formal theorems contains a module that tries to derive the angle from the golden ratio φ, the number satisfying φ² = φ + 1, which is about 1.618. The module defines several candidate formulas, all built from φ. The one it calls its best prediction is sin²(θ_W) = (3 - φ)/6, which evaluates to about 0.230. The library proves, with a machine-checked theorem, that this value is within 0.01 of the observed 0.2229. The plain-language result is that a simple golden-ratio formula lands within about 3 percent of the measured value, with nothing fitted.

The module also includes a geometric picture. It defines an eight-tick structure, a discrete set of phases, and assigns three phases to the SU(2) sector and one to the U(1) sector. The mixing angle then emerges as a ratio of these phase counts, giving exactly 1/4 for the simple case. This is a definitional choice, a model, not a derivation. The framework also includes a running formula that starts from the grand unified value 3/8 and decreases with energy, and a falsifier structure that states the conditions under which the φ-based prediction would be wrong: if it deviates from observation by more than 5 percent, or if the running does not follow the predicted pattern.

In Recognition Science, the Weinberg angle is a hypothesis with a named falsifier, not a proved theorem. The library proves the arithmetic fact that (3 - φ)/6 is close to the observed value, but it does not prove that this formula is the unique consequence of the framework's axioms. The derivation status string in the module itself calls the result "promising," which is an honest summary. The gap between 0.230 and 0.2229 is real, about 0.007, and it is larger than the measurement error by a factor of more than twenty. The framework's contribution is a candidate structure, not a settled prediction.

/-- sin²(θ_W) in the ON-SHELL scheme: 1 − (M_W/M_Z)² with PDG 2024 masses
    (80.3692/91.1876)² → 0.22290. Corrected 2026-07-29: this definition was
    previously docstringed "MS-bar scheme", which was wrong. The MS-bar value
    at M_Z is 0.23121(4) (PDG 2024), and that is the anchor the predictions
    registry compares `(3−φ)/6` against. The two schemes differ by ≈ 0.008,
    far more than either uncertainty, so no comparison in this file or the
    registry is well-posed without naming which scheme it uses. -/
noncomputable def sin2ThetaW_observed : ℝ := 0.2229

theorem best_prediction_close_to_observed :
    |bestPrediction - sin2ThetaW_observed| < 0.01 := by
  unfold bestPrediction prediction3 sin2ThetaW_observed
  -- Need: |(3 - φ)/6 - 0.2229| < 0.01
  -- φ > 1.61 → (3 - φ)/6 < 1.39/6 = 0.2317
  -- φ < 1.62 → (3 - φ)/6 > 1.38/6 = 0.23
  have h_phi_gt : phi > 1.61 := phi_gt_onePointSixOne
  have h_phi_lt : phi < 1.62 := phi_lt_onePointSixTwo
  have h_pred_gt : (3 - phi) / 6 > 0.23 := by linarith
  have h_pred_lt : (3 - phi) / 6 < 0.232 := by linarith
  rw [abs_lt]
  constructor <;> linarith

/-- **THEOREM**: Simple geometric ratio gives sin²(θ_W) = 1/4 = 0.25.

    This is close but not exact. The correction comes from φ. -/
theorem simple_geometric_ratio : geometricMixing ⟨3, 1, 8⟩ = 1/4 := by
  unfold geometricMixing
  norm_num

/-- At the GUT scale (~10¹⁶ GeV), the couplings unify.

    sin²(θ_W)(GUT) = 3/8 = 0.375 (SU(5) prediction)

    The running from GUT to M_Z scale is:
    sin²(θ_W)(M_Z) ≈ 0.23

    RS explains both the GUT value AND the running! -/
noncomputable def sin2ThetaW_GUT : ℝ := 3/8

What this page does not claim

The framework does not prove that sin²(θ_W) must equal (3 - φ)/6; it only proves the arithmetic closeness to the observed value. The module does not derive the Weinberg angle from the framework's axioms; it defines candidate formulas and checks one against data.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/StandardModel/WeinbergAngle.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: