$Q = T_3 + \frac12 Y$ does not couple to the Higgs vacuum

Proved

ElectroweakWiki.electric_charge_unbroken

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

electroweakmathematical-physics

Let $v\neq 0$ and $h_0 = (0, v/\sqrt2)$ . On the Higgs doublet (hypercharge $Y=1$ , isospin $T_3 = \sigma_3/2$ ) the combination $aT_3 + bY/2$ acts as the matrix $\frac a2\sigma_3 + \frac b2\mathbb 1$ . Then

the charge generator $Q = T_3 + \frac12 Y$ (that is $a=b=1$ ) annihilates $h_0$ ;
the lower component of the doublet has charge $Q(-\tfrac12, 1) = -\tfrac12 + \tfrac12 = 0$ ;
for real $a, b$ , the generator $aT_3 + bY/2$ annihilates $h_0$ if and only if $a = b$ .

So, up to scale, $Q$ is the only combination of $T_3$ and $Y$ that does not couple to the vacuum; any other combination acts nontrivially on it. This is the sense in which $\mathrm U(1)_{em}$ is unbroken.

Preamble

import Definitions.Def_ElectroweakWiki_defs
open Matrix

Formal statement

namespace ElectroweakWiki

theorem electric_charge_unbroken (v : ℝ) (hv : v ≠ 0) :
    isospinHyperchargeGenerator 1 1 *ᵥ higgsVacuum v = 0 ∧
      electricCharge (-1 / 2) 1 = 0 ∧
      (∀ a b : ℝ, isospinHyperchargeGenerator a b *ᵥ higgsVacuum v = 0 ↔ a = b) := by sorry

end ElectroweakWiki

Source

Wikipedia, "Electroweak interaction", revision oldid=1360331872, https://en.wikipedia.org/w/index.php?title=Electroweak_interaction&oldid=1360331872; Section Formulation, 'The electric charge arises as the particular linear combination (nontrivial) of YW and T3 (Q = T3 + ½YW) that does not couple to the Higgs boson ... while any other combination of the hypercharge and the weak isospin must interact with the Higgs' and 'U(1)em ... is unbroken' (pp. 2–3 of the PDF)

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 every real $v$ with $v\neq0$ , with $h_0 = (0, v/\sqrt2)\in\mathbb C^2$ and $G(a,b) = \frac a2\sigma_3 + \frac b2 I = \mathrm{diag}\big(\frac{a+b}{2}, \frac{b-a}{2}\big)$ , the statement asserts: $G(1,1)h_0 = 0$ ; $-\frac12 + \frac12\cdot 1 = 0$ ; and for all real $a, b$ , $G(a,b)h_0 = 0$ if and only if $a=b$ .

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Q=T3+12YQ = T_3 + \frac12 YQ=T3​+21​Y does not couple to the Higgs vacuum

$Q = T_3 + \frac12 Y$ does not couple to the Higgs vacuum