Prove2Me

Neutral-current couplings: eQ A+gcos⁡θW(T3−sin⁡2θWQ)ZeQ\,A + \frac{g}{\cos\theta_W}(T_3 - \sin^2\theta_W Q)Z

Proved
ElectroweakWiki.neutral_current_coupling

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

electroweakmathematical-physics

Let g>0g>0, g′>0g'>0, θW=arctan⁡(g′/g)\theta_W = \arctan(g'/g) and e=gg′/g2+g′2e = gg'/\sqrt{g^2+g'^2}. For a fermion with isospin component T3T_3 and hypercharge YY, let Q=T3+Y/2Q = T_3 + Y/2. For real field values B,W3B, W_3 let A=cos⁡θWB+sin⁡θWW3A = \cos\theta_W B + \sin\theta_W W_3 (photon) and Z=−sin⁡θWB+cos⁡θWW3Z = -\sin\theta_W B + \cos\theta_W W_3. Then

g T3 W3+g′ Y2 B=e Q A+gcos⁡θW(T3−sin⁡2θW Q)Z.g\,T_3\,W_3 + g'\,\frac Y2\,B = e\,Q\,A + \frac{g}{\cos\theta_W}\left(T_3 - \sin^2\theta_W\, Q\right) Z.

The left side is the neutral part of the gauge coupling in the covariant derivative DμD_\mu; the right side gives the couplings of AA and ZZ that appear in LN=eJμemAμ+gcos⁡θW(Jμ3−sin⁡2θWJμem)Zμ\mathcal L_N = eJ^{em}_\mu A^\mu + \frac{g}{\cos\theta_W}(J^3_\mu - \sin^2\theta_W J^{em}_\mu)Z^\mu.

Preamble
import Definitions.Def_ElectroweakWiki_defs
open Matrix
Formal statement
namespace ElectroweakWiki

theorem neutral_current_coupling (g g' T3 Y B W3 : ℝ) (hg : 0 < g) (hg' : 0 < g') :
    g * T3 * W3 + g' * (Y / 2) * B =
      elemCharge g g' * electricCharge T3 Y * photonField (weinbergAngle g g') B W3 +
        g / Real.cos (weinbergAngle g g') *
          (T3 - Real.sin (weinbergAngle g g') ^ 2 * electricCharge T3 Y) *
            zField (weinbergAngle g g') B W3 := 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', neutral current Lagrangian L_N (p. 5 of the PDF), with the covariant derivative D_μ of p. 4
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′,T3,Y,B,W3g, g', T_3, Y, B, W_3 with g>0g>0 and g′>0g'>0, writing θ=arctan⁡(g′/g)\theta = \arctan(g'/g), e=gg′/g2+g′2e = gg'/\sqrt{g^2+g'^2}, Q=T3+Y/2Q = T_3 + Y/2, A=cos⁡θ B+sin⁡θ W3A = \cos\theta\,B+\sin\theta\,W_3 and Z=−sin⁡θ B+cos⁡θ W3Z = -\sin\theta\,B+\cos\theta\,W_3, the statement asserts the real identity

gT3W3+g′Y2B=eQA+gcos⁡θ (T3−sin⁡2θ Q) Z.gT_3W_3 + g'\frac{Y}{2}B = eQA + \frac{g}{\cos\theta}\,(T_3 - \sin^2\theta\,Q)\,Z.
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