Chapter ParityHypercharge

import Definitions.Def_ChapterA3
import Definitions.Def_ChapterParity
import Mathlib


/-!
# Chapter "On the physical parity transformation and antiparticles" — the `U(1)_Y`
one-parameter group generated by `iγ⁵`

This file continues the finite algebraic core of the `book.tex` chapter *"On the physical
parity transformation and antiparticles"* (`book.tex` line ~7522, §"Majorana spinors in
the Standard Model").  The chapter's distinguishing feature of the hypercharge gauge group
is that

  *"the generator of the gauge group `U(1)_Y` is `iγ⁵`",*

and that the color triplet / hypercharge phases are taken *"with the imaginary unit
replaced by `iγ⁵`"*.  Concretely `Q_L → e^{iγ⁵ ϑ/6} Q_L`, `u_R → e^{-iγ⁵ 2ϑ/3} u_R`, i.e.
the `U(1)_Y` phase `e^{iγ⁵ Y ϑ}` is generated by `iγ⁵`.

In the concrete real Majorana model of `ChapterA3` the matrix `iγ⁵ = mgamma5` is a genuine
**real matrix** (integer entries) with `(iγ⁵)² = -1` (`ChapterA3.mgamma5_sq`): it is a
*real* complex structure, which is exactly the book's point — at the quantum level the
imaginary unit is realized by the real matrix `iγ⁵`.

Because `J := iγ⁵` satisfies `J² = -1`, the one-parameter `U(1)_Y` phase group has the
closed form

  `e^{ϑ J} = cos ϑ · 1 + sin ϑ · J`,

which we take as the definition `hyperPhase ϑ` and prove is a one-parameter group
`ℝ → GL` (`hyperPhase_zero`, `hyperPhase_add`, `hyperPhase_neg_mul`) generated by `iγ⁵`.

## Contents

* `mgamma5_real` : `iγ⁵` is represented by a real matrix (`conj(iγ⁵) = iγ⁵`) — "the
  imaginary unit replaced by `iγ⁵`".
* `hyperPhase` : the `U(1)_Y` phase `e^{ϑ iγ⁵} = cos ϑ · 1 + sin ϑ · iγ⁵`.
* `hyperPhase_zero` : `hyperPhase 0 = 1`.
* `hyperPhase_add` : `hyperPhase ϑ · hyperPhase φ = hyperPhase (ϑ + φ)` — the abelian
  `U(1)_Y` group law.
* `hyperPhase_neg_mul` : `hyperPhase ϑ · hyperPhase (-ϑ) = 1` — every phase is invertible.
* `hyperPhase_comm` : `hyperPhase ϑ` commutes with its generator `iγ⁵`.

The surrounding physical modelling (the Standard-Model gauge structure, the hypercharge
assignments of the individual fermion multiplets) is left as prose.

Everything is `sorry`-free and `axiom`-free (only `propext`, `Classical.choice`,
`Quot.sound`).
-/

open Matrix
open scoped ComplexConjugate

namespace BookProof.ChapterParityHypercharge

open BookProof.ChapterA3



/-- The `U(1)_Y` phase group `e^{ϑ iγ⁵}`, in the closed form given by `(iγ⁵)² = -1`:
`hyperPhase ϑ = cos ϑ · 1 + sin ϑ · iγ⁵`. -/
noncomputable def hyperPhase (θ : ℝ) : Matrix (Fin 4) (Fin 4) ℂ :=
  (Real.cos θ : ℂ) • (1 : Matrix (Fin 4) (Fin 4) ℂ) + (Real.sin θ : ℂ) • mgamma5









end BookProof.ChapterParityHypercharge