Chapter ParityZ4

import Definitions.Def_ChapterA3
import Definitions.Def_ChapterParity
import Definitions.Def_ChapterParityQL
import Mathlib


/-!
# Chapter "On the physical parity transformation and antiparticles" — the combined `ℤ₄`
background-symmetry generator

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 states that, promoting the CKM matrix to a background field, the electroweak
Lagrangian is invariant under a background symmetry
`SU(2)_L × (SU(3)_C × U(1)_Y) ⋊ Z₄`, **where the `Z₄` group is generated by the (single)
generalized parity-reversal transformation** acting *simultaneously* on all fields:

* Higgs doublet:  `φ(t,x⃗) ↦ i σ₂ φ(t,-x⃗)`               — internal part `higgsParity = i σ₂`;
* left-handed quark doublet: `Q_L(t,x⃗) ↦ -σ₂ γ⁰ Q_L(t,-x⃗)` — internal part `QLParity = -(σ₂⊗iγ⁰)`;
* right-handed quarks:  `u_R, d_R ↦ i γ⁰ …(t,-x⃗)`        — internal part `mgamma 0 = i γ⁰`.

The individual internal parts were each shown to be order four in `ChapterParity`
(`higgsParity_order_four`, `fermionParity_order_four`) and `ChapterParityQL`
(`QLParity_order_four`).  Here we assemble them into the **single** operator that the
book says generates the `Z_4` factor, and prove that this combined generator has order
*exactly* four as an element of the (product) monoid of the field-space endomorphisms:
`P² ≠ 1` while `P⁴ = 1`, i.e. `orderOf P = 4`.  This is the precise sense in which the
one parity transformation generates a cyclic group `ℤ₄ = ℤ/4ℤ`.

The surrounding physics (the full background gauge group and its semidirect structure)
is left as prose, matching the neighbouring parity files.

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

open Matrix

namespace BookProof.ChapterParityZ4

open BookProof.ChapterParity
open BookProof.ChapterParityQL
open BookProof.ChapterA3

/-- The internal part of the field space on which the combined electroweak parity acts:
the Higgs doublet `ℂ²`, the left-handed quark doublet `ℂ²⊗ℂ⁴ ≅ ℂ⁸`, and the two
right-handed quarks `u_R`, `d_R`, each `ℂ⁴`.  We package the four endomorphisms as a
single element of the product monoid. -/
abbrev FieldOps :=
  Matrix (Fin 2) (Fin 2) ℂ × Matrix (Fin 2 × Fin 4) (Fin 2 × Fin 4) ℂ ×
    Matrix (Fin 4) (Fin 4) ℂ × Matrix (Fin 4) (Fin 4) ℂ

/-- The single generalized-parity generator of the book's `Z_4` background symmetry,
acting simultaneously on `(φ, Q_L, u_R, d_R)`. -/
noncomputable def combinedParity : FieldOps :=
  (higgsParity, QLParity, mgamma 0, mgamma 0)

/-
The square of the combined parity is `(-1, -1, -1, -1)`: on every field the parity
squares to `-1` (the invariant selecting the double cover `Pin(3,1)`).
-/










end BookProof.ChapterParityZ4