Standard Model Electroweak Mass Bridge

The mass bridge

The electroweak mass bridge is a formal result inside Recognition Science. It shows that the Standard Model's tree-level mass relations for the W and Z bosons follow from a single shared scale v and two positive gauge couplings g and g'. In plain terms, if you know the strength of the two interactions and the scale at which electroweak symmetry breaks, the masses of the heavy gauge bosons are determined. The module proves this in a machine-checked library of formal theorems, meaning every step is verified by a computer.

The Standard Model itself has long used these formulas. The W mass squared is g²v²/4, and the Z mass squared is (g² + g'²)v²/4. The ratio of the W mass to the Z mass equals the cosine of the Weinberg angle θ_W, defined by cos² θ_W = g²/(g² + g'²). The bridge formalizes these relations as theorems, not assumptions. It also proves that the W mass is always less than or equal to the Z mass when the couplings are positive, and that cos² θ_W lies strictly between zero and one.

What makes this a bridge is its conditional structure. The module does not derive the numerical values of g, g', or v from the Recognition Science substrate. Those remain empirical inputs. The bridge proves that if you supply those values, the Standard Model mass relations hold. This is a theorem about the logical structure, not a prediction of particle masses. The numerical calibration of the couplings from the framework is an open problem, tracked separately.

In Recognition Science, this bridge connects the framework's abstract cost and recognition substrate to a concrete piece of established physics. The framework models the universe as maintaining a discrete record of recognition events, and from that starting point it derives constants and scaling laws. The mass bridge shows that the electroweak sector's mass relations are compatible with that substrate, provided the scale v is identified with the recognition substrate's scale. That identification is a separate step, formalized in a companion module, and its numerical match to measured masses is an empirical check, not a theorem.

The practical consequence is that the Standard Model's electroweak mass formulas are not an independent postulate in this framework. They are consequences of a single scale and two couplings. A reader can now see that the framework does not contradict the Standard Model at tree level; it reproduces its mass relations as derived results. What remains open is the numerical origin of the couplings, which the framework does not yet explain.

/-- W boson mass squared: `m_W² = g² v² / 4`. -/
def mW_sq (g v : ℝ) : ℝ := g ^ 2 * v ^ 2 / 4

/-- Z boson mass squared: `m_Z² = (g² + g'²) v² / 4`. -/
def mZ_sq (g gp v : ℝ) : ℝ := (g ^ 2 + gp ^ 2) * v ^ 2 / 4

/-- The W/Z mass ratio identity in mass form (under positivity). -/
theorem mW_over_mZ_eq_cos_thetaW (g gp v : ℝ)
    (hg : 0 < g) (hgp : 0 ≤ gp) (hv : 0 < v) :
    mW g v / mZ g gp v = Real.sqrt (cos_sq_thetaW_SM g gp) := by
  unfold mW mZ
  have hmW_sq_pos : 0 < mW_sq g v := by
    unfold mW_sq; positivity
  have hmZ_sq_pos : 0 < mZ_sq g gp v := by
    unfold mZ_sq
    have hg2 : 0 < g ^ 2 := by positivity
    have hgp2 : 0 ≤ gp ^ 2 := sq_nonneg _
    have hsum : 0 < g ^ 2 + gp ^ 2 := by linarith
    have hv2 : 0 < v ^ 2 := by positivity
    positivity
  -- Use Real.sqrt_div_sqrt-style identity via Real.sqrt_div'
  have hmW_nn : 0 ≤ mW_sq g v := le_of_lt hmW_sq_pos
  have hmZ_nn : 0 ≤ mZ_sq g gp v := le_of_lt hmZ_sq_pos
  rw [← Real.sqrt_div hmW_nn]
  congr 1
  exact mW_over_mZ_sq_eq_cos_sq g gp v hg hv

/-- The Z is heavier than (or equal to) the W in mass-squared. -/
theorem mZ_sq_ge_mW_sq (g gp v : ℝ) : mW_sq g v ≤ mZ_sq g gp v :=
  mW_sq_le_mZ_sq g gp v

/-- `cos²θ_W ∈ (0, 1]` for any nontrivial gauge coupling pair. -/
theorem cos_sq_thetaW_in_unit_interval (g gp : ℝ) (hg : 0 < g) :
    0 < cos_sq_thetaW_SM g gp ∧ cos_sq_thetaW_SM g gp ≤ 1 := by
  unfold cos_sq_thetaW_SM
  have hg2 : 0 < g ^ 2 := by positivity
  have hgp2 : 0 ≤ gp ^ 2 := sq_nonneg _
  have hsum_pos : 0 < g ^ 2 + gp ^ 2 := by linarith
  refine ⟨?_, ?_⟩
  · exact div_pos hg2 hsum_pos
  · rw [div_le_one hsum_pos]; linarith

What this page does not claim

The numerical values of g, g', and v are derived from the framework; they remain empirical inputs. The framework predicts the measured W and Z masses; it only proves the relations conditional on those inputs. The mass bridge derives the Weinberg angle from first principles; it only proves the SM definition's relation.

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