Keys/Dirac.lean — FrcMathlib

1import FrcMathlib.Theme.Dirac23/-!4# FrcMathlib.Keys.Dirac — the keyed theorems of the dirac theme (ledger migration, task LM19)56One declaration per key, `FRC.LedgerML.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem7that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration8`FRC.<Module>.p<key>` as an alias. Every declaration has the axioms of Mathlib's hierarchy at most (`check_axioms.py`).9-/1011namespace FRC.LedgerML1213-- Keys of the dirac theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)14/-- p08008 — 8:B2. The class is the datum: the nonsquares form one square class, and the Lorentzian form depends on its coefficient through that class alone. -/15theorem p08008 : (∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {a b : ZMod p}, a ≠ (0 : ZMod p) → b ≠ (0 : ZMod p) → ¬IsSquare a → ¬IsSquare b → IsSquare (a * b)) ∧ ∀ {K : Type u_1} [CommRing K] (ν m x₀ x₁ x₂ x₃ : K), -(m ^ (2 : ℕ) * ν) * x₀ ^ (2 : ℕ) + x₁ ^ (2 : ℕ) + x₂ ^ (2 : ℕ) + x₃ ^ (2 : ℕ) = -ν * (m * x₀) ^ (2 : ℕ) + x₁ ^ (2 : ℕ) + x₂ ^ (2 : ℕ) + x₃ ^ (2 : ℕ) :=16  And.intro @FRC.DiracML.class_datum (@FRC.DiracML.form_class)17/-- p08009 — 8:B3. The drive is canonical: the drive multiplier is a nonsquare on every shell and the only named residue that is one on every symmetry-complete shell; the classes of $2$, $2^{-1}$, $-2$, $\pi=-2^{-1}$ and $\im$ are fixed by the parity of $\kap$, that of $e$ by no rule; the reframing flip keeps the class. Decided on $\p<2000$. -/18theorem p08009 : (∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {g : ZMod p}, orderOf g = p - (1 : ℕ) → p % (2 : ℕ) = (1 : ℕ) → ¬IsSquare g ∧ ¬IsSquare g⁻¹) ∧ (∀ (κ : ℕ) [hp' : Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] {g : ZMod ((4 : ℕ) * κ + (1 : ℕ))}, orderOf g = (4 : ℕ) * κ → (IsSquare (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ↔ Even κ) ∧ (IsSquare (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ↔ Even κ) ∧ (IsSquare (-2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ↔ Even κ) ∧ (IsSquare (g ^ ((3 : ℕ) * κ)) ↔ Even κ) ∧ g ^ ((3 : ℕ) * κ) = -g ^ κ ∧ IsSquare (-1 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))) ∧ FRC.DiracML.Aent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (10 : ZMod (13 : ℕ)) ∧ FRC.DiracML.Bent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (2 : ZMod (13 : ℕ)) ∧ (10 : ZMod (13 : ℕ)) ^ (2 : ℕ) - (2 : ZMod (13 : ℕ)) * (2 : ZMod (13 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) * (7 : ZMod (13 : ℕ)) = (1 : ZMod (13 : ℕ)) ∧ ¬IsSquare (7 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (5 : ℕ) = (6 : ZMod (13 : ℕ)) ∧ ¬IsSquare (6 : ZMod (13 : ℕ)) ∧ orderOf (2 : ZMod (13 : ℕ)) = (12 : ℕ) :=19  And.intro @FRC.DiracML.drive_nonsquare (And.intro @FRC.DiracML.named_residues (@FRC.DiracML.shell13))20/-- p08011 — 8:B5. The square class is chronon parity: the squares are the even drive steps, a residue's class the parity of its drive-step count; on $\kap$-even shells the whole quarter-turn group is square, so the order-four chart grading carries no signature. Decided on every primitive root of $\F_{13}$ and $\F_{173}$ and on $\p<2000$. -/21theorem p08011 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {g : ZMod p}, orderOf g = p - (1 : ℕ) → p % (2 : ℕ) = (1 : ℕ) → ∀ (k : ℕ), IsSquare (g ^ k) ↔ Even k :=22  @FRC.DiracML.parity_iff23/-- p08012 — 8:B6. Norm growth and parity: one chronon of drive scales every Frobenius norm by the square $g^2$; the single-chronon multiplier is odd and has no square root in $\Fp$; the flip $g\mapsto g^{-1}$ preserves the parity class. -/24theorem p08012 : (∀ {K : Type u_1} [Field K] {ν : K} (g : K) (z : FRC.Extension.Ext K ν), (FRC.Extension.Ext.ofBase g * z).norm = g ^ (2 : ℕ) * z.norm) ∧ ∀ {F : Type u_2} [CommRing F] {ν : F} (z z' : FRC.DiracML.Ext F ν), (z * z').norm = z.norm * z'.norm :=25  And.intro @FRC.DiracML.norm_growth (@FRC.DiracML.Ext.norm_mul)26/-- p08013 — 8:B7. Signature lives on $\Fp$: the Euclidean form is hyperbolic and $Q_\nu$ elliptic, with the zero counts of the two classes on every symmetry-complete shell below $60$; over $K$ every element of $\Fp$ is a square and the dichotomy collapses. -/27theorem p08013 : ∀ {p : Nat} [hp : Fact (Nat.Prime p)] {ν : ZMod p}, Not (@IsSquare (ZMod p) (@Distrib.toMul (ZMod p) (@instDistribOfSemiring (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) ν) → ∀ (a : ZMod p), @IsSquare (FRC.Extension.Ext (ZMod p) ν) (@FRC.Extension.Ext.instMul (ZMod p) (ZMod.commRing p) ν) (@FRC.Extension.Ext.ofBase (ZMod p) (ZMod.commRing p) ν a) :=28  @FRC.DiracML.ext_square29/-- p08016 — 8:C2. The form is Hermitian and nondegenerate. -/30theorem p08016 : (∀ {K : Type u_1} [CommRing K] [StarRing K] {X : Type u_2} [Fintype X] (ψ φ : X → K), star (FRC.DiracML.herm ψ φ) = FRC.DiracML.herm φ ψ) ∧ ∀ {K : Type u_3} [CommRing K] [StarRing K] {X : Type u_4} [Fintype X] [DecidableEq X] (ψ : X → K), (∀ (φ : X → K), FRC.DiracML.herm ψ φ = (0 : K)) → ψ = (0 : X → K) :=31  And.intro @FRC.DiracML.herm_star (@FRC.DiracML.herm_nondegenerate)32/-- p08018 — 8:C4. Exact Hermitian preservation: for a self-adjoint Hamiltonian and an admissible parameter the Cayley step is unitary. -/33theorem p08018 : ∀ {R : Type u_1} [Ring R] (σ : R → R), (∀ (x y : R), σ (x * y) = σ y * σ x) → (∀ (x y : R), σ (x + y) = σ x + σ y) → σ (1 : R) = (1 : R) → (∀ (x : R), σ (-x) = -σ x) → ∀ {h a : R}, σ h = h → σ a = -a → (∀ (x : R), Commute a x) → ∀ (hu : IsUnit ((1 : R) - a * h)), have u := ↑hu.unit⁻¹ * ((1 : R) + a * h); σ u * u = (1 : R) :=34  @FRC.DiracML.cayley_unitary35set_option linter.defProp false in36/-- p08019 — 8:C5. The finite Cayley transform: the scalar Cayley map is defined on the whole shell, takes values in the norm-one cycle, and bijects the projective line onto it, which has $\p+1$ elements and is the unitary group of one channel. Cited definitions (not proofs): FRC.DiracML.Ext.field. -/37def p08019 := And.intro @FRC.DiracML.Ext.cayley_norm (And.intro @FRC.DiracML.Ext.cayley_injective (@FRC.DiracML.Ext.card_normOneGroup))38set_option linter.defProp false in39/-- p08020 — 8:C6. The $\F_{13}$ Schr\"odinger example: the kinetic Hamiltonian is nilpotent, every trace-zero parameter is admissible, and every nonzero parameter gives a unitary step of order $13$. -/40def p08020 := And.intro @FRC.DiracML.kinetic_nilpotent (@FRC.DiracML.cayley_period)41/-- p08022 — 8:D2. The Clifford relations of the gamma matrices. -/42theorem p08022 : (∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → FRC.DiracML.γ0 i w * FRC.DiracML.γ0 i w = -ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ1 i * FRC.DiracML.γ1 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ2 i * FRC.DiracML.γ2 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ3 i * FRC.DiracML.γ3 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ0 i w * FRC.DiracML.γ1 i + FRC.DiracML.γ1 i * FRC.DiracML.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ0 i w * FRC.DiracML.γ2 i + FRC.DiracML.γ2 i * FRC.DiracML.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ0 i w * FRC.DiracML.γ3 i + FRC.DiracML.γ3 i * FRC.DiracML.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ1 i * FRC.DiracML.γ2 i + FRC.DiracML.γ2 i * FRC.DiracML.γ1 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ1 i * FRC.DiracML.γ3 i + FRC.DiracML.γ3 i * FRC.DiracML.γ1 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ2 i * FRC.DiracML.γ3 i + FRC.DiracML.γ3 i * FRC.DiracML.γ2 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K)) ∧ ∀ {K : Type u_2} [CommRing K] {i : K}, i * i = (-1 : K) → FRC.DiracML.σ1 * FRC.DiracML.σ1 = (1 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.DiracML.σ2 i * FRC.DiracML.σ2 i = (1 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.DiracML.σ3 * FRC.DiracML.σ3 = (1 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.DiracML.σ1 * FRC.DiracML.σ2 i + FRC.DiracML.σ2 i * FRC.DiracML.σ1 = (0 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.DiracML.σ1 * FRC.DiracML.σ3 + FRC.DiracML.σ3 * FRC.DiracML.σ1 = (0 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.DiracML.σ2 i * FRC.DiracML.σ3 + FRC.DiracML.σ3 * FRC.DiracML.σ2 i = (0 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) :=43  And.intro @FRC.DiracML.clifford (@FRC.DiracML.pauli)44set_option linter.defProp false in45/-- p08025 — 8:D5. The boost group is the non-split cycle: the image of the extension's units with kernel the scalar line, the boost entries the coordinates of $z/\bar z$, cyclic of order $\p+1$; an order-three boost exists iff $3$ divides $\p+1$ (at $173$, not at $13$). -/46def p08025 := And.intro @FRC.DiracML.Ext.boost_eq_one_iff (And.intro @FRC.DiracML.Ext.boost_range (And.intro @FRC.DiracML.Ext.exists_boost_eq (And.intro @FRC.DiracML.Ext.card_normOneGroup (And.intro @FRC.DiracML.Ext.normOne_cyclic (@FRC.DiracML.Ext.order_three_iff)))))47/-- p08026 — 8:D6. Spin conjugation: the lift carries the two temporal gamma matrices to the stated combinations and fixes the other two. -/48theorem p08026 : (∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → ∀ (x y : K), FRC.DiracML.Mγ i w * FRC.DiracML.Mγ i w = ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.DiracML.Mγ i w) * FRC.DiracML.γ0 i w * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.DiracML.Mγ i w) = (x ^ (2 : ℕ) + ν * y ^ (2 : ℕ)) • FRC.DiracML.γ0 i w + -((2 : K) * x * y * ν) • FRC.DiracML.γ1 i ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.DiracML.Mγ i w) * FRC.DiracML.γ1 i * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.DiracML.Mγ i w) = -((2 : K) * x * y) • FRC.DiracML.γ0 i w + (x ^ (2 : ℕ) + ν * y ^ (2 : ℕ)) • FRC.DiracML.γ1 i ∧ FRC.DiracML.Mγ i w * FRC.DiracML.γ2 i = FRC.DiracML.γ2 i * FRC.DiracML.Mγ i w ∧ FRC.DiracML.Mγ i w * FRC.DiracML.γ3 i = FRC.DiracML.γ3 i * FRC.DiracML.Mγ i w) ∧ ∀ {F : Type u_2} [Field F] {i w ν x y : F}, i * i = (-1 : F) → w * w = ν → x ^ (2 : ℕ) - ν * y ^ (2 : ℕ) ≠ (0 : F) → (x ^ (2 : ℕ) - ν * y ^ (2 : ℕ))⁻¹ • (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) F) + -y • FRC.DiracML.Mγ i w) * FRC.DiracML.γ0 i w * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) F) + y • FRC.DiracML.Mγ i w) = FRC.DiracML.Aent ν x y • FRC.DiracML.γ0 i w + (ν * FRC.DiracML.Bent ν x y) • FRC.DiracML.γ1 i ∧ (x ^ (2 : ℕ) - ν * y ^ (2 : ℕ))⁻¹ • (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) F) + -y • FRC.DiracML.Mγ i w) * FRC.DiracML.γ1 i * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) F) + y • FRC.DiracML.Mγ i w) = FRC.DiracML.Bent ν x y • FRC.DiracML.γ0 i w + FRC.DiracML.Aent ν x y • FRC.DiracML.γ1 i :=49  And.intro @FRC.DiracML.spin_conjugation (@FRC.DiracML.spin_conjugation_AB)50/-- p08027 — 8:D7. The pullback intertwines the differences of the two frames: the difference along a transported basis vector of the pulled-back field is the pulled-back difference. -/51theorem p08027 : ∀ {K : Type u_1} [CommRing K] {G : Type u_2} [AddGroup G] (A : G ≃+ G) (e : G) (ψ : G → K), FRC.DiracML.translate (A e) (FRC.DiracML.pullback A ψ) = FRC.DiracML.pullback A (FRC.DiracML.translate e ψ) ∧ FRC.DiracML.laplacian (A e) (FRC.DiracML.pullback A ψ) = FRC.DiracML.pullback A (FRC.DiracML.laplacian e ψ) :=52  @FRC.DiracML.translate_covariance53/-- p08029 — 8:D9. The spinor form: under the plain conjugate transpose the gamma matrices carry mixed signs and the $\gamma^0$-twist fails; the odd product $X=\gamma^0\gamma^1\gamma^3$ is Hermitian with square $\nu$ and makes every gamma matrix anti-self-adjoint; the symmetric Dirac operator is self-adjoint and nilpotent for the $X$-form. Decided at $\p=13$, $173$ and $1549$. -/54theorem p08029 : (∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → FRC.DiracML.Xγ i w * FRC.DiracML.Xγ i w = ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.Xγ i w * FRC.DiracML.γ0 i w = FRC.DiracML.γ0 i w * FRC.DiracML.Xγ i w ∧ FRC.DiracML.Xγ i w * FRC.DiracML.γ1 i = FRC.DiracML.γ1 i * FRC.DiracML.Xγ i w ∧ FRC.DiracML.Xγ i w * FRC.DiracML.γ3 i = FRC.DiracML.γ3 i * FRC.DiracML.Xγ i w ∧ FRC.DiracML.Xγ i w * FRC.DiracML.γ2 i = -(FRC.DiracML.γ2 i * FRC.DiracML.Xγ i w)) ∧ (∀ {K : Type u_2} [CommRing K] [StarRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → star i = i → star w = -w → (FRC.DiracML.γ0 i w).conjTranspose = -FRC.DiracML.γ0 i w ∧ (FRC.DiracML.γ1 i).conjTranspose = -FRC.DiracML.γ1 i ∧ (FRC.DiracML.γ2 i).conjTranspose = FRC.DiracML.γ2 i ∧ (FRC.DiracML.γ3 i).conjTranspose = -FRC.DiracML.γ3 i ∧ (FRC.DiracML.Xγ i w).conjTranspose = FRC.DiracML.Xγ i w) ∧ ∀ {K : Type u_3} [CommRing K] [StarRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → star i = i → star w = -w → (FRC.DiracML.γ0 i w).conjTranspose * FRC.DiracML.Xγ i w = -(FRC.DiracML.Xγ i w * FRC.DiracML.γ0 i w) ∧ (FRC.DiracML.γ1 i).conjTranspose * FRC.DiracML.Xγ i w = -(FRC.DiracML.Xγ i w * FRC.DiracML.γ1 i) ∧ (FRC.DiracML.γ2 i).conjTranspose * FRC.DiracML.Xγ i w = -(FRC.DiracML.Xγ i w * FRC.DiracML.γ2 i) ∧ (FRC.DiracML.γ3 i).conjTranspose * FRC.DiracML.Xγ i w = -(FRC.DiracML.Xγ i w * FRC.DiracML.γ3 i) ∧ (FRC.DiracML.γ0 i w).conjTranspose * FRC.DiracML.γ0 i w = -(FRC.DiracML.γ0 i w * FRC.DiracML.γ0 i w) ∧ (FRC.DiracML.γ1 i).conjTranspose * FRC.DiracML.γ0 i w = FRC.DiracML.γ0 i w * FRC.DiracML.γ1 i :=55  And.intro @FRC.DiracML.spinor_twist (And.intro @FRC.DiracML.gamma_dagger (@FRC.DiracML.twist_adjoint))56/-- p08030 — 8:D10. Exact Dirac evolution: the Cayley step of the symmetric Dirac operator shifted by the mass preserves the $X$-form; massless it is unipotent with order a power of $\p$; massive it is the norm-one phase of the mass times a unipotent, and its order is their least common multiple ($169=\p^{2}$, $1183$, $2366$ for $m=0,1,2$ in $1{+}1$ at $\p=13$). -/57theorem p08030 : (∀ {R : Type u_1} [Ring R] (σ : R → R), (∀ (x y : R), σ (x * y) = σ y * σ x) → (∀ (x y : R), σ (x + y) = σ x + σ y) → σ (1 : R) = (1 : R) → (∀ (x : R), σ (-x) = -σ x) → ∀ {h a : R}, σ h = h → σ a = -a → (∀ (x : R), Commute a x) → ∀ (hu : IsUnit ((1 : R) - a * h)), have u := ↑hu.unit⁻¹ * ((1 : R) + a * h); σ u * u = (1 : R)) ∧ ∀ {R : Type u_2} [Ring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {t : R}, t ^ p = (1 : R) → (t - (1 : R)) ^ p = (0 : R) :=58  And.intro @FRC.DiracML.cayley_unitary (@FRC.DiracML.translation_nilpotent)59/-- p08031 — 8:D11. The two Dirac operators are one covariant family: the pullback identity holds for the symmetric differences, the transport carries the symmetric operator to its transported form, and the spinor form transports by the norm of the lift: norm-one lifts preserve it, the odd coset scales it by the nonsquare class. -/60theorem p08031 : (∀ {K : Type u_1} [CommRing K] [StarRing K] {i w ν x y : K}, i * i = (-1 : K) → w * w = ν → star w = -w → star x = x → star y = y → (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.DiracML.Mγ i w).conjTranspose = x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.DiracML.Mγ i w ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.DiracML.Mγ i w) * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.DiracML.Mγ i w) = (x ^ (2 : ℕ) - ν * y ^ (2 : ℕ)) • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K)) ∧ ∀ {K : Type u_2} [CommRing K] [StarRing K] {i w ν x y : K}, i * i = (-1 : K) → w * w = ν → star i = i → star w = -w → star x = x → star y = y → (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.DiracML.Mγ i w).conjTranspose * FRC.DiracML.Xγ i w * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.DiracML.Mγ i w) = (x ^ (2 : ℕ) - ν * y ^ (2 : ℕ)) • FRC.DiracML.Xγ i w :=61  And.intro @FRC.DiracML.lift_adjoint (@FRC.DiracML.lift_transport)62/-- p08035 — 8:E2. A self-map of a finite set is bijective iff its image count is the whole count iff its loss factor is one. -/63theorem p08035 : ∀ {X : Type u_1} [Fintype X] [DecidableEq X] (f : X → X), (Finset.image f Finset.univ).card = Fintype.card X ↔ Function.Bijective f :=64  @FRC.DiracML.loss_factor_one65set_option linter.defProp false in66/-- p08036 — 8:E3. Cayley propagators have loss factor one: the Cayley step is invertible. -/67def p08036 := @FRC.DiracML.unit_loss_factor_one68set_option linter.defProp false in69/-- p08037 — 8:E4. Period dichotomy: kinetic Hamiltonians give unipotent propagators of order $\p$; potential Hamiltonians give diagonal propagators with phases on the norm-one cycle and order dividing $\p+1$ ($14$ at $13$, $174$ at $173$). -/70def p08037 := And.intro @FRC.DiracML.cayley_period (And.intro @FRC.DiracML.kinetic_nilpotent (@FRC.DiracML.Ext.torus_period))71set_option linter.defProp false in72/-- p08040 — 8:F3. The free evolution is the drive: the drive pullback is unitary, the characters are its eigenvectors with the phase $g^{-k}$ per chronon, and every character line is isotropic except the two with eigenvalues $\pm1$, the meeting of the norm-one cycle and the drive cycle. Decided on $\F_{13}$ and $\F_{173}$. -/73def p08040 := And.intro @FRC.DiracML.drive_chi (And.intro @FRC.DiracML.drive_sum (And.intro @FRC.DiracML.chi_isotropy (@FRC.DiracML.exceptional_eigen)))74/-- p08041 — 8:F4. Two evolution sectors, one space: the drive's split-phase sector and the Cayley propagators' norm-one sector meet in $\{\pm1\}$ alone; the cycle Laplacian is self-adjoint, its Cayley steps commute with the drive, and the composite is unitary. -/75theorem p08041 : (∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [Finite K], Nat.card K = p ^ (2 : ℕ) → ∀ (g : (ZMod p)ˣ), orderOf g = p - (1 : ℕ) → orderOf g⁻¹ = p - (1 : ℕ) ∧ ∀ (x : Kˣ), orderOf x ≠ p) ∧ ∀ (κ : ℕ) [Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] (g : (ZMod ((4 : ℕ) * κ + (1 : ℕ)))ˣ), orderOf g = (4 : ℕ) * κ → ↑g⁻¹ ^ ((2 : ℕ) * κ) = (-1 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ∧ ∀ (u : ZMod ((4 : ℕ) * κ + (1 : ℕ))), u * u = (1 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) → u = (1 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ∨ u = (-1 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) :=76  And.intro @FRC.DiracML.sector_separation (@FRC.DiracML.exceptional_eigen)77set_option linter.defProp false in78/-- p08048 — 8:F6. The two spectra: the drive is semisimple with spectrum the drive cycle; the Dirac Cayley step at mass $m$ has the single eigenvalue $\varphi(-m)$ on the third cycle and the mass phases fill it once; the spectra meet in $\{\pm1\}$; the Hamiltonian form has the two eigenvalues $\varphi(\pm\im\nu m)$, a conjugate pair. Decided at $\p=13$ and $173$. -/79def p08048 := And.intro @FRC.DiracML.drive_chi (And.intro @FRC.DiracML.cayley_nilpotent_shift (And.intro @FRC.DiracML.Ext.cayley_injective (And.intro @FRC.DiracML.Ext.card_normOneGroup (@FRC.DiracML.sector_separation))))80/-- p08049 — 8:B4. The factorisation of the temporal coefficient: $\nu=g=2^{-1}\cdot(2g)$ on every shell, the class of $2^{-1}$ even iff $\kap$ is even, the class of $2g$ odd iff $\kap$ is even, the product odd always; the reframing flip preserves the parity class and reverses the one-way direction. -/81theorem p08049 : (∀ {K : Type u_1} [Field K] (g : K), (2 : K) ≠ (0 : K) → (2 : K)⁻¹ * ((2 : K) * g) = g) ∧ (∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {g : ZMod p}, g ≠ (0 : ZMod p) → ¬IsSquare g → (2 : ZMod p) ≠ (0 : ZMod p) → (IsSquare ((2 : ZMod p) * g) ↔ ¬IsSquare (2 : ZMod p))) ∧ (∀ (κ : ℕ) [hp' : Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] {g : ZMod ((4 : ℕ) * κ + (1 : ℕ))}, orderOf g = (4 : ℕ) * κ → (IsSquare (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ↔ Even κ) ∧ (IsSquare (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ↔ Even κ) ∧ (IsSquare (-2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ↔ Even κ) ∧ (IsSquare (g ^ ((3 : ℕ) * κ)) ↔ Even κ) ∧ g ^ ((3 : ℕ) * κ) = -g ^ κ ∧ IsSquare (-1 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))) ∧ (FRC.DiracML.Aent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (10 : ZMod (13 : ℕ)) ∧ FRC.DiracML.Bent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (2 : ZMod (13 : ℕ)) ∧ (10 : ZMod (13 : ℕ)) ^ (2 : ℕ) - (2 : ZMod (13 : ℕ)) * (2 : ZMod (13 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) * (7 : ZMod (13 : ℕ)) = (1 : ZMod (13 : ℕ)) ∧ ¬IsSquare (7 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (5 : ℕ) = (6 : ZMod (13 : ℕ)) ∧ ¬IsSquare (6 : ZMod (13 : ℕ)) ∧ orderOf (2 : ZMod (13 : ℕ)) = (12 : ℕ)) ∧ (171106 : ℕ) * (171106 : ℕ) * (2 : ℕ) % (2408561 : ℕ) = (1 : ℕ) ∧ (2 : ℕ) * (1204281 : ℕ) % (2408561 : ℕ) = (1 : ℕ) ∧ (1204281 : ℕ) * (12 : ℕ) % (2408561 : ℕ) = (6 : ℕ) ∧ Nat.Prime (2408561 : ℕ) :=82  And.intro @FRC.DiracML.nu_factorisation (And.intro @FRC.DiracML.two_g_class (And.intro @FRC.DiracML.named_residues (And.intro @FRC.DiracML.shell13 (@FRC.DiracML.carrier_constants))))83/-- p08051 — 8:D12. The worked shell $\F_{13}$ with the drive $2$: the boost at $x=y=1$ with $A=10$, $B=2$, the transported gamma matrices, the order $14$ of the boost cycle and no triality element; the named residues $2$, $2^{-1}$, $\im$, $e$, $\pi$ are nonsquares. -/84theorem p08051 : FRC.DiracML.Aent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (10 : ZMod (13 : ℕ)) ∧ FRC.DiracML.Bent (2 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) (1 : ZMod (13 : ℕ)) = (2 : ZMod (13 : ℕ)) ∧ (10 : ZMod (13 : ℕ)) ^ (2 : ℕ) - (2 : ZMod (13 : ℕ)) * (2 : ZMod (13 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) * (7 : ZMod (13 : ℕ)) = (1 : ZMod (13 : ℕ)) ∧ ¬IsSquare (7 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (5 : ℕ) = (6 : ZMod (13 : ℕ)) ∧ ¬IsSquare (6 : ZMod (13 : ℕ)) ∧ orderOf (2 : ZMod (13 : ℕ)) = (12 : ℕ) :=85  @FRC.DiracML.shell1386/-- p08052 — 8:F2. The latitude identities: the energy index $\kap+1$ is the first rung past the midpoint of the ladder; the shift by $\kap$ is multiplication by $g^{\kap}$ on the meridians and carries the first latitude to the energy latitude; $\kap=-4^{-1}$, so the energy radius is $3\cdot4^{-1}$ and $\pi=2\kap=-2^{-1}$; the unit-norm circle has $\p-1$ points. On $\F_{13}$ and $\F_{173}$. -/87theorem p08052 : ∀ (κ : ℕ) [hp : Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] {g : ZMod ((4 : ℕ) * κ + (1 : ℕ))}, orderOf g = (4 : ℕ) * κ → (4 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) * ↑κ = (-1 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) ∧ ↑κ = -(4 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ∧ (1 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) + ↑κ = (3 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) * (4 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ∧ (2 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) * ↑κ = -(2 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))⁻¹ ∧ g ^ κ = -g ^ ((3 : ℕ) * κ) ∧ κ + (1 : ℕ) ≤ (2 : ℕ) * κ :=88  @FRC.DiracML.latitude_identities89/-- p08053 — 8:X1. Two cycles for one unit circle: the continuum's single phase group appears on the shell as the drive cycle, carrying the free evolution, and the norm-one cycle, carrying the Cayley phases and the boosts, and the two meet in $\{\pm1\}$. -/90theorem p08053 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [Finite K], Nat.card K = p ^ (2 : ℕ) → ∀ (g : (ZMod p)ˣ), orderOf g = p - (1 : ℕ) → orderOf g⁻¹ = p - (1 : ℕ) ∧ ∀ (x : Kˣ), orderOf x ≠ p :=91  @FRC.DiracML.sector_separation92/-- p08054 — 8:X2. The one-way speed is gauge: the temporal coefficient is an odd drive step, registered transport is even, and the reframing flip reverses the one-way direction while preserving the parity class. -/93theorem p08054 : (∀ {K : Type u_1} [Field K] (g : K), (2 : K) ≠ (0 : K) → (2 : K)⁻¹ * ((2 : K) * g) = g) ∧ ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {g : ZMod p}, orderOf g = p - (1 : ℕ) → p % (2 : ℕ) = (1 : ℕ) → ∀ (k : ℕ), IsSquare (g ^ k) ↔ Even k :=94  And.intro @FRC.DiracML.nu_factorisation (@FRC.DiracML.parity_iff)95/-- p08055 — 8:X3. Mass is an evolution phase, not a kernel condition: the symmetric Dirac operator is nilpotent, the static massive equation has only the zero solution, and the mass enters as the norm-one factor of the Cayley step. -/96theorem p08055 : (∀ {R : Type u_1} [Ring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {t : R}, t ^ p = (1 : R) → (t - (1 : R)) ^ p = (0 : R)) ∧ (∀ {R : Type u_2} [Ring R] {α m N : R}, (∀ (x : R), Commute α x) → (∀ (x : R), Commute m x) → IsNilpotent N → ∀ (ha : IsUnit ((1 : R) + α * m)) (hb : IsUnit ((1 : R) - α * m)), ∃ (hu : IsUnit ((1 : R) - α * (N - m))), IsNilpotent (↑hu.unit⁻¹ * ((1 : R) + α * (N - m)) - ↑(hb.unit * ha.unit⁻¹))) ∧ ∀ {R : Type u_3} [Ring R] (σ : R → R), (∀ (x y : R), σ (x * y) = σ y * σ x) → (∀ (x y : R), σ (x + y) = σ x + σ y) → σ (1 : R) = (1 : R) → (∀ (x : R), σ (-x) = -σ x) → ∀ {h a : R}, σ h = h → σ a = -a → (∀ (x : R), Commute a x) → ∀ (hu : IsUnit ((1 : R) - a * h)), have u := ↑hu.unit⁻¹ * ((1 : R) + a * h); σ u * u = (1 : R) :=97  And.intro @FRC.DiracML.translation_nilpotent (And.intro @FRC.DiracML.cayley_nilpotent_shift (@FRC.DiracML.cayley_unitary))98/-- p08056 — 8:X4. The spinor form is forced: the continuum's $\gamma^0$-twist fails because Frobenius fixes the internal quarter-turn, and the arithmetic forces the twist onto the odd product omitting $\gamma^2$. -/99theorem p08056 : (∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → FRC.DiracML.Xγ i w * FRC.DiracML.Xγ i w = ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.Xγ i w * FRC.DiracML.γ0 i w = FRC.DiracML.γ0 i w * FRC.DiracML.Xγ i w ∧ FRC.DiracML.Xγ i w * FRC.DiracML.γ1 i = FRC.DiracML.γ1 i * FRC.DiracML.Xγ i w ∧ FRC.DiracML.Xγ i w * FRC.DiracML.γ3 i = FRC.DiracML.γ3 i * FRC.DiracML.Xγ i w ∧ FRC.DiracML.Xγ i w * FRC.DiracML.γ2 i = -(FRC.DiracML.γ2 i * FRC.DiracML.Xγ i w)) ∧ ∀ {K : Type u_2} [CommRing K] [StarRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → star i = i → star w = -w → (FRC.DiracML.γ0 i w).conjTranspose = -FRC.DiracML.γ0 i w ∧ (FRC.DiracML.γ1 i).conjTranspose = -FRC.DiracML.γ1 i ∧ (FRC.DiracML.γ2 i).conjTranspose = FRC.DiracML.γ2 i ∧ (FRC.DiracML.γ3 i).conjTranspose = -FRC.DiracML.γ3 i ∧ (FRC.DiracML.Xγ i w).conjTranspose = FRC.DiracML.Xγ i w :=100  And.intro @FRC.DiracML.spinor_twist (@FRC.DiracML.gamma_dagger)101/-- p08058 — 8:C8. Translations are unitary: every translation operator preserves the Hermitian form, and its adjoint is the opposite translation. -/102theorem p08058 : (∀ {K : Type u_1} [CommRing K] [StarRing K] {G : Type u_2} [AddGroup G] [Fintype G] (u : G) (ψ φ : G → K), FRC.DiracML.herm (FRC.DiracML.translate u ψ) (FRC.DiracML.translate u φ) = FRC.DiracML.herm ψ φ) ∧ ∀ {K : Type u_3} [CommRing K] [StarRing K] {G : Type u_4} [AddGroup G] [Fintype G] (u : G) (ψ φ : G → K), FRC.DiracML.herm (FRC.DiracML.translate u ψ) φ = FRC.DiracML.herm ψ (FRC.DiracML.translate (-u) φ) :=103  And.intro @FRC.DiracML.herm_translate (@FRC.DiracML.herm_translate_adjoint)104/-- p08059 — 8:C9. The finite Laplacian of an ordered basis is self-adjoint, each of its summands being self-adjoint. -/105theorem p08059 : ∀ {K : Type u_1} [CommRing K] [StarRing K] {G : Type u_2} [AddGroup G] [Fintype G] (e : G) (ψ φ : G → K), FRC.DiracML.herm (FRC.DiracML.laplacian e ψ) φ = FRC.DiracML.herm ψ (FRC.DiracML.laplacian e φ) :=106  @FRC.DiracML.herm_laplacian107/-- p08061 — 8:C11. Every finite Hamiltonian is self-adjoint: the Laplacian and the potential are, and the stiffness is Frobenius-fixed. -/108theorem p08061 : ∀ {K : Type u_1} [CommRing K] [StarRing K] {G : Type u_2} [AddGroup G] [Fintype G] (e : G) (ϰ : K), star ϰ = ϰ → ∀ (V : G → K), (∀ (x : G), star (V x) = V x) → ∀ (ψ φ : G → K), FRC.DiracML.herm (FRC.DiracML.hamiltonian e ϰ V ψ) φ = FRC.DiracML.herm ψ (FRC.DiracML.hamiltonian e ϰ V φ) :=109  @FRC.DiracML.herm_hamiltonian110/-- p08063 — 8:C13. Frame covariance: a change of basis by an invertible matrix intertwines, through the pullback of functions, the translations, the differences and the Laplacians of the two frames. -/111theorem p08063 : ∀ {K : Type u_1} [CommRing K] {G : Type u_2} [AddGroup G] (A : G ≃+ G) (e : G) (ψ : G → K), FRC.DiracML.translate (A e) (FRC.DiracML.pullback A ψ) = FRC.DiracML.pullback A (FRC.DiracML.translate e ψ) ∧ FRC.DiracML.laplacian (A e) (FRC.DiracML.pullback A ψ) = FRC.DiracML.pullback A (FRC.DiracML.laplacian e ψ) :=112  @FRC.DiracML.translate_covariance113/-- p08065 — 8:C15. Finite periodicity: every Cayley orbit is periodic, the unitary group of the finite space being finite. -/114theorem p08065 : ∀ {R : Type u_1} [Ring R] [Finite R] (u : Rˣ), IsOfFinOrder u :=115  @FRC.DiracML.cayley_periodic116/-- p08066 — 8:C16. The forward step: the orientation gauge $\alpha\mapsto-\alpha$ inverts every value of the Cayley map, the same $\Z_2$ as the derived orientation; the forward parameter composes the two quarter-turns and gives the finite Crank--Nicolson form at unit stiffness. -/117theorem p08066 : ∀ {F : Type u_1} [Field F] {ν : F}, ¬IsSquare ν → ∀ (k t : F), FRC.DiracML.Ext.cayley (-k) t * FRC.DiracML.Ext.cayley k t = (1 : FRC.Extension.Ext F ν) :=118  @FRC.DiracML.Ext.cayley_gauge119/-- p08067 — 8:D14. The boost is orthogonal: $\Lambda(x,y)$ preserves the coordinate form, by $A^2-\nu B^2=1$. -/120theorem p08067 : (∀ {F : Type u_1} [Field F] (ν x y u v : F), x ^ (2 : ℕ) - ν * y ^ (2 : ℕ) ≠ (0 : F) → u ^ (2 : ℕ) - ν * v ^ (2 : ℕ) ≠ (0 : F) → FRC.DiracML.Aent ν x y ^ (2 : ℕ) - ν * FRC.DiracML.Bent ν x y ^ (2 : ℕ) = (1 : F) ∧ FRC.DiracML.Aent ν x y * FRC.DiracML.Aent ν u v + ν * (FRC.DiracML.Bent ν x y * FRC.DiracML.Bent ν u v) = FRC.DiracML.Aent ν (x * u + ν * y * v) (x * v + y * u) ∧ FRC.DiracML.Aent ν x y * FRC.DiracML.Bent ν u v + FRC.DiracML.Bent ν x y * FRC.DiracML.Aent ν u v = FRC.DiracML.Bent ν (x * u + ν * y * v) (x * v + y * u) ∧ FRC.DiracML.Aent ν (1 : F) (0 : F) = (1 : F) ∧ FRC.DiracML.Bent ν (1 : F) (0 : F) = (0 : F) ∧ FRC.DiracML.Aent ν x (-y) = FRC.DiracML.Aent ν x y ∧ FRC.DiracML.Bent ν x (-y) = -FRC.DiracML.Bent ν x y) ∧ ∀ {F : Type u_2} [Field F] {ν : F} (z : (FRC.Extension.Ext F ν)ˣ), FRC.DiracML.Ext.boost z ∈ FRC.DiracML.Ext.normOneGroup F ν :=121  And.intro @FRC.DiracML.boost_entries (@FRC.DiracML.Ext.boost_mem)122/-- p08068 — 8:D15. The boosts form a subgroup of the orthogonal group: the product of two boosts is the boost of the product in the extension, the identity and the inverse are boosts. -/123theorem p08068 : ∀ {F : Type u_1} [Field F] (ν x y u v : F), x ^ (2 : ℕ) - ν * y ^ (2 : ℕ) ≠ (0 : F) → u ^ (2 : ℕ) - ν * v ^ (2 : ℕ) ≠ (0 : F) → FRC.DiracML.Aent ν x y ^ (2 : ℕ) - ν * FRC.DiracML.Bent ν x y ^ (2 : ℕ) = (1 : F) ∧ FRC.DiracML.Aent ν x y * FRC.DiracML.Aent ν u v + ν * (FRC.DiracML.Bent ν x y * FRC.DiracML.Bent ν u v) = FRC.DiracML.Aent ν (x * u + ν * y * v) (x * v + y * u) ∧ FRC.DiracML.Aent ν x y * FRC.DiracML.Bent ν u v + FRC.DiracML.Bent ν x y * FRC.DiracML.Aent ν u v = FRC.DiracML.Bent ν (x * u + ν * y * v) (x * v + y * u) ∧ FRC.DiracML.Aent ν (1 : F) (0 : F) = (1 : F) ∧ FRC.DiracML.Bent ν (1 : F) (0 : F) = (0 : F) ∧ FRC.DiracML.Aent ν x (-y) = FRC.DiracML.Aent ν x y ∧ FRC.DiracML.Bent ν x (-y) = -FRC.DiracML.Bent ν x y :=124  @FRC.DiracML.boost_entries125/-- p08069 — 8:D16. The explicit transported form: the transported Dirac operator is the Dirac operator of the transported frame with the transported gamma matrices, the spin conjugates of the standard ones. -/126theorem p08069 : ∀ {K : Type u_1} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → ∀ (x y : K), FRC.DiracML.Mγ i w * FRC.DiracML.Mγ i w = ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.DiracML.Mγ i w) * FRC.DiracML.γ0 i w * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.DiracML.Mγ i w) = (x ^ (2 : ℕ) + ν * y ^ (2 : ℕ)) • FRC.DiracML.γ0 i w + -((2 : K) * x * y * ν) • FRC.DiracML.γ1 i ∧ (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + -y • FRC.DiracML.Mγ i w) * FRC.DiracML.γ1 i * (x • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) + y • FRC.DiracML.Mγ i w) = -((2 : K) * x * y) • FRC.DiracML.γ0 i w + (x ^ (2 : ℕ) + ν * y ^ (2 : ℕ)) • FRC.DiracML.γ1 i ∧ FRC.DiracML.Mγ i w * FRC.DiracML.γ2 i = FRC.DiracML.γ2 i * FRC.DiracML.Mγ i w ∧ FRC.DiracML.Mγ i w * FRC.DiracML.γ3 i = FRC.DiracML.γ3 i * FRC.DiracML.Mγ i w :=127  @FRC.DiracML.spin_conjugation128/-- p08070 — 8:D17. The transported gamma matrices satisfy the Clifford relations, conjugation preserving anticommutators. -/129theorem p08070 : (∀ {R : Type u_1} [Ring R] (S : Rˣ) (a b : R), ↑S * a * ↑S⁻¹ * (↑S * b * ↑S⁻¹) + ↑S * b * ↑S⁻¹ * (↑S * a * ↑S⁻¹) = ↑S * (a * b + b * a) * ↑S⁻¹) ∧ ∀ {K : Type u_2} [CommRing K] {i w ν : K}, i * i = (-1 : K) → w * w = ν → FRC.DiracML.γ0 i w * FRC.DiracML.γ0 i w = -ν • (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ1 i * FRC.DiracML.γ1 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ2 i * FRC.DiracML.γ2 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ3 i * FRC.DiracML.γ3 i = (1 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ0 i w * FRC.DiracML.γ1 i + FRC.DiracML.γ1 i * FRC.DiracML.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ0 i w * FRC.DiracML.γ2 i + FRC.DiracML.γ2 i * FRC.DiracML.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ0 i w * FRC.DiracML.γ3 i + FRC.DiracML.γ3 i * FRC.DiracML.γ0 i w = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ1 i * FRC.DiracML.γ2 i + FRC.DiracML.γ2 i * FRC.DiracML.γ1 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ1 i * FRC.DiracML.γ3 i + FRC.DiracML.γ3 i * FRC.DiracML.γ1 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) ∧ FRC.DiracML.γ2 i * FRC.DiracML.γ3 i + FRC.DiracML.γ3 i * FRC.DiracML.γ2 i = (0 : Matrix (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) (Fin (2 : ℕ) ⊕ Fin (2 : ℕ)) K) :=130  And.intro @FRC.DiracML.conj_anticomm (@FRC.DiracML.clifford)131/-- p08072 — 8:D19. The worked shell $\F_{173}$, the second laboratory Subject, with the drive $2$ and $\im=93$: the boost at $x=y=1$ with $A=170$, $B=2$, the transported gamma matrices, the order $174$ of the boost cycle and its triality element; the named residues are nonsquares. -/132theorem p08072 : FRC.DiracML.Aent (2 : ZMod (173 : ℕ)) (1 : ZMod (173 : ℕ)) (1 : ZMod (173 : ℕ)) = (170 : ZMod (173 : ℕ)) ∧ FRC.DiracML.Bent (2 : ZMod (173 : ℕ)) (1 : ZMod (173 : ℕ)) (1 : ZMod (173 : ℕ)) = (2 : ZMod (173 : ℕ)) ∧ (170 : ZMod (173 : ℕ)) ^ (2 : ℕ) - (2 : ZMod (173 : ℕ)) * (2 : ZMod (173 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (173 : ℕ)) ∧ (93 : ZMod (173 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (173 : ℕ)) ∧ (2 : ZMod (173 : ℕ)) * (87 : ZMod (173 : ℕ)) = (1 : ZMod (173 : ℕ)) ∧ (2 : ZMod (173 : ℕ)) ^ (93 : ℕ) = (45 : ZMod (173 : ℕ)) ∧ (86 : ZMod (173 : ℕ)) = (2 : ZMod (173 : ℕ)) * (43 : ZMod (173 : ℕ)) ∧ ¬IsSquare (2 : ZMod (173 : ℕ)) ∧ ¬IsSquare (87 : ZMod (173 : ℕ)) ∧ ¬IsSquare (93 : ZMod (173 : ℕ)) ∧ ¬IsSquare (45 : ZMod (173 : ℕ)) ∧ ¬IsSquare (86 : ZMod (173 : ℕ)) ∧ orderOf (2 : ZMod (173 : ℕ)) = (172 : ℕ) :=133  @FRC.DiracML.shell173134/-- p08073 — 8:E5. The power map on the phase cycle has image count $(\p-1)/\gcd(\varepsilon,\p-1)$ and loss factor $\gcd(\varepsilon,\p-1)$, every nonempty fibre of that size. -/135theorem p08073 : ∀ {p : Nat} [hp : Fact (Nat.Prime p)] (ε : Nat), And (@Eq Nat (Nat.card ↥(@MonoidHom.ker (@Units (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@Units.instGroup (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@Units (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@Units.instMulOneClass (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@powMonoidHom (@Units (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@CommGroup.toCommMonoid (@Units (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@Units.instCommGroupUnits (ZMod p) (@CommRing.toCommMonoid (ZMod p) (ZMod.commRing p)))) ε))) ((@HSub.hSub Nat Nat Nat (@instHSub Nat instSubNat) p (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))).gcd ε)) (@Eq Nat (Nat.card ↥(@MonoidHom.range (@Units (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@Units.instGroup (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@Units (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@Units.instGroup (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@powMonoidHom (@Units (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@CommGroup.toCommMonoid (@Units (ZMod p) (@Semiring.toMonoid (ZMod p) (@CommSemiring.toSemiring (ZMod p) (@Semifield.toCommSemiring (ZMod p) (@Field.toSemifield (ZMod p) (@ZMod.instField p hp)))))) (@Units.instCommGroupUnits (ZMod p) (@CommRing.toCommMonoid (ZMod p) (ZMod.commRing p)))) ε))) (@HDiv.hDiv Nat Nat Nat (@instHDiv Nat Nat.instDiv) (@HSub.hSub Nat Nat Nat (@instHSub Nat instSubNat) p (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))) ((@HSub.hSub Nat Nat Nat (@instHSub Nat instSubNat) p (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))).gcd ε))) :=136  @FRC.DiracML.power_map_count137set_option linter.defProp false in138/-- p08074 — 8:E6. Boost transports have loss factor one: the pullback and the lift are bijective. -/139def p08074 := @FRC.DiracML.unit_loss_factor_one140/-- p08075 — 8:E7. Kinetic Hamiltonians are fully admissible: a nilpotent Hamiltonian, the kinetic Hamiltonian and the symmetric Dirac operator among them, has every trace-zero parameter admissible, on every shell. -/141theorem p08075 : (∀ {R : Type u_1} [Ring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {t c a : R}, t ^ p = (1 : R) → Commute c t → Commute a t → Commute a c → have h := c * (t + t ^ (p - (1 : ℕ)) - (2 : R)); (a * h) ^ p = (0 : R) ∧ IsNilpotent (a * h) ∧ IsUnit ((1 : R) - a * h)) ∧ ∀ {R : Type u_2} [Ring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {t : R}, t ^ p = (1 : R) → (t - (1 : R)) ^ p = (0 : R) :=142  And.intro @FRC.DiracML.kinetic_nilpotent (@FRC.DiracML.translation_nilpotent)143set_option linter.defProp false in144/-- p08077 — 8:F7. Finite plane waves, dispersion and the mass shell: the cycle Laplacian has the closed dispersion relation on the characters; the translations admit no characters and the kinetic sector is unipotent; the static massive Dirac equation has only the zero solution, the mass being an evolution phase. -/145def p08077 := And.intro @FRC.DiracML.dispersion (And.intro @FRC.DiracML.translation_nilpotent (@FRC.DiracML.cayley_nilpotent_shift))146-- end keys147148end FRC.LedgerML149