Masses Electroweak Masses Sin2 Theta Positive

The Weinberg angle in RS

The Weinberg angle, usually written θ_W, is the parameter in the standard model of particle physics that mixes the electromagnetic and weak forces. It controls the mass ratio of the W and Z bosons: m_W = m_Z cos θ_W. Its squared sine, sin²θ_W, is measured to be about 0.231, and it is one of the quantities the standard model does not predict from first principles; experiment fixes it.

Recognition Science (RS) proposes a fixed value: sin²θ_W = (3 − φ)/6, where φ is the golden ratio, about 1.618. This is a definitional choice, tagged MODEL, not a derived theorem. The number is about 0.2302, close to the measured value. The declaration sin2_theta_positive proves a narrower statement: that this proposed value is greater than zero. The proof uses the fact that φ is less than 2, so (3 − φ) is positive. A companion theorem proves sin²θ_W is also less than 1/2. These are THEOREM claims: machine-checked facts about the defined number, not about the physical world.

What sin2_theta_positive does not claim is as important as what it proves. It does not claim the RS value matches the measured Weinberg angle to any precision; that comparison is an empirical check, not a theorem. It does not claim the Weinberg angle is derived from the framework's forcing chain; the value is an identification, a choice of how to embed gauge geometry into the framework's rung structure. It does not claim the standard model is wrong or incomplete; RS treats the standard model as itself derivable from recognition principles.

The practical consequence is modest but real: within RS, the Weinberg angle is not a free parameter. It is fixed by the golden ratio, the same constant that appears throughout the framework's mass ladder. The positivity proof is a sanity check, ensuring the proposed value is physically admissible before any comparison to experiment is made.

theorem sin2_theta_positive : 0 < sin2_theta_W_rs := by
  unfold sin2_theta_W_rs
  have hphi : Constants.phi < 2 := by
    rw [phi_eq_goldenRatio]; exact Real.goldenRatio_lt_two
  linarith

noncomputable def sin2_theta_W_rs : ℝ := (3 - Constants.phi) / 6

theorem sin2_theta_lt_half : sin2_theta_W_rs < 1/2 := by
  unfold sin2_theta_W_rs
  have hphi : 0 < Constants.phi := phi_pos
  linarith

noncomputable def w_pred : ℝ := z_pred * cos_theta_W_rs

What this page does not claim

The RS value of sin²θ_W is not claimed to match the measured value to any stated precision. The Weinberg angle is not claimed to be derived from the framework's forcing chain; it is an identification. The standard model is not claimed to be incorrect or incomplete.

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/Masses/ElectroweakMasses.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: