Registry · Theorem IV.T145 tau-effective formalized

IV.T145 — Uniqueness: C_tau = sigma (lobe-swap uniquely determines C)

sigma swaps chi_plus <-> chi_minus characters (proved in Characters.lean: sigma_swaps_chi_plus, sigma_swaps_chi_minus). This is precisely what charge conjugation must do to reverse U(1)-holonomy charge. Combined with uniqueness of the lobe-swap involution (I.D18), this proves C_tau = sigma. Verified numerically: chi_plus(sigma(z)) = chi_minus(z) for all SplitComplex z.

Book IV Part 3 Ch. 24

Dependency Graph

Depends on (2)

Depended on by (3)

Lean Formalization

Module: TauLib.BookIV.Electroweak.MajoranaStructure

Symbol: sigma_is_charge_conjugation