$e = g\sin\theta_W = g'\cos\theta_W$

Proved

ElectroweakWiki.elemCharge_eq_g_sin_eq_gp_cos

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

electroweakmathematical-physics

Let $g>0$ , $g'>0$ , $\theta_W = \arctan(g'/g)$ , and let $e = gg'/\sqrt{g^2+g'^2}$ be the electromagnetic coupling (the altitude of the Weinberg triangle). Then

e = g\sin\theta_W = g'\cos\theta_W.

This is the relation quoted in the article under the neutral-current Lagrangian $\mathcal L_N$ , and it identifies the coupling of the photon.

Preamble

import Definitions.Def_ElectroweakWiki_defs
open Matrix

Formal statement

namespace ElectroweakWiki

theorem elemCharge_eq_g_sin_eq_gp_cos (g g' : ℝ) (hg : 0 < g) (hg' : 0 < g') :
    elemCharge g g' = g * Real.sin (weinbergAngle g g') ∧
      elemCharge g g' = g' * Real.cos (weinbergAngle g g') := by sorry

end ElectroweakWiki

Source

Wikipedia, "Electroweak interaction", revision oldid=1360331872, https://en.wikipedia.org/w/index.php?title=Electroweak_interaction&oldid=1360331872; Section 'After electroweak symmetry breaking', text below L_N: 'where e = g sin θW = g′ cos θW' (p. 5 of the PDF); also the Weinberg-angle figure (p. 2)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted these Lean statements (at the explicit direction of the proposal's owner), not by an independent blind auditor. The author knew the intended meaning while writing it, so it must not be mistaken for independent testimony; reviewers should check it against the Lean code themselves.

For all real $g, g'$ with $g>0$ and $g'>0$ , writing $\theta = \arctan(g'/g)$ and $e = gg'/\sqrt{g^2+g'^2}$ , the statement asserts both $e = g\sin\theta$ and $e = g'\cos\theta$ .

View graph

e=gsin⁡θW=g′cos⁡θWe = g\sin\theta_W = g'\cos\theta_We=gsinθW​=g′cosθW​

$e = g\sin\theta_W = g'\cos\theta_W$