Theme/Operator.lean — FrcCore

1import FrcCore.Orbit2import FrcCore.Theme.Quadratic34/-!5# The operator layer of 8-dirac — a ring of operators up to a congruence, no axioms67The fourth file of the dirac theme (5 November 2026, the core-proof programme, decision D2): the general form of the8operator rows. An `OpRing` is a type with `+`, `*`, `−`, `0`, `1` and a congruence `≈` (an equivalence respected by the9three operations) satisfying the ring laws up to `≈`. The congruence is what lets the matrices of the spinor file —10functions of two indices read below the dimension — form a ring without function extensionality: two matrices are11congruent when their entries agree on the range, and nothing here needs more. Every theorem of the layer is stated up to12`≈` and holds in every `OpRing`: the Cayley step of a symmetric operator at an admissible parameter is unitary (C4); a13nilpotent operator has the geometric series as the inverse of `1 − N`, so the static massive equation has only the zero14solution (X3, F7); the Cayley step of a nilpotent shift minus a mass is a unit congruent, modulo a nilpotent, to the15scalar phase (D10); a two-sided unit is injective and surjective (E3, E6); conjugation by a unit preserves the16anticommutator (D17); the square of a sum of pairwise anticommuting operators is the sum of the squares, so the Dirac17operator factorises, `(𝒟 − m)(𝒟 + m) = □_η − m²` (D3, D18); and in characteristic `p`, `t^p = 1` forces `(t − 1)^p = 0`,18the translations unipotent (F7), by the binomial theorem and `p ∣ C(p, k)` on the shell. No axioms.19-/2021namespace FRC.Dirac.Operator2223/-! ## The ring up to a congruence -/2425/-- A ring of operators up to a congruence `eq`: the equivalence, its compatibility with the operations, and the26ring laws (commutative addition, associative multiplication, the unit, the two distributive laws), all up to `eq`. -/27class OpRing (R : Type) [Add R] [Mul R] [Neg R] [OfNat R 0] [OfNat R 1] where28  eq : R → R → Prop29  refl : ∀ x, eq x x30  symm : ∀ {x y}, eq x y → eq y x31  trans : ∀ {x y z}, eq x y → eq y z → eq x z32  add_congr : ∀ {x x' y y'}, eq x x' → eq y y' → eq (x + y) (x' + y')33  mul_congr : ∀ {x x' y y'}, eq x x' → eq y y' → eq (x * y) (x' * y')34  neg_congr : ∀ {x x'}, eq x x' → eq (-x) (-x')35  add_comm : ∀ x y, eq (x + y) (y + x)36  add_assoc : ∀ x y z, eq (x + y + z) (x + (y + z))37  zero_add : ∀ x, eq (0 + x) x38  add_neg : ∀ x, eq (x + -x) 039  mul_assoc : ∀ x y z, eq (x * y * z) (x * (y * z))40  one_mul : ∀ x, eq (1 * x) x41  mul_one : ∀ x, eq (x * 1) x42  left_distrib : ∀ x y z, eq (x * (y + z)) (x * y + x * z)43  right_distrib : ∀ x y z, eq ((x + y) * z) (x * z + y * z)4445variable {R : Type} [Add R] [Mul R] [Neg R] [OfNat R 0] [OfNat R 1] [OpRing R]4647instance : HasEquiv R := ⟨OpRing.eq⟩4849instance : Trans (α := R) (β := R) (γ := R) (· ≈ ·) (· ≈ ·) (· ≈ ·) := ⟨OpRing.trans⟩5051open OpRing (add_congr mul_congr neg_congr add_comm add_assoc zero_add add_neg mul_assoc one_mul mul_one left_distrib right_distrib)5253theorem eq_refl (x : R) : x ≈ x := OpRing.refl x54theorem eq_symm {x y : R} (h : x ≈ y) : y ≈ x := OpRing.symm h55theorem eq_trans {x y z : R} (h : x ≈ y) (h' : y ≈ z) : x ≈ z := OpRing.trans h h'56theorem eq_of_eq {x y : R} (h : x = y) : x ≈ y := h ▸ OpRing.refl x5758theorem add_congr_left {x x' : R} (y : R) (h : x ≈ x') : x + y ≈ x' + y := add_congr h (eq_refl y)59theorem add_congr_right (x : R) {y y' : R} (h : y ≈ y') : x + y ≈ x + y' := add_congr (eq_refl x) h60theorem mul_congr_left {x x' : R} (y : R) (h : x ≈ x') : x * y ≈ x' * y := mul_congr h (eq_refl y)61theorem mul_congr_right (x : R) {y y' : R} (h : y ≈ y') : x * y ≈ x * y' := mul_congr (eq_refl x) h6263theorem add_zero (x : R) : x + 0 ≈ x := eq_trans (add_comm x 0) (zero_add x)64theorem neg_add (x : R) : -x + x ≈ 0 := eq_trans (add_comm (-x) x) (add_neg x)65theorem add_left_comm (x y z : R) : x + (y + z) ≈ y + (x + z) :=66  calc x + (y + z) ≈ x + y + z := eq_symm (add_assoc x y z)67    _ ≈ y + x + z := add_congr_left z (add_comm x y)68    _ ≈ y + (x + z) := add_assoc y x z69theorem add_add_add_comm (a b c d : R) : a + b + (c + d) ≈ a + c + (b + d) :=70  calc a + b + (c + d) ≈ a + (b + (c + d)) := add_assoc a b (c + d)71    _ ≈ a + (c + (b + d)) := add_congr_right a (add_left_comm b c d)72    _ ≈ a + c + (b + d) := eq_symm (add_assoc a c (b + d))7374/-- Cancellation on the left: `x + y ≈ x + z → y ≈ z`. -/75theorem add_left_cancel {x y z : R} (h : x + y ≈ x + z) : y ≈ z :=76  calc y ≈ 0 + y := eq_symm (zero_add y)77    _ ≈ -x + x + y := add_congr_left y (eq_symm (neg_add x))78    _ ≈ -x + (x + y) := add_assoc _ _ _79    _ ≈ -x + (x + z) := add_congr_right _ h80    _ ≈ -x + x + z := eq_symm (add_assoc _ _ _)81    _ ≈ 0 + z := add_congr_left z (neg_add x)82    _ ≈ z := zero_add z8384theorem add_right_cancel {x y z : R} (h : y + x ≈ z + x) : y ≈ z :=85  add_left_cancel (eq_trans (add_comm x y) (eq_trans h (add_comm z x)))8687theorem neg_eq_of_add_eq_zero {x y : R} (h : x + y ≈ 0) : -x ≈ y :=88  add_left_cancel (eq_trans (add_neg x) (eq_symm h))8990theorem neg_neg (x : R) : - -x ≈ x := neg_eq_of_add_eq_zero (neg_add x)91theorem neg_zero : (-0 : R) ≈ 0 := neg_eq_of_add_eq_zero (zero_add 0)92theorem neg_add_rev (x y : R) : -(x + y) ≈ -x + -y :=93  neg_eq_of_add_eq_zero <|94    calc x + y + (-x + -y) ≈ x + -x + (y + -y) := add_add_add_comm x y (-x) (-y)95      _ ≈ 0 + 0 := add_congr (add_neg x) (add_neg y)96      _ ≈ 0 := zero_add 09798theorem mul_zero (x : R) : x * 0 ≈ 0 :=99  add_left_cancel (x := x * 0) <|100    calc x * 0 + x * 0 ≈ x * (0 + 0) := eq_symm (left_distrib x 0 0)101      _ ≈ x * 0 := mul_congr_right x (zero_add 0)102      _ ≈ x * 0 + 0 := eq_symm (add_zero _)103theorem zero_mul (x : R) : 0 * x ≈ 0 :=104  add_left_cancel (x := 0 * x) <|105    calc 0 * x + 0 * x ≈ (0 + 0) * x := eq_symm (right_distrib 0 0 x)106      _ ≈ 0 * x := mul_congr_left x (zero_add 0)107      _ ≈ 0 * x + 0 := eq_symm (add_zero _)108theorem neg_mul (x y : R) : -(x * y) ≈ -x * y :=109  neg_eq_of_add_eq_zero <|110    calc x * y + -x * y ≈ (x + -x) * y := eq_symm (right_distrib x (-x) y)111      _ ≈ 0 * y := mul_congr_left y (add_neg x)112      _ ≈ 0 := zero_mul y113theorem mul_neg (x y : R) : -(x * y) ≈ x * -y :=114  neg_eq_of_add_eq_zero <|115    calc x * y + x * -y ≈ x * (y + -y) := eq_symm (left_distrib x y (-y))116      _ ≈ x * 0 := mul_congr_right x (add_neg y)117      _ ≈ 0 := mul_zero x118theorem neg_one_mul (x : R) : (-1 : R) * x ≈ -x := eq_trans (eq_symm (neg_mul 1 x)) (neg_congr (one_mul x))119theorem mul_neg_one (x : R) : x * (-1 : R) ≈ -x := eq_trans (eq_symm (mul_neg x 1)) (neg_congr (mul_one x))120theorem neg_mul_neg (x y : R) : -x * -y ≈ x * y :=121  calc -x * -y ≈ -(x * -y) := eq_symm (neg_mul x (-y))122    _ ≈ - -(x * y) := neg_congr (eq_symm (mul_neg x y))123    _ ≈ x * y := neg_neg _124theorem sub_self (x : R) : x + -x ≈ 0 := add_neg x125theorem eq_of_sub_eq_zero {x y : R} (h : x + -y ≈ 0) : x ≈ y :=126  calc x ≈ x + 0 := eq_symm (add_zero x)127    _ ≈ x + (-y + y) := add_congr_right x (eq_symm (neg_add y))128    _ ≈ x + -y + y := eq_symm (add_assoc _ _ _)129    _ ≈ 0 + y := add_congr_left y h130    _ ≈ y := zero_add y131theorem sub_eq_zero_of_eq {x y : R} (h : x ≈ y) : x + -y ≈ 0 :=132  eq_trans (add_congr_left (-y) h) (add_neg y)133/-- `x − (y + z) = (x − y) − z`. -/134theorem sub_add (x y z : R) : x + -(y + z) ≈ x + -y + -z :=135  calc x + -(y + z) ≈ x + (-y + -z) := add_congr_right x (neg_add_rev y z)136    _ ≈ x + -y + -z := eq_symm (add_assoc _ _ _)137/-- `(x + y) − y = x`. -/138theorem add_sub_cancel (x y : R) : x + y + -y ≈ x :=139  calc x + y + -y ≈ x + (y + -y) := add_assoc _ _ _140    _ ≈ x + 0 := add_congr_right x (add_neg y)141    _ ≈ x := add_zero x142143/-! ## Commuting and central elements -/144145/-- `x` and `y` commute. -/146def Comm (x y : R) : Prop := x * y ≈ y * x147/-- `c` commutes with everything. -/148def Central (c : R) : Prop := ∀ x, c * x ≈ x * c149150theorem Comm.symm {x y : R} (h : Comm x y) : Comm y x := OpRing.symm h151theorem Central.comm {c : R} (hc : Central c) (x : R) : Comm c x := hc x152theorem Comm.mul_left {x y z : R} (hx : Comm x z) (hy : Comm y z) : Comm (x * y) z :=153  calc x * y * z ≈ x * (y * z) := mul_assoc _ _ _154    _ ≈ x * (z * y) := mul_congr_right x hy155    _ ≈ x * z * y := eq_symm (mul_assoc _ _ _)156    _ ≈ z * x * y := mul_congr_left y hx157    _ ≈ z * (x * y) := mul_assoc _ _ _158theorem Comm.mul_right {x y z : R} (hx : Comm z x) (hy : Comm z y) : Comm z (x * y) :=159  (Comm.mul_left hx.symm hy.symm).symm160theorem Comm.add_left {x y z : R} (hx : Comm x z) (hy : Comm y z) : Comm (x + y) z :=161  calc (x + y) * z ≈ x * z + y * z := right_distrib _ _ _162    _ ≈ z * x + z * y := add_congr hx hy163    _ ≈ z * (x + y) := eq_symm (left_distrib _ _ _)164theorem Comm.add_right {x y z : R} (hx : Comm z x) (hy : Comm z y) : Comm z (x + y) :=165  (Comm.add_left hx.symm hy.symm).symm166theorem Comm.neg_left {x z : R} (hx : Comm x z) : Comm (-x) z :=167  calc -x * z ≈ -(x * z) := eq_symm (neg_mul x z)168    _ ≈ -(z * x) := neg_congr hx169    _ ≈ z * -x := mul_neg z x170theorem Comm.neg_right {x z : R} (hx : Comm z x) : Comm z (-x) := (Comm.neg_left hx.symm).symm171theorem Comm.one_left (x : R) : Comm 1 x := eq_trans (one_mul x) (eq_symm (mul_one x))172theorem Comm.zero_left (x : R) : Comm 0 x := eq_trans (zero_mul x) (eq_symm (mul_zero x))173theorem Comm.refl (x : R) : Comm x x := OpRing.refl _174theorem Comm.congr {x x' y y' : R} (hx : x ≈ x') (hy : y ≈ y') (h : Comm x y) : Comm x' y' :=175  eq_trans (mul_congr (eq_symm hx) (eq_symm hy)) (eq_trans h (mul_congr hy hx))176theorem Central.mul {c d : R} (hc : Central c) (hd : Central d) : Central (c * d) :=177  fun x => Comm.mul_left (hc x) (hd x)178theorem Central.add {c d : R} (hc : Central c) (hd : Central d) : Central (c + d) :=179  fun x => Comm.add_left (hc x) (hd x)180theorem Central.neg {c : R} (hc : Central c) : Central (-c) := fun x => Comm.neg_left (hc x)181theorem Central.one : Central (1 : R) := Comm.one_left182theorem Central.zero : Central (0 : R) := Comm.zero_left183theorem Central.congr {c c' : R} (h : c ≈ c') (hc : Central c) : Central c' :=184  fun x => Comm.congr h (eq_refl x) (hc x)185186/-! ## Powers -/187188/-- `x ^ n` by structural recursion, `x ^ (n+1) = x ^ n * x`. -/189def opow (x : R) : Nat → R190  | 0 => 1191  | n + 1 => opow x n * x192193omit [Add R] [Neg R] [OfNat R 0] [OpRing R] in194theorem opow_zero (x : R) : opow x 0 = 1 := rfl195omit [Add R] [Neg R] [OfNat R 0] [OpRing R] in196theorem opow_succ (x : R) (n : Nat) : opow x (n + 1) = opow x n * x := rfl197theorem opow_one (x : R) : opow x 1 ≈ x := one_mul x198199theorem opow_congr {x x' : R} (h : x ≈ x') : ∀ n, opow x n ≈ opow x' n200  | 0 => eq_refl 1201  | n + 1 => mul_congr (opow_congr h n) h202203theorem opow_comm {x y : R} (h : Comm x y) : ∀ n, Comm (opow x n) y204  | 0 => Comm.one_left y205  | n + 1 => Comm.mul_left (opow_comm h n) h206207theorem opow_self_comm (x : R) (n : Nat) : Comm (opow x n) x := opow_comm (Comm.refl x) n208209theorem opow_add (x : R) (m : Nat) : ∀ n, opow x (m + n) ≈ opow x m * opow x n210  | 0 => eq_symm (mul_one _)211  | n + 1 =>212    calc opow x (m + n) * x ≈ opow x m * opow x n * x := mul_congr_left x (opow_add x m n)213      _ ≈ opow x m * (opow x n * x) := mul_assoc _ _ _214215theorem opow_succ' (x : R) (n : Nat) : opow x (n + 1) ≈ x * opow x n :=216  calc opow x n * x ≈ x * opow x n := opow_self_comm x n217218/-- `(x y)^n = x^n y^n` for commuting `x`, `y`. -/219theorem mul_opow {x y : R} (h : Comm x y) : ∀ n, opow (x * y) n ≈ opow x n * opow y n220  | 0 => eq_symm (one_mul 1)221  | n + 1 =>222    calc opow (x * y) n * (x * y) ≈ opow x n * opow y n * (x * y) := mul_congr_left _ (mul_opow h n)223      _ ≈ opow x n * (opow y n * (x * y)) := mul_assoc _ _ _224      _ ≈ opow x n * (opow y n * x * y) := mul_congr_right _ (eq_symm (mul_assoc _ _ _))225      _ ≈ opow x n * (x * opow y n * y) := mul_congr_right _ (mul_congr_left y (opow_comm h.symm n))226      _ ≈ opow x n * (x * (opow y n * y)) := mul_congr_right _ (mul_assoc _ _ _)227      _ ≈ opow x n * x * (opow y n * y) := eq_symm (mul_assoc _ _ _)228229theorem opow_one_left : ∀ n, opow (1 : R) n ≈ 1230  | 0 => eq_refl 1231  | n + 1 => eq_trans (mul_one _) (opow_one_left n)232233theorem opow_zero_of_zero : ∀ n, opow (0 : R) (n + 1) ≈ 0234  | _ => mul_zero _235236/-- A power past a vanishing power vanishes. -/237theorem opow_eq_zero_of {x : R} {k : Nat} (h : opow x k ≈ 0) (j : Nat) : opow x (k + j) ≈ 0 :=238  calc opow x (k + j) ≈ opow x k * opow x j := opow_add x k j239    _ ≈ 0 * opow x j := mul_congr_left _ h240    _ ≈ 0 := zero_mul _241242theorem Central.opow {c : R} (hc : Central c) (n : Nat) : Central (opow c n) := fun x => opow_comm (hc x) n243244/-! ## Natural multiples -/245246/-- `n • x = x + ⋯ + x` (`n` terms). -/247def nsmul : Nat → R → R248  | 0, _ => 0249  | n + 1, x => nsmul n x + x250251omit [Mul R] [Neg R] [OfNat R 1] [OpRing R] in252theorem nsmul_zero (x : R) : nsmul 0 x = 0 := rfl253omit [Mul R] [Neg R] [OfNat R 1] [OpRing R] in254theorem nsmul_succ (n : Nat) (x : R) : nsmul (n + 1) x = nsmul n x + x := rfl255256theorem nsmul_congr {x x' : R} (h : x ≈ x') : ∀ n, nsmul n x ≈ nsmul n x'257  | 0 => eq_refl 0258  | n + 1 => add_congr (nsmul_congr h n) h259260theorem nsmul_add (x y : R) : ∀ n, nsmul n (x + y) ≈ nsmul n x + nsmul n y261  | 0 => eq_symm (zero_add 0)262  | n + 1 =>263    calc nsmul n (x + y) + (x + y) ≈ nsmul n x + nsmul n y + (x + y) := add_congr_left _ (nsmul_add x y n)264      _ ≈ nsmul n x + x + (nsmul n y + y) := add_add_add_comm _ _ _ _265266theorem add_nsmul (m : Nat) (x : R) : ∀ n, nsmul (m + n) x ≈ nsmul m x + nsmul n x267  | 0 => eq_symm (add_zero _)268  | n + 1 =>269    calc nsmul (m + n) x + x ≈ nsmul m x + nsmul n x + x := add_congr_left x (add_nsmul m x n)270      _ ≈ nsmul m x + (nsmul n x + x) := add_assoc _ _ _271272theorem nsmul_mul_left (x y : R) : ∀ n, nsmul n x * y ≈ nsmul n (x * y)273  | 0 => zero_mul y274  | n + 1 =>275    calc (nsmul n x + x) * y ≈ nsmul n x * y + x * y := right_distrib _ _ _276      _ ≈ nsmul n (x * y) + x * y := add_congr_left _ (nsmul_mul_left x y n)277278theorem mul_nsmul_right (x y : R) : ∀ n, x * nsmul n y ≈ nsmul n (x * y)279  | 0 => mul_zero x280  | n + 1 =>281    calc x * (nsmul n y + y) ≈ x * nsmul n y + x * y := left_distrib _ _ _282      _ ≈ nsmul n (x * y) + x * y := add_congr_left _ (mul_nsmul_right x y n)283284theorem mul_nsmul (m : Nat) (x : R) : ∀ n, nsmul (m * n) x ≈ nsmul m (nsmul n x)285  | 0 => by rw [Nat.mul_zero]; exact eq_symm (nsmul_zero_right m)286  | n + 1 =>287    calc nsmul (m * n + m) x ≈ nsmul (m * n) x + nsmul m x := add_nsmul _ x m288      _ ≈ nsmul m (nsmul n x) + nsmul m x := add_congr_left _ (mul_nsmul m x n)289      _ ≈ nsmul m (nsmul n x + x) := eq_symm (nsmul_add _ _ m)290where291  nsmul_zero_right : ∀ m, nsmul m (0 : R) ≈ 0292    | 0 => eq_refl 0293    | m + 1 => eq_trans (add_zero _) (nsmul_zero_right m)294295theorem nsmul_zero_right : ∀ m, nsmul m (0 : R) ≈ 0 := mul_nsmul.nsmul_zero_right296297theorem nsmul_eq_mul_one (x : R) (n : Nat) : nsmul n x ≈ nsmul n 1 * x :=298  eq_symm (eq_trans (nsmul_mul_left 1 x n) (nsmul_congr (one_mul x) n))299300/-- A natural multiple of a vanishing element vanishes. -/301theorem nsmul_of_eq_zero {x : R} (h : x ≈ 0) (n : Nat) : nsmul n x ≈ 0 :=302  eq_trans (nsmul_congr h n) (nsmul_zero_right n)303304theorem nsmul_comm_of {x y : R} (h : Comm x y) (n : Nat) : Comm (nsmul n x) y :=305  calc nsmul n x * y ≈ nsmul n (x * y) := nsmul_mul_left x y n306    _ ≈ nsmul n (y * x) := nsmul_congr h n307    _ ≈ y * nsmul n x := eq_symm (mul_nsmul_right y x n)308309/-! ## Sums -/310311/-- `Σ_{j<n} f j` in the ring. -/312def osum (f : Nat → R) : Nat → R313  | 0 => 0314  | n + 1 => osum f n + f n315316omit [Mul R] [Neg R] [OfNat R 1] [OpRing R] in317theorem osum_zero (f : Nat → R) : osum f 0 = 0 := rfl318omit [Mul R] [Neg R] [OfNat R 1] [OpRing R] in319theorem osum_succ (f : Nat → R) (n : Nat) : osum f (n + 1) = osum f n + f n := rfl320321theorem osum_congr {f h : Nat → R} : ∀ n, (∀ j, j < n → f j ≈ h j) → osum f n ≈ osum h n322  | 0, _ => eq_refl 0323  | n + 1, e => add_congr (osum_congr n fun j hj => e j (Nat.lt_succ_of_lt hj)) (e n (Nat.lt_succ_self n))324325theorem osum_add (f h : Nat → R) : ∀ n, osum (fun j => f j + h j) n ≈ osum f n + osum h n326  | 0 => eq_symm (zero_add 0)327  | n + 1 =>328    calc osum (fun j => f j + h j) n + (f n + h n) ≈ osum f n + osum h n + (f n + h n) :=329          add_congr_left _ (osum_add f h n)330      _ ≈ osum f n + f n + (osum h n + h n) := add_add_add_comm _ _ _ _331332theorem osum_mul_left (c : R) (f : Nat → R) : ∀ n, c * osum f n ≈ osum (fun j => c * f j) n333  | 0 => mul_zero c334  | n + 1 =>335    calc c * (osum f n + f n) ≈ c * osum f n + c * f n := left_distrib _ _ _336      _ ≈ osum (fun j => c * f j) n + c * f n := add_congr_left _ (osum_mul_left c f n)337338theorem osum_mul_right (c : R) (f : Nat → R) : ∀ n, osum f n * c ≈ osum (fun j => f j * c) n339  | 0 => zero_mul c340  | n + 1 =>341    calc (osum f n + f n) * c ≈ osum f n * c + f n * c := right_distrib _ _ _342      _ ≈ osum (fun j => f j * c) n + f n * c := add_congr_left _ (osum_mul_right c f n)343344theorem osum_eq_zero {f : Nat → R} : ∀ n, (∀ j, j < n → f j ≈ 0) → osum f n ≈ 0345  | 0, _ => eq_refl 0346  | n + 1, h =>347    calc osum f n + f n ≈ 0 + 0 := add_congr (osum_eq_zero n fun j hj => h j (Nat.lt_succ_of_lt hj)) (h n (Nat.lt_succ_self n))348      _ ≈ 0 := zero_add 0349350theorem osum_neg (f : Nat → R) : ∀ n, osum (fun j => -(f j)) n ≈ -(osum f n)351  | 0 => eq_symm neg_zero352  | n + 1 =>353    calc osum (fun j => -(f j)) n + -(f n) ≈ -(osum f n) + -(f n) := add_congr_left _ (osum_neg f n)354      _ ≈ -(osum f n + f n) := eq_symm (neg_add_rev _ _)355356theorem osum_comm {f : Nat → R} {y : R} : ∀ n, (∀ j, j < n → Comm (f j) y) → Comm (osum f n) y357  | 0, _ => Comm.zero_left y358  | n + 1, h => Comm.add_left (osum_comm n fun j hj => h j (Nat.lt_succ_of_lt hj)) (h n (Nat.lt_succ_self n))359360/-! ## Units (8:E3, 8:E6) -/361362/-- `v` is a two-sided inverse of `u`. -/363def Inverse (u v : R) : Prop := u * v ≈ 1 ∧ v * u ≈ 1364365theorem Inverse.symm {u v : R} (h : Inverse u v) : Inverse v u := ⟨h.2, h.1⟩366367theorem Inverse.congr {u u' v v' : R} (hu : u ≈ u') (hv : v ≈ v') (h : Inverse u v) : Inverse u' v' :=368  ⟨eq_trans (mul_congr (eq_symm hu) (eq_symm hv)) h.1, eq_trans (mul_congr (eq_symm hv) (eq_symm hu)) h.2⟩369370theorem Inverse.one : Inverse (1 : R) 1 := ⟨one_mul 1, one_mul 1⟩371372theorem Inverse.mul {u v u' v' : R} (h : Inverse u v) (h' : Inverse u' v') : Inverse (u * u') (v' * v) := by373  refine ⟨?_, ?_⟩374  · calc u * u' * (v' * v) ≈ u * (u' * v' * v) := eq_trans (mul_assoc _ _ _) (mul_congr_right u (eq_symm (mul_assoc _ _ _)))375      _ ≈ u * (1 * v) := mul_congr_right u (mul_congr_left v h'.1)376      _ ≈ u * v := mul_congr_right u (one_mul v)377      _ ≈ 1 := h.1378  · calc v' * v * (u * u') ≈ v' * (v * u * u') := eq_trans (mul_assoc _ _ _) (mul_congr_right v' (eq_symm (mul_assoc _ _ _)))379      _ ≈ v' * (1 * u') := mul_congr_right v' (mul_congr_left u' h.2)380      _ ≈ v' * u' := mul_congr_right v' (one_mul u')381      _ ≈ 1 := h'.2382383/-- The inverse of an element commuting with `x` commutes with `x`. -/384theorem Inverse.comm_of_comm {u v x : R} (h : Inverse u v) (hx : Comm u x) : Comm v x :=385  calc v * x ≈ v * x * 1 := eq_symm (mul_one _)386    _ ≈ v * x * (u * v) := mul_congr_right _ (eq_symm h.1)387    _ ≈ v * (x * u) * v := eq_trans (eq_symm (mul_assoc _ _ _)) (mul_congr_left v (mul_assoc _ _ _))388    _ ≈ v * (u * x) * v := mul_congr_left v (mul_congr_right v (eq_symm hx))389    _ ≈ v * u * x * v := mul_congr_left v (eq_symm (mul_assoc _ _ _))390    _ ≈ 1 * x * v := mul_congr_left v (mul_congr_left x h.2)391    _ ≈ x * v := mul_congr_left v (one_mul x)392393theorem Inverse.central {u v : R} (h : Inverse u v) (hu : Central u) : Central v :=394  fun x => h.comm_of_comm (hu x)395396/-- 8:E3, 8:E6 — a unit is injective: `u x ≈ u y → x ≈ y` when `u` has a left inverse. -/397theorem unit_injective {u v : R} (h : v * u ≈ 1) {x y : R} (e : u * x ≈ u * y) : x ≈ y :=398  calc x ≈ 1 * x := eq_symm (one_mul x)399    _ ≈ v * u * x := mul_congr_left x (eq_symm h)400    _ ≈ v * (u * x) := mul_assoc _ _ _401    _ ≈ v * (u * y) := mul_congr_right v e402    _ ≈ v * u * y := eq_symm (mul_assoc _ _ _)403    _ ≈ 1 * y := mul_congr_left y h404    _ ≈ y := one_mul y405406/-- 8:E3, 8:E6 — a unit is surjective: every `y` is `u x` when `u` has a right inverse. -/407theorem unit_surjective {u v : R} (h : u * v ≈ 1) (y : R) : ∃ x, u * x ≈ y :=408  ⟨v * y, calc u * (v * y) ≈ u * v * y := eq_symm (mul_assoc _ _ _)409    _ ≈ 1 * y := mul_congr_left y h410    _ ≈ y := one_mul y⟩411412/-- A unit has trivial kernel: `u x ≈ 0 → x ≈ 0`. -/413theorem unit_kernel {u v : R} (h : v * u ≈ 1) {x : R} (e : u * x ≈ 0) : x ≈ 0 :=414  unit_injective h (eq_trans e (eq_symm (mul_zero u)))415416/-! ## The geometric series and nilpotent operators (8:X3, 8:F7) -/417418/-- `1 + N + ⋯ + N^{k−1}`. -/419def geom (N : R) (k : Nat) : R := osum (fun j => opow N j) k420421theorem geom_comm {N x : R} (h : Comm N x) (k : Nat) : Comm (geom N k) x :=422  osum_comm k fun j _ => opow_comm h j423424theorem geom_congr {N N' : R} (h : N ≈ N') (k : Nat) : geom N k ≈ geom N' k :=425  osum_congr k fun j _ => opow_congr h j426427/-- `(1 − N)(1 + N + ⋯ + N^{k−1}) = 1 − N^k`, the telescoping product. -/428theorem one_sub_mul_geom (N : R) : ∀ k, (1 + -N) * geom N k ≈ 1 + -(opow N k)429  | 0 => eq_trans (mul_zero _) (eq_symm (add_neg 1))430  | k + 1 =>431    calc (1 + -N) * (geom N k + opow N k) ≈ (1 + -N) * geom N k + (1 + -N) * opow N k := left_distrib _ _ _432      _ ≈ 1 + -(opow N k) + (opow N k + -(opow N (k + 1))) := by433          refine add_congr (one_sub_mul_geom N k) ?_434          calc (1 + -N) * opow N k ≈ 1 * opow N k + -N * opow N k := right_distrib _ _ _435            _ ≈ opow N k + -(N * opow N k) := add_congr (one_mul _) (eq_symm (neg_mul _ _))436            _ ≈ opow N k + -(opow N (k + 1)) := add_congr_right _ (neg_congr (eq_symm (opow_succ' N k)))437      _ ≈ 1 + (-(opow N k) + opow N k) + -(opow N (k + 1)) :=438          eq_trans (eq_symm (add_assoc _ _ _)) (add_congr_left _ (add_assoc _ _ _))439      _ ≈ 1 + 0 + -(opow N (k + 1)) := add_congr_left _ (add_congr_right _ (neg_add _))440      _ ≈ 1 + -(opow N (k + 1)) := add_congr_left _ (add_zero 1)441442theorem geom_mul_one_sub (N : R) (k : Nat) : geom N k * (1 + -N) ≈ 1 + -(opow N k) :=443  eq_trans (geom_comm (Comm.add_right (eq_symm (Comm.one_left N)) (Comm.neg_right (Comm.refl N))) k)444    (one_sub_mul_geom N k)445446/-- 8:X3 — the series inverse: for a nilpotent `N` (`N^k ≈ 0`), `1 − N` is a unit with inverse the geometric series. -/447theorem series_inverse {N : R} {k : Nat} (h : opow N k ≈ 0) : Inverse (1 + -N) (geom N k) :=448  ⟨eq_trans (one_sub_mul_geom N k) (eq_trans (add_congr_right 1 (neg_congr h)) (eq_trans (add_congr_right 1 neg_zero) (add_zero 1))),449   eq_trans (geom_mul_one_sub N k) (eq_trans (add_congr_right 1 (neg_congr h)) (eq_trans (add_congr_right 1 neg_zero) (add_zero 1)))⟩450451/-- `geom N (j + 1) ≈ 1 + N · geom N j`. -/452theorem geom_succ_left (N : R) : ∀ j, geom N (j + 1) ≈ 1 + N * geom N j453  | 0 => eq_trans (zero_add 1) (eq_symm (eq_trans (add_congr_right 1 (mul_zero N)) (add_zero 1)))454  | j + 1 =>455    calc geom N (j + 1) + opow N (j + 1) ≈ 1 + N * geom N j + N * opow N j :=456          add_congr (geom_succ_left N j) (opow_succ' N j)457      _ ≈ 1 + (N * geom N j + N * opow N j) := add_assoc _ _ _458      _ ≈ 1 + N * (geom N j + opow N j) := add_congr_right 1 (eq_symm (left_distrib _ _ _))459460/-- 8:X3, 8:F7 — the static massive equation has only the zero solution: with `N` nilpotent and the mass `m` a461unit of central inverse (`m m' ≈ 1`, `m'` central), `N − m` is a unit — its inverse `geom (m' N) k · (−m')` — so462`(N − m) ψ ≈ 0` forces `ψ ≈ 0`. -/463theorem static_inverse {N m m' : R} {k : Nat} (h : opow N k ≈ 0) (hm' : Central m')464    (hmm : m * m' ≈ 1) : Inverse (N + -m) (geom (m' * N) k * -m') := by465  have hX : opow (m' * N) k ≈ 0 :=466    calc opow (m' * N) k ≈ opow m' k * opow N k := mul_opow (hm' N) k467      _ ≈ opow m' k * 0 := mul_congr_right _ h468      _ ≈ 0 := mul_zero _469  have hG := series_inverse hX470  have hm'm : m' * m ≈ 1 := eq_trans (hm' m) hmm471  have hfac : N + -m ≈ -m * (1 + -(m' * N)) :=472    calc N + -m ≈ -m + N := add_comm _ _473      _ ≈ -m + 1 * N := add_congr_right _ (eq_symm (one_mul N))474      _ ≈ -m + m * m' * N := add_congr_right _ (mul_congr_left N (eq_symm hmm))475      _ ≈ -m + m * (m' * N) := add_congr_right _ (mul_assoc _ _ _)476      _ ≈ -m * 1 + -m * -(m' * N) := add_congr (eq_symm (mul_one _)) (eq_symm (neg_mul_neg _ _))477      _ ≈ -m * (1 + -(m' * N)) := eq_symm (left_distrib _ _ _)478  have hneg : Inverse (-m) (-m') := ⟨eq_trans (neg_mul_neg _ _) hmm, eq_trans (neg_mul_neg _ _) hm'm⟩479  exact (hneg.mul hG).congr (eq_symm hfac) (eq_refl _)480481/-- 8:X3, 8:F7 — the static massive equation `(N − m) ψ ≈ 0` has only the zero solution, `N − m` being a unit. -/482theorem static_unique {N m m' : R} {k : Nat} (h : opow N k ≈ 0) (hm' : Central m')483    (hmm : m * m' ≈ 1) {ψ : R} (e : (N + -m) * ψ ≈ 0) : ψ ≈ 0 :=484  unit_kernel (static_inverse h hm' hmm).2 e485486/-! ## The Cayley step (8:C4, 8:D10) -/487488/-- An anti-automorphism of the ring up to the congruence — the adjoint `†`. -/489structure Adjoint (σ : R → R) : Prop where490  congr : ∀ {x y : R}, x ≈ y → σ x ≈ σ y491  mul : ∀ x y : R, σ (x * y) ≈ σ y * σ x492  add : ∀ x y : R, σ (x + y) ≈ σ x + σ y493  one : σ (1 : R) ≈ 1494  neg : ∀ x : R, σ (-x) ≈ -(σ x)495496/-- The adjoint of `1 + a h` is `1 − a h` when `h` is symmetric and `a` central with `σ a ≈ −a`. -/497theorem Adjoint.one_add {σ : R → R} (hσ : Adjoint σ) {h a : R} (hh : σ h ≈ h) (ha : σ a ≈ -a) (hc : Central a) :498    σ (1 + a * h) ≈ 1 + -(a * h) :=499  calc σ (1 + a * h) ≈ σ 1 + σ (a * h) := hσ.add _ _500    _ ≈ 1 + σ h * σ a := add_congr hσ.one (hσ.mul _ _)501    _ ≈ 1 + h * -a := add_congr_right 1 (mul_congr hh ha)502    _ ≈ 1 + -(h * a) := add_congr_right 1 (eq_symm (mul_neg _ _))503    _ ≈ 1 + -(a * h) := add_congr_right 1 (neg_congr (eq_symm (hc h)))504505theorem Adjoint.one_sub {σ : R → R} (hσ : Adjoint σ) {h a : R} (hh : σ h ≈ h) (ha : σ a ≈ -a) (hc : Central a) :506    σ (1 + -(a * h)) ≈ 1 + a * h :=507  calc σ (1 + -(a * h)) ≈ σ 1 + σ (-(a * h)) := hσ.add _ _508    _ ≈ 1 + -(σ (a * h)) := add_congr hσ.one (hσ.neg _)509    _ ≈ 1 + -(σ h * σ a) := add_congr_right 1 (neg_congr (hσ.mul _ _))510    _ ≈ 1 + -(h * -a) := add_congr_right 1 (neg_congr (mul_congr hh ha))511    _ ≈ 1 + - -(h * a) := add_congr_right 1 (neg_congr (eq_symm (mul_neg _ _)))512    _ ≈ 1 + h * a := add_congr_right 1 (neg_neg _)513    _ ≈ 1 + a * h := add_congr_right 1 (eq_symm (hc h))514515/-- The adjoint of an inverse pair is an inverse pair. -/516theorem Adjoint.inverse {σ : R → R} (hσ : Adjoint σ) {u v : R} (h : Inverse u v) : Inverse (σ u) (σ v) :=517  ⟨eq_trans (eq_symm (hσ.mul v u)) (eq_trans (hσ.congr h.2) hσ.one),518   eq_trans (eq_symm (hσ.mul u v)) (eq_trans (hσ.congr h.1) hσ.one)⟩519520/-- The twist of an adjoint by a unit: `τ a = X' σ(a) X` with `X X' ≈ 1`, `X' X ≈ 1` is an adjoint again — the521`X`-adjoint of the spinor form, for which the Cayley step preserves the `X`-form (8:D10). -/522theorem Adjoint.twist {σ : R → R} (hσ : Adjoint σ) {X X' : R} (hX : Inverse X X') :523    Adjoint (fun a => X' * σ a * X) where524  congr := fun h => mul_congr_left _ (mul_congr_right _ (hσ.congr h))525  mul := fun a b =>526    calc X' * σ (a * b) * X ≈ X' * (σ b * σ a) * X := mul_congr_left _ (mul_congr_right _ (hσ.mul a b))527      _ ≈ X' * σ b * σ a * X := mul_congr_left _ (eq_symm (mul_assoc _ _ _))528      _ ≈ X' * σ b * (1 * σ a) * X := mul_congr_left _ (mul_congr_right _ (eq_symm (one_mul _)))529      _ ≈ X' * σ b * (X * X' * σ a) * X := mul_congr_left _ (mul_congr_right _ (mul_congr_left _ (eq_symm hX.1)))530      _ ≈ X' * σ b * (X * (X' * σ a)) * X := mul_congr_left _ (mul_congr_right _ (mul_assoc _ _ _))531      _ ≈ X' * σ b * X * (X' * σ a) * X := mul_congr_left _ (eq_symm (mul_assoc _ _ _))532      _ ≈ X' * σ b * X * (X' * σ a * X) := mul_assoc _ _ _533  add := fun a b =>534    calc X' * σ (a + b) * X ≈ X' * (σ a + σ b) * X := mul_congr_left _ (mul_congr_right _ (hσ.add a b))535      _ ≈ (X' * σ a + X' * σ b) * X := mul_congr_left _ (left_distrib _ _ _)536      _ ≈ X' * σ a * X + X' * σ b * X := right_distrib _ _ _537  one :=538    calc X' * σ 1 * X ≈ X' * 1 * X := mul_congr_left _ (mul_congr_right _ hσ.one)539      _ ≈ X' * X := mul_congr_left _ (mul_one _)540      _ ≈ 1 := hX.2541  neg := fun a =>542    calc X' * σ (-a) * X ≈ X' * -(σ a) * X := mul_congr_left _ (mul_congr_right _ (hσ.neg a))543      _ ≈ -(X' * σ a) * X := mul_congr_left _ (eq_symm (mul_neg _ _))544      _ ≈ -(X' * σ a * X) := eq_symm (neg_mul _ _)545546/-- 8:C4, 8:D10, 8:X3 — the Cayley step is unitary: for `h` symmetric (`σ h ≈ h`), `a` central with `σ a ≈ −a`, and `v` the inverse547of `1 − a h`, the step `u = v (1 + a h)` satisfies `σ(u) u ≈ 1`. The adjoint of `1 − a h` is `1 + a h`, so `σ v` is the548inverse of `1 + a h`; `v` commutes with `1 + a h`; and `σ(u) u = (1 − a h) σ(v) v (1 + a h) = (1 − a h) σ(v) (1 + a h) v`. -/549theorem cayley_unitary {σ : R → R} (hσ : Adjoint σ) {h a v : R} (hh : σ h ≈ h) (ha : σ a ≈ -a) (hc : Central a)550    (hv : Inverse (1 + -(a * h)) v) : σ (v * (1 + a * h)) * (v * (1 + a * h)) ≈ 1 := by551  have hσv : Inverse (1 + a * h) (σ v) := (hσ.inverse hv).congr (hσ.one_sub hh ha hc) (eq_refl _)552  have hMP : Comm (1 + -(a * h)) (1 + a * h) :=553    Comm.add_left (Comm.one_left _) (Comm.neg_left (Comm.add_right (Comm.one_left _).symm (Comm.refl _)))554  have hvP : Comm v (1 + a * h) := hv.comm_of_comm hMP555  calc σ (v * (1 + a * h)) * (v * (1 + a * h)) ≈ σ (1 + a * h) * σ v * (v * (1 + a * h)) :=556        mul_congr_left _ (hσ.mul _ _)557    _ ≈ (1 + -(a * h)) * σ v * ((1 + a * h) * v) := mul_congr (mul_congr_left _ (hσ.one_add hh ha hc)) hvP558    _ ≈ (1 + -(a * h)) * (σ v * ((1 + a * h) * v)) := mul_assoc _ _ _559    _ ≈ (1 + -(a * h)) * (σ v * (1 + a * h) * v) := mul_congr_right _ (eq_symm (mul_assoc _ _ _))560    _ ≈ (1 + -(a * h)) * (1 * v) := mul_congr_right _ (mul_congr_left v hσv.2)561    _ ≈ (1 + -(a * h)) * v := mul_congr_right _ (one_mul v)562    _ ≈ 1 := hv.1563564/-- 8:D10 — the Cayley step of a nilpotent shift minus a mass. With `α`, `m` central, `a = 1 + α m` a central unit565of inverse `a'`, `b = 1 − α m`, and `N` nilpotent (`N^{k+1} ≈ 0`): `1 − α(N − m) = a (1 − a' α N)` is a unit, with566inverse `V = geom (a' α N) (k+1) · a'`, and the step `U = V (1 + α(N − m))` differs from the scalar phase `b a'` by567`N c` with `c` commuting with `N`. The massless step (`m = 0`, `b = a = a' = 1`) is `1 + N c`. -/568theorem cayley_nilpotent_shift {α m a' N : R} {k : Nat} (hα : Central α) (hm : Central m) (ha' : Central a')569    (ha : Inverse (1 + α * m) a') (hN : opow N (k + 1) ≈ 0) :570    Inverse (1 + -(α * (N + -m))) (geom (a' * (α * N)) (k + 1) * a') ∧571    ∃ c, Comm N c ∧ geom (a' * (α * N)) (k + 1) * a' * (1 + α * (N + -m)) + -((1 + -(α * m)) * a') ≈ N * c := by572  have hca : Central (a' * α) := ha'.mul hα573  have hXN : a' * (α * N) ≈ N * (a' * α) := eq_trans (eq_symm (mul_assoc _ _ _)) (hca N)574  have hCXN : Comm (a' * (α * N)) N := Comm.mul_left (ha' N) (Comm.mul_left (hα N) (Comm.refl N))575  have hX : opow (a' * (α * N)) (k + 1) ≈ 0 :=576    calc opow (a' * (α * N)) (k + 1) ≈ opow (N * (a' * α)) (k + 1) := opow_congr hXN _577      _ ≈ opow N (k + 1) * opow (a' * α) (k + 1) := mul_opow (eq_symm (hca N)) _578      _ ≈ 0 * opow (a' * α) (k + 1) := mul_congr_left _ hN579      _ ≈ 0 := zero_mul _580  have hG := series_inverse hX581  have haX : (1 + α * m) * (a' * (α * N)) ≈ α * N :=582    calc (1 + α * m) * (a' * (α * N)) ≈ (1 + α * m) * a' * (α * N) := eq_symm (mul_assoc _ _ _)583      _ ≈ 1 * (α * N) := mul_congr_left _ ha.1584      _ ≈ α * N := one_mul _585  have hMfac : 1 + -(α * (N + -m)) ≈ (1 + α * m) * (1 + -(a' * (α * N))) :=586    calc 1 + -(α * (N + -m)) ≈ 1 + -(α * N + α * -m) := add_congr_right 1 (neg_congr (left_distrib _ _ _))587      _ ≈ 1 + -(α * N + -(α * m)) := add_congr_right 1 (neg_congr (add_congr_right _ (eq_symm (mul_neg _ _))))588      _ ≈ 1 + (-(α * N) + - -(α * m)) := add_congr_right 1 (neg_add_rev _ _)589      _ ≈ 1 + (-(α * N) + α * m) := add_congr_right 1 (add_congr_right _ (neg_neg _))590      _ ≈ 1 + (α * m + -(α * N)) := add_congr_right 1 (add_comm _ _)591      _ ≈ 1 + α * m + -(α * N) := eq_symm (add_assoc _ _ _)592      _ ≈ (1 + α * m) * 1 + -((1 + α * m) * (a' * (α * N))) :=593          add_congr (eq_symm (mul_one _)) (neg_congr (eq_symm haX))594      _ ≈ (1 + α * m) * 1 + (1 + α * m) * -(a' * (α * N)) := add_congr_right _ (mul_neg _ _)595      _ ≈ (1 + α * m) * (1 + -(a' * (α * N))) := eq_symm (left_distrib _ _ _)596  refine ⟨(ha.mul hG).congr (eq_symm hMfac) (eq_refl _), ?_⟩597  -- the step minus the phase598  have hb : Central (1 + -(α * m)) := Central.add Central.one (Central.neg (hα.mul hm))599  have hP : 1 + α * (N + -m) ≈ 1 + -(α * m) + α * N :=600    calc 1 + α * (N + -m) ≈ 1 + (α * N + α * -m) := add_congr_right 1 (left_distrib _ _ _)601      _ ≈ 1 + (α * N + -(α * m)) := add_congr_right 1 (add_congr_right _ (eq_symm (mul_neg _ _)))602      _ ≈ 1 + (-(α * m) + α * N) := add_congr_right 1 (add_comm _ _)603      _ ≈ 1 + -(α * m) + α * N := eq_symm (add_assoc _ _ _)604  have hGk : geom (a' * (α * N)) (k + 1) ≈ 1 + a' * (α * N) * geom (a' * (α * N)) k := geom_succ_left _ k605  have hGX : Comm (geom (a' * (α * N)) (k + 1)) (a' * (α * N)) := geom_comm (Comm.refl _) _606  have hGkN : Comm N (geom (a' * (α * N)) k) := (geom_comm hCXN k).symm607  have hGN : Comm N (geom (a' * (α * N)) (k + 1)) := (geom_comm hCXN (k + 1)).symm608  refine ⟨a' * α * (geom (a' * (α * N)) k * (a' * (1 + -(α * m)))) + a' * α * geom (a' * (α * N)) (k + 1), ?_, ?_⟩609  · exact Comm.add_right610      (Comm.mul_right (eq_symm (hca N)) (Comm.mul_right hGkN (Comm.mul_right (eq_symm (ha' N)) (eq_symm (hb N)))))611      (Comm.mul_right (eq_symm (hca N)) hGN)612  · -- `U = G a' P = G (a' b) + G (a' α N)`; `G (a' b) = a' b + X G_k (a' b)`; `a' b = b a'`613    have hU : geom (a' * (α * N)) (k + 1) * a' * (1 + α * (N + -m)) ≈614        (1 + -(α * m)) * a' +615          (a' * (α * N) * geom (a' * (α * N)) k * (a' * (1 + -(α * m))) +616            geom (a' * (α * N)) (k + 1) * (a' * (α * N))) :=617      calc geom (a' * (α * N)) (k + 1) * a' * (1 + α * (N + -m))618          ≈ geom (a' * (α * N)) (k + 1) * (a' * (1 + -(α * m) + α * N)) :=619            eq_trans (mul_assoc _ _ _) (mul_congr_right _ (mul_congr_right _ hP))620        _ ≈ geom (a' * (α * N)) (k + 1) * (a' * (1 + -(α * m)) + a' * (α * N)) :=621            mul_congr_right _ (left_distrib _ _ _)622        _ ≈ geom (a' * (α * N)) (k + 1) * (a' * (1 + -(α * m))) + geom (a' * (α * N)) (k + 1) * (a' * (α * N)) :=623            left_distrib _ _ _624        _ ≈ (1 + a' * (α * N) * geom (a' * (α * N)) k) * (a' * (1 + -(α * m))) +625              geom (a' * (α * N)) (k + 1) * (a' * (α * N)) := add_congr_left _ (mul_congr_left _ hGk)626        _ ≈ 1 * (a' * (1 + -(α * m))) + a' * (α * N) * geom (a' * (α * N)) k * (a' * (1 + -(α * m))) +627              geom (a' * (α * N)) (k + 1) * (a' * (α * N)) := add_congr_left _ (right_distrib _ _ _)628        _ ≈ (1 + -(α * m)) * a' + a' * (α * N) * geom (a' * (α * N)) k * (a' * (1 + -(α * m))) +629              geom (a' * (α * N)) (k + 1) * (a' * (α * N)) :=630            add_congr_left _ (add_congr_left _ (eq_trans (one_mul _) (ha' _)))631        _ ≈ (1 + -(α * m)) * a' +632              (a' * (α * N) * geom (a' * (α * N)) k * (a' * (1 + -(α * m))) +633                geom (a' * (α * N)) (k + 1) * (a' * (α * N))) := add_assoc _ _ _634    calc geom (a' * (α * N)) (k + 1) * a' * (1 + α * (N + -m)) + -((1 + -(α * m)) * a')635        ≈ (1 + -(α * m)) * a' +636            (a' * (α * N) * geom (a' * (α * N)) k * (a' * (1 + -(α * m))) +637              geom (a' * (α * N)) (k + 1) * (a' * (α * N))) + -((1 + -(α * m)) * a') := add_congr_left _ hU638      _ ≈ a' * (α * N) * geom (a' * (α * N)) k * (a' * (1 + -(α * m))) +639            geom (a' * (α * N)) (k + 1) * (a' * (α * N)) + (1 + -(α * m)) * a' + -((1 + -(α * m)) * a') :=640          add_congr_left _ (add_comm _ _)641      _ ≈ a' * (α * N) * geom (a' * (α * N)) k * (a' * (1 + -(α * m))) +642            geom (a' * (α * N)) (k + 1) * (a' * (α * N)) := add_sub_cancel _ _643      _ ≈ N * (a' * α * (geom (a' * (α * N)) k * (a' * (1 + -(α * m))))) +644            N * (a' * α * geom (a' * (α * N)) (k + 1)) := by645          refine add_congr ?_ ?_646          · calc a' * (α * N) * geom (a' * (α * N)) k * (a' * (1 + -(α * m)))647                ≈ N * (a' * α) * geom (a' * (α * N)) k * (a' * (1 + -(α * m))) :=648                  mul_congr_left _ (mul_congr_left _ hXN)649              _ ≈ N * (a' * α * geom (a' * (α * N)) k) * (a' * (1 + -(α * m))) :=650                  mul_congr_left _ (mul_assoc _ _ _)651              _ ≈ N * (a' * α * geom (a' * (α * N)) k * (a' * (1 + -(α * m)))) := mul_assoc _ _ _652              _ ≈ N * (a' * α * (geom (a' * (α * N)) k * (a' * (1 + -(α * m))))) :=653                  mul_congr_right _ (mul_assoc _ _ _)654          · calc geom (a' * (α * N)) (k + 1) * (a' * (α * N))655                ≈ a' * (α * N) * geom (a' * (α * N)) (k + 1) := hGX656              _ ≈ N * (a' * α) * geom (a' * (α * N)) (k + 1) := mul_congr_left _ hXN657              _ ≈ N * (a' * α * geom (a' * (α * N)) (k + 1)) := mul_assoc _ _ _658      _ ≈ N * (a' * α * (geom (a' * (α * N)) k * (a' * (1 + -(α * m)))) + a' * α * geom (a' * (α * N)) (k + 1)) :=659          eq_symm (left_distrib _ _ _)660661/-- 8:D10 — the step minus the phase is nilpotent: `(U − b a')^{k+1} ≈ 0` when `U − b a' ≈ N c`, `N c ≈ c N`,662`N^{k+1} ≈ 0`. With the phase central, `U^{(k+1)} ≈ (b a')^{k+1}` follows in characteristic `p` for `k + 1 = p`663(the unipotent file); the massless step has `b a' = 1`. -/664theorem nilpotent_of_eq_mul {u N c : R} {k : Nat} (hu : u ≈ N * c) (hc : Comm N c) (hN : opow N (k + 1) ≈ 0) :665    opow u (k + 1) ≈ 0 :=666  calc opow u (k + 1) ≈ opow (N * c) (k + 1) := opow_congr hu _667    _ ≈ opow N (k + 1) * opow c (k + 1) := mul_opow hc _668    _ ≈ 0 * opow c (k + 1) := mul_congr_left _ hN669    _ ≈ 0 := zero_mul _670671/-! ## Conjugation and the anticommutator (8:D17) -/672673/-- Conjugation `a ↦ S a S'` by a unit `S` of inverse `S'`. -/674def conjBy (S S' a : R) : R := S * a * S'675676theorem conjBy_mul {S S' : R} (h : Inverse S S') (a b : R) : conjBy S S' a * conjBy S S' b ≈ conjBy S S' (a * b) :=677  calc S * a * S' * (S * b * S') ≈ S * a * (S' * (S * b * S')) := mul_assoc _ _ _678    _ ≈ S * a * (S' * (S * b) * S') := mul_congr_right _ (eq_symm (mul_assoc _ _ _))679    _ ≈ S * a * (S' * S * b * S') := mul_congr_right _ (mul_congr_left _ (eq_symm (mul_assoc _ _ _)))680    _ ≈ S * a * (1 * b * S') := mul_congr_right _ (mul_congr_left _ (mul_congr_left _ h.2))681    _ ≈ S * a * (b * S') := mul_congr_right _ (mul_congr_left _ (one_mul b))682    _ ≈ S * a * b * S' := eq_symm (mul_assoc _ _ _)683    _ ≈ S * (a * b) * S' := mul_congr_left _ (mul_assoc _ _ _)684685theorem conjBy_add (S S' a b : R) : conjBy S S' (a + b) ≈ conjBy S S' a + conjBy S S' b :=686  calc S * (a + b) * S' ≈ (S * a + S * b) * S' := mul_congr_left _ (left_distrib _ _ _)687    _ ≈ S * a * S' + S * b * S' := right_distrib _ _ _688689/-- 8:D17, 8:D18 — conjugation by a unit preserves the anticommutator: `{S a S', S b S'} ≈ S {a, b} S'`, so the transported690gammas satisfy the Clifford relations the originals do. -/691theorem conj_anticomm {S S' : R} (h : Inverse S S') (a b : R) :692    conjBy S S' a * conjBy S S' b + conjBy S S' b * conjBy S S' a ≈ conjBy S S' (a * b + b * a) :=693  eq_trans (add_congr (conjBy_mul h a b) (conjBy_mul h b a)) (eq_symm (conjBy_add _ _ _ _))694695/-- Conjugation preserves central values: `S c S' ≈ c` for central `c`. -/696theorem conjBy_central {S S' : R} (h : Inverse S S') {c : R} (hc : Central c) : conjBy S S' c ≈ c :=697  calc S * c * S' ≈ c * S * S' := mul_congr_left _ (eq_symm (hc S))698    _ ≈ c * (S * S') := mul_assoc _ _ _699    _ ≈ c * 1 := mul_congr_right _ h.1700    _ ≈ c := mul_one c701702/-! ## The square of a sum of anticommuting operators and the Dirac factorisation (8:D3, 8:D18) -/703704/-- `A` and `B` anticommute. -/705def Anticomm (A B : R) : Prop := A * B + B * A ≈ 0706707theorem Anticomm.symm {A B : R} (h : Anticomm A B) : Anticomm B A := eq_trans (add_comm _ _) h708709theorem Anticomm.add_left {A B C : R} (hA : Anticomm A C) (hB : Anticomm B C) : Anticomm (A + B) C :=710  calc (A + B) * C + C * (A + B) ≈ A * C + B * C + (C * A + C * B) := add_congr (right_distrib _ _ _) (left_distrib _ _ _)711    _ ≈ A * C + C * A + (B * C + C * B) := add_add_add_comm _ _ _ _712    _ ≈ 0 + 0 := add_congr hA hB713    _ ≈ 0 := zero_add 0714715/-- `(A + B)² ≈ A² + B²` when `A`, `B` anticommute. -/716theorem sq_add_of_anticomm {A B : R} (h : Anticomm A B) : (A + B) * (A + B) ≈ A * A + B * B :=717  calc (A + B) * (A + B) ≈ (A + B) * A + (A + B) * B := left_distrib _ _ _718    _ ≈ A * A + B * A + (A * B + B * B) := add_congr (right_distrib _ _ _) (right_distrib _ _ _)719    _ ≈ A * A + (B * A + (A * B + B * B)) := add_assoc _ _ _720    _ ≈ A * A + (B * A + A * B + B * B) := add_congr_right _ (eq_symm (add_assoc _ _ _))721    _ ≈ A * A + (0 + B * B) := add_congr_right _ (add_congr_left _ h.symm)722    _ ≈ A * A + B * B := add_congr_right _ (zero_add _)723724/-- The square of a sum of pairwise anticommuting operators is the sum of the squares. -/725theorem sq_osum {A : Nat → R} : ∀ n, (∀ i j, i < n → j < n → i ≠ j → Anticomm (A i) (A j)) →726    osum A n * osum A n ≈ osum (fun i => A i * A i) n727  | 0, _ => mul_zero 0728  | n + 1, h => by729    have hS : Anticomm (osum A n) (A n) := by730      show osum A n * A n + A n * osum A n ≈ 0731      calc osum A n * A n + A n * osum A n ≈ osum (fun i => A i * A n) n + osum (fun i => A n * A i) n :=732            add_congr (osum_mul_right _ _ n) (osum_mul_left _ _ n)733        _ ≈ osum (fun i => A i * A n + A n * A i) n := eq_symm (osum_add _ _ n)734        _ ≈ 0 := osum_eq_zero n fun i hi =>735            h i n (Nat.lt_succ_of_lt hi) (Nat.lt_succ_self n) (Nat.ne_of_lt hi)736    calc (osum A n + A n) * (osum A n + A n) ≈ osum A n * osum A n + A n * A n := sq_add_of_anticomm hS737      _ ≈ osum (fun i => A i * A i) n + A n * A n :=738          add_congr_left _ (sq_osum n fun i j hi hj hij => h i j (Nat.lt_succ_of_lt hi) (Nat.lt_succ_of_lt hj) hij)739740/-- `(d g)(d' g') ≈ (d d')(g g')` when `g` commutes with `d'`. -/741theorem mul_mul_swap {d g d' g' : R} (hgd : Comm g d') : d * g * (d' * g') ≈ d * d' * (g * g') :=742  calc d * g * (d' * g') ≈ d * (g * (d' * g')) := mul_assoc _ _ _743    _ ≈ d * (g * d' * g') := mul_congr_right _ (eq_symm (mul_assoc _ _ _))744    _ ≈ d * (d' * g * g') := mul_congr_right _ (mul_congr_left _ hgd)745    _ ≈ d * (d' * (g * g')) := mul_congr_right _ (mul_assoc _ _ _)746    _ ≈ d * d' * (g * g') := eq_symm (mul_assoc _ _ _)747748/-- The summands `∇_μ γ_μ` of a Dirac operator anticommute when the differences commute with each other and with749the gammas and the gammas anticommute. -/750theorem anticomm_of_clifford {d d' g g' : R} (hdd : Comm d d') (hdg : Comm d g') (hd'g : Comm d' g)751    (hgg : Anticomm g g') : Anticomm (d * g) (d' * g') :=752  calc d * g * (d' * g') + d' * g' * (d * g) ≈ d * d' * (g * g') + d' * d * (g' * g) :=753        add_congr (mul_mul_swap hd'g.symm) (mul_mul_swap hdg.symm)754    _ ≈ d * d' * (g * g') + d * d' * (g' * g) := add_congr_right _ (mul_congr_left _ (eq_symm hdd))755    _ ≈ d * d' * (g * g' + g' * g) := eq_symm (left_distrib _ _ _)756    _ ≈ d * d' * 0 := mul_congr_right _ hgg757    _ ≈ 0 := mul_zero _758759/-- 8:D3, 8:D18 — the Dirac factorisation. For `𝒟 = Σ_{μ<n} ∇_μ γ_μ` with the differences commuting with each other760and with the gammas, the gammas anticommuting and squaring to central `η_μ`, and the mass `m` central:761`(𝒟 − m)(𝒟 + m) ≈ Σ_μ η_μ ∇_μ² − m²`. The cross terms pair into anticommutators, which vanish (`sq_osum`). -/762theorem dirac_factorisation {n : Nat} {del γ η : Nat → R} {m : R}763    (hdd : ∀ μ ν, μ < n → ν < n → Comm (del μ) (del ν)) (hdg : ∀ μ ν, μ < n → ν < n → Comm (del μ) (γ ν))764    (hgg : ∀ μ ν, μ < n → ν < n → μ ≠ ν → Anticomm (γ μ) (γ ν)) (hsq : ∀ μ, μ < n → γ μ * γ μ ≈ η μ)765    (hη : ∀ μ, μ < n → Central (η μ)) (hm : Central m) :766    (osum (fun μ => del μ * γ μ) n + -m) * (osum (fun μ => del μ * γ μ) n + m) ≈767      osum (fun μ => η μ * (del μ * del μ)) n + -(m * m) := by768  have hDD : osum (fun μ => del μ * γ μ) n * osum (fun μ => del μ * γ μ) n ≈ osum (fun μ => η μ * (del μ * del μ)) n :=769    calc osum (fun μ => del μ * γ μ) n * osum (fun μ => del μ * γ μ) n ≈ osum (fun μ => del μ * γ μ * (del μ * γ μ)) n :=770          sq_osum n fun i j hi hj hij => anticomm_of_clifford (hdd i j hi hj) (hdg i j hi hj) (hdg j i hj hi) (hgg i j hi hj hij)771      _ ≈ osum (fun μ => η μ * (del μ * del μ)) n := osum_congr n fun μ hμ =>772          calc del μ * γ μ * (del μ * γ μ) ≈ del μ * del μ * (γ μ * γ μ) := mul_mul_swap (hdg μ μ hμ hμ).symm773            _ ≈ del μ * del μ * η μ := mul_congr_right _ (hsq μ hμ)774            _ ≈ η μ * (del μ * del μ) := eq_symm (hη μ hμ _)775  calc (osum (fun μ => del μ * γ μ) n + -m) * (osum (fun μ => del μ * γ μ) n + m)776      ≈ (osum (fun μ => del μ * γ μ) n + -m) * osum (fun μ => del μ * γ μ) n + (osum (fun μ => del μ * γ μ) n + -m) * m :=777        left_distrib _ _ _778    _ ≈ osum (fun μ => del μ * γ μ) n * osum (fun μ => del μ * γ μ) n + -m * osum (fun μ => del μ * γ μ) n +779          (osum (fun μ => del μ * γ μ) n * m + -m * m) := add_congr (right_distrib _ _ _) (right_distrib _ _ _)780    _ ≈ osum (fun μ => del μ * γ μ) n * osum (fun μ => del μ * γ μ) n + -(osum (fun μ => del μ * γ μ) n * m) +781          (osum (fun μ => del μ * γ μ) n * m + -(m * m)) :=782        add_congr (add_congr_right _ (eq_trans (eq_symm (neg_mul _ _)) (neg_congr (hm _))))783          (add_congr_right _ (eq_symm (neg_mul _ _)))784    _ ≈ osum (fun μ => del μ * γ μ) n * osum (fun μ => del μ * γ μ) n +785          (-(osum (fun μ => del μ * γ μ) n * m) + osum (fun μ => del μ * γ μ) n * m + -(m * m)) :=786        eq_trans (add_assoc _ _ _) (add_congr_right _ (eq_symm (add_assoc _ _ _)))787    _ ≈ osum (fun μ => del μ * γ μ) n * osum (fun μ => del μ * γ μ) n + (0 + -(m * m)) :=788        add_congr_right _ (add_congr_left _ (neg_add _))789    _ ≈ osum (fun μ => η μ * (del μ * del μ)) n + -(m * m) := add_congr hDD (zero_add _)790791end FRC.Dirac.Operator792