Prove2Me

(γ,Z0)(\gamma, Z^0) is a rotation of (B,W3)(B, W_3)

Proved
ElectroweakWiki.neutral_rotation_inverse

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

electroweakmathematical-physics

For every angle θ\theta and real field values B,W3B, W_3, put

(γZ0)=(cos⁡θsin⁡θ−sin⁡θcos⁡θ)(BW3).\begin{pmatrix}\gamma\\ Z^0\end{pmatrix} = \begin{pmatrix}\cos\theta & \sin\theta\\ -\sin\theta & \cos\theta\end{pmatrix}\begin{pmatrix}B\\ W_3\end{pmatrix}.

Then the transformation is inverted by the transposed matrix, B=cos⁡θ γ−sin⁡θ Z0B = \cos\theta\,\gamma - \sin\theta\, Z^0 and W3=sin⁡θ γ+cos⁡θ Z0W_3 = \sin\theta\,\gamma + \cos\theta\,Z^0, and it preserves the sum of squares: γ2+(Z0)2=B2+W32\gamma^2 + (Z^0)^2 = B^2 + W_3^2.

This is the precise content of the article's remark that "the axes representing the particles have essentially just been rotated, in the (W3,B)(W_3, B) plane, by the angle θW\theta_W".

Preamble
import Definitions.Def_ElectroweakWiki_defs
open Matrix
Formal statement
namespace ElectroweakWiki

theorem neutral_rotation_inverse (θ B W3 : ℝ) :
    B = Real.cos θ * photonField θ B W3 - Real.sin θ * zField θ B W3 ∧
      W3 = Real.sin θ * photonField θ B W3 + Real.cos θ * zField θ B W3 ∧
      photonField θ B W3 ^ 2 + zField θ B W3 ^ 2 = B ^ 2 + W3 ^ 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, matrix equation for (γ, Z0) and the sentence 'The axes representing the particles have essentially just been rotated, in the (W3, B) plane, by the angle θw' (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 numbers θ,B,W3\theta, B, W_3, with γ=cos⁡θ B+sin⁡θ W3\gamma = \cos\theta\,B+\sin\theta\,W_3 and Z=−sin⁡θ B+cos⁡θ W3Z = -\sin\theta\,B+\cos\theta\,W_3, the statement asserts the three equalities

B=cos⁡θ γ−sin⁡θ Z,W3=sin⁡θ γ+cos⁡θ Z,γ2+Z2=B2+W32.B = \cos\theta\,\gamma - \sin\theta\,Z,\qquad W_3 = \sin\theta\,\gamma+\cos\theta\,Z,\qquad \gamma^2+Z^2 = B^2+W_3^2.

There is no hypothesis on θ\theta.

View graph