Standard Model Weak Coupling

Weak coupling in the standard model

In the standard model of particle physics, the weak nuclear force is responsible for radioactive decay and for the nuclear reactions that power the Sun. Its strength is described by a quantity called the weak coupling constant, usually written α_W. Unlike the fine-structure constant α, which measures the strength of electromagnetism, α_W is not a single number: it changes with the energy of the interaction, a property called running. At low energies, the weak force appears much weaker than electromagnetism, but at high energies, the two forces become comparable in strength. This running behavior is a central feature of the electroweak theory, which unifies the weak force with electromagnetism.

The standard model connects α_W to α through the weak mixing angle θ_W, also called the Weinberg angle. The tree-level identity is α = α_W · sin²θ_W, which means α_W = α / sin²θ_W. Since sin²θ_W is always less than 1, this identity shows that α_W is always larger than α. The weak mixing angle is itself a fundamental parameter of the standard model, measured experimentally to high precision. Its value determines how much the Z boson, the carrier of the weak neutral current, mixes with the photon.

In Recognition Science, a framework that derives physical constants from a small set of axioms about how a system tracks its own states, this identity takes on a specific form. The framework models the weak mixing angle as sin²θ_W = (3 − φ)/6, where φ is the golden ratio (1.618...). This value is about 0.2309, which falls within the experimentally measured range for sin²θ_W at the Z boson mass scale. The framework also has a construction for α, based on a seed value of 44π, but the exact value of α is treated as a free boundary condition, not a derived constant.

The module in the framework's machine-checked library of formal theorems defines α_W as α divided by sin²θ_W and proves three structural facts. First, α_W is positive. Second, α_W is greater than α. Third, α_W is greater than twice α, because sin²θ_W is less than 1/2. These are formal theorems, checked by a computer, and they hold for any positive α. The module does not claim to derive the measured value of α_W from first principles, because the input α is a construction-band object, not a parameter-free derivation.

The practical lesson is that α_W is not an independent constant: it is tied to α and to the weak mixing angle. The framework's contribution is to show that the weak mixing angle has a simple geometric origin, involving the golden ratio, and that the structural relationships between the couplings follow from this. The measured value of α_W remains an experimental fact, but the framework provides a possible explanation for why the weak mixing angle takes the value it does.

/-- The weak coupling constant α_W = α / sin²θ_W.
    From the tree-level electroweak identity: α_EM = α_W · sin²θ_W,
    so α_W = α_EM / sin²θ_W. -/
def alpha_W : ℝ := alpha / sin2_theta_W_rs

/-- sin²θ_W > 0 (needed for division). -/
theorem sin2_pos : 0 < sin2_theta_W_rs := sin2_theta_positive

/-- α_W is positive (both α and sin²θ_W are positive). -/
theorem alpha_W_pos : 0 < alpha_W := by
  unfold alpha_W
  exact div_pos alpha_pos_aux sin2_theta_positive

/-- α_W > α (since sin²θ_W < 1, dividing by it increases α). -/
theorem alpha_W_gt_alpha : alpha < alpha_W := by
  unfold alpha_W
  rw [lt_div_iff₀ sin2_theta_positive]
  calc alpha * sin2_theta_W_rs
      < alpha * 1 := by {
        apply mul_lt_mul_of_pos_left _ alpha_pos_aux
        linarith [sin2_theta_lt_half]
      }
    _ = alpha := mul_one _

/-- α_W > 2α (since sin²θ_W < 1/2). -/
theorem alpha_W_gt_two_alpha : 2 * alpha < alpha_W := by
  unfold alpha_W
  rw [lt_div_iff₀ sin2_theta_positive]
  calc 2 * alpha * sin2_theta_W_rs
      < 2 * alpha * (1/2) := by {
        apply mul_lt_mul_of_pos_left sin2_lt_half
        exact mul_pos (by norm_num) alpha_pos_aux
      }
    _ = alpha := by ring

What this page does not claim

This answer does not claim that the framework derives the measured value of α_W from first principles. This answer does not claim that the framework's value for α is a parameter-free derivation. This answer does not claim that the weak mixing angle is exactly (3 − φ)/6 in the standard model.

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/WeakCoupling.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: