Prove2Me

W±=(W1∓iW2)/2W^\pm = (W_1 \mp iW_2)/\sqrt2

Proved
ElectroweakWiki.charged_boson_combination

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

electroweakmathematical-physics

For real field values W1,W2W_1, W_2 put W±=(W1∓iW2)/2W^\pm = (W_1 \mp iW_2)/\sqrt 2. Then

  1. W−=W+‾W^- = \overline{W^+};
  2. W1=(W++W−)/2W_1 = (W^+ + W^-)/\sqrt2;
  3. W2=i (W+−W−)/2W_2 = i\,(W^+ - W^-)/\sqrt2;
  4. W+W−=12(W12+W22)W^+W^- = \tfrac12(W_1^2+W_2^2).

So the charged fields carry the same information as W1,W2W_1, W_2, and W+W−W^+W^- is the real quadratic form that appears in the mass term mW2Wμ+W−μm_W^2 W^+_\mu W^{-\mu}.

Preamble
import Definitions.Def_ElectroweakWiki_defs
open Matrix
Formal statement
namespace ElectroweakWiki

theorem charged_boson_combination (W1 W2 : ℝ) :
    wMinus W1 W2 = (starRingEnd ℂ) (wPlus W1 W2) ∧
      (W1 : ℂ) = (wPlus W1 W2 + wMinus W1 W2) / (Real.sqrt 2 : ℂ) ∧
      (W2 : ℂ) = Complex.I * (wPlus W1 W2 - wMinus W1 W2) / (Real.sqrt 2 : ℂ) ∧
      wPlus W1 W2 * wMinus W1 W2 = (((W1 ^ 2 + W2 ^ 2) / 2 : ℝ) : ℂ) := 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 W1 and W2 bosons, in turn, combine to produce the charged massive bosons W±: W± = (W1 ∓ iW2)/√2' (p. 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 all real W1,W2W_1, W_2, with W+=(W1−iW2)/2W^+ = (W_1 - iW_2)/\sqrt2 and W−=(W1+iW2)/2W^- = (W_1+iW_2)/\sqrt2 (complex numbers, 2\sqrt2 the real square root viewed in C\mathbb C), the statement asserts the four equalities in C\mathbb C:

W−=W+‾,W1=W++W−2,W2=i(W+−W−)2,W+W−=W12+W222.W^- = \overline{W^+},\quad W_1 = \frac{W^++W^-}{\sqrt2},\quad W_2 = \frac{i(W^+-W^-)}{\sqrt2},\quad W^+W^- = \frac{W_1^2+W_2^2}{2}.

View graph