Theme/Unipotent.lean — FrcCore

1import FrcCore.Theme.Operator2import FrcCore.Poly34/-!5# The unipotent file of 8-dirac — the binomial theorem and the Frobenius in characteristic `p`, no axioms67The fifth file of the dirac theme (5 November 2026, the core-proof programme): `t^p ≈ 1` forces `(t − 1)^p ≈ 0` in an8operator ring of characteristic `p` (F7's kinetic unipotency, D10's orders). The binomial coefficients `C(n, k)` by9Pascal's rule, the identity `(k+1) C(n+1, k+1) = (n+1) C(n, k)`, and `p ∣ C(p, k)` for `0 < k < p` read on the shell10`𝔽_p` with a frame as the primality witness (`k · C(p, k) = p · C(p−1, k−1)` vanishes on the shell and `k` does not,11so `C(p, k)` does, the shell having no zero divisors). The binomial theorem in an `OpRing` for commuting elements,12by Pascal's rule and the shift of a sum; in characteristic `p` (`p • 1 ≈ 0`) the middle terms vanish, so13`(x + y)^p ≈ x^p + y^p` for commuting `x`, `y`, and `t^p ≈ 1` gives `(t − 1)^p ≈ t^p + (−1)^p ≈ 0` for odd `p`. No axioms.14-/1516namespace FRC.Dirac.Operator1718/-! ## Binomial coefficients -/1920/-- `C(n, k)` by Pascal's rule. -/21def choose : Nat → Nat → Nat22  | _, 0 => 123  | 0, _ + 1 => 024  | n + 1, k + 1 => choose n k + choose n (k + 1)2526theorem choose_zero_right (n : Nat) : choose n 0 = 1 := by cases n <;> rfl27theorem choose_zero_succ (k : Nat) : choose 0 (k + 1) = 0 := rfl28theorem choose_succ_succ (n k : Nat) : choose (n + 1) (k + 1) = choose n k + choose n (k + 1) := rfl2930theorem choose_eq_zero_of_lt : ∀ n k, n < k → choose n k = 031  | 0, k + 1, _ => rfl32  | n + 1, k + 1, h => by33    rw [choose_succ_succ, choose_eq_zero_of_lt n k (Nat.lt_of_succ_lt_succ h),34      choose_eq_zero_of_lt n (k + 1) (Nat.lt_of_succ_lt h)]3536theorem choose_one : ∀ n, choose n 1 = n37  | 0 => rfl38  | n + 1 => by rw [choose_succ_succ, choose_zero_right, choose_one n, Nat.add_comm]3940/-- `(k+1) C(n+1, k+1) = (n+1) C(n, k)`. -/41theorem succ_mul_choose_succ : ∀ n k, (k + 1) * choose (n + 1) (k + 1) = (n + 1) * choose n k42  | 0, 0 => rfl43  | 0, k + 1 => by44    rw [choose_succ_succ, choose_zero_succ, choose_zero_succ, Nat.add_zero, Nat.mul_zero, Nat.mul_zero]45  | n + 1, 0 => by46    show 1 * choose (n + 1 + 1) 1 = (n + 1 + 1) * choose (n + 1) 047    rw [choose_one, choose_zero_right, Nat.one_mul, Nat.mul_one]48  | n + 1, k + 1 => by49    have h1 := succ_mul_choose_succ n k50    have h2 := succ_mul_choose_succ n (k + 1)51    rw [choose_succ_succ (n + 1) (k + 1), Nat.mul_add, h2, Nat.add_mul (k + 1) 1 (choose (n + 1) (k + 1)), Nat.one_mul,52      h1, Nat.add_mul (n + 1) 1 (choose (n + 1) (k + 1)), Nat.one_mul, choose_succ_succ n k, Nat.mul_add,53      Nat.add_right_comm]5455/-! ## `p ∣ C(p, k)` on the shell -/5657open FRC.Shell in58theorem ofNat_mul {p : Nat} [Pos p] (a b : Nat) : (ofNat (a * b) : Shell p) = ofNat a * ofNat b :=59  Shell.ext (by rw [val_mul, val_ofNat, val_ofNat, val_ofNat, FRC.Nat.mul_mod _ _ _ Pos.pos])6061open FRC.Shell in62theorem ofNat_self {p : Nat} [Pos p] : (ofNat p : Shell p) = 0 :=63  Shell.ext (by rw [val_ofNat, val_zero, FRC.Nat.mod_self _ Pos.pos])6465open FRC.Shell in66theorem ofNat_ne_zero_of {p : Nat} [Pos p] {k : Nat} (h0 : 0 < k) (hk : k < p) : (ofNat k : Shell p) ≠ 0 := fun e => by67  have := val_injective e68  rw [val_ofNat, val_zero, FRC.Nat.mod_eq_of_lt hk] at this69  exact absurd this (Nat.ne_of_gt h0)7071open FRC.Shell in72/-- `p ∣ C(p, k)` for `0 < k < p`, on the frame: `k C(p, k) = p C(p−1, k−1)` vanishes on the shell, `k` does not. -/73theorem choose_mod_prime {p κ : Nat} [Pos p] {g : Shell p} (F : Frame p κ g) {k : Nat} (h0 : 0 < k) (hk : k < p) :74    choose p k % p = 0 := by75  obtain ⟨k', rfl⟩ : ∃ k', k = k' + 1 := ⟨k - 1, (FRC.Nat.sub_add_cancel h0).symm⟩76  obtain ⟨p', hp'⟩ : ∃ p', p = p' + 1 := ⟨p - 1, (FRC.Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) hk)).symm⟩77  have hid : (k' + 1) * choose p (k' + 1) = p * choose p' k' := by rw [hp']; exact succ_mul_choose_succ p' k'78  have hsh : (ofNat (k' + 1) : Shell p) * ofNat (choose p (k' + 1)) = 0 := by79    rw [← ofNat_mul, hid, ofNat_mul, ofNat_self, Shell.zero_mul]80  rcases F.mul_eq_zero hsh with h | h81  · exact absurd h (ofNat_ne_zero_of h0 hk)82  · have := val_injective h83    rw [val_ofNat, val_zero] at this84    exact this8586/-! ## The binomial theorem in an operator ring -/8788variable {R : Type} [Add R] [Mul R] [Neg R] [OfNat R 0] [OfNat R 1] [OpRing R]8990open 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)9192omit [Add R] [Mul R] [Neg R] [OfNat R 0] [OfNat R 1] [OpRing R] in93/-- `n − (k+1) + 1 = n − k` for `k < n`. -/94theorem sub_succ_add_one {n k : Nat} (hk : k < n) : n - (k + 1) + 1 = n - k := by95  have hd := FRC.Nat.sub_add_cancel hk96  calc n - (k + 1) + 1 = n - (k + 1) + 1 + k - k := (FRC.Nat.add_sub_cancel _ _).symm97    _ = n - (k + 1) + (k + 1) - k := by rw [Nat.add_assoc, Nat.add_comm 1 k]98    _ = n - k := by rw [hd]99100/-- `x^{m n} ≈ (x^m)^n`. -/101theorem opow_mul (x : R) (m : Nat) : ∀ n, opow x (m * n) ≈ opow (opow x m) n102  | 0 => by rw [Nat.mul_zero]; exact eq_refl 1103  | n + 1 => by104    rw [Nat.mul_succ]105    exact eq_trans (opow_add x (m * n) m) (mul_congr_left _ (opow_mul x m n))106107/-- A sum split at its first term. -/108theorem osum_succ_left (f : Nat → R) : ∀ n, osum f (n + 1) ≈ f 0 + osum (fun k => f (k + 1)) n109  | 0 => eq_trans (zero_add _) (eq_symm (add_zero _))110  | n + 1 =>111    calc osum f (n + 1) + f (n + 1) ≈ f 0 + osum (fun k => f (k + 1)) n + f (n + 1) :=112          add_congr_left _ (osum_succ_left f n)113      _ ≈ f 0 + (osum (fun k => f (k + 1)) n + f (n + 1)) := add_assoc _ _ _114115/-- The binomial sum `Σ_{k≤n} C(n, k) x^k y^{n−k}`. -/116def binom (x y : R) (n : Nat) : R := osum (fun k => nsmul (choose n k) (opow x k * opow y (n - k))) (n + 1)117118/-- The binomial theorem for commuting `x`, `y`: `(x + y)^n ≈ Σ_{k≤n} C(n, k) x^k y^{n−k}`. -/119theorem binomial {x y : R} (h : Comm x y) : ∀ n, opow (x + y) n ≈ binom x y n120  | 0 =>121    calc (1 : R) ≈ 1 + 0 := eq_symm (add_zero 1)122      _ ≈ 0 + 1 := add_comm _ _123      _ ≈ 0 + nsmul 1 (1 * 1) := add_congr_right _ (eq_symm (eq_trans (zero_add _) (one_mul 1)))124  | n + 1 => by125    -- `(x+y)^{n+1} = binom n · x + binom n · y`126    have hyx : ∀ j, Comm (opow y j) x := fun j => opow_comm h.symm j127    have hstep : opow (x + y) (n + 1) ≈ binom x y n * x + binom x y n * y :=128      calc opow (x + y) n * (x + y) ≈ binom x y n * (x + y) := mul_congr_left _ (binomial h n)129        _ ≈ binom x y n * x + binom x y n * y := left_distrib _ _ _130    -- the two products, term by term131    have hbx : binom x y n * x ≈ osum (fun k => nsmul (choose n k) (opow x (k + 1) * opow y (n - k))) (n + 1) :=132      eq_trans (osum_mul_right _ _ _) (osum_congr _ fun k _ =>133        calc nsmul (choose n k) (opow x k * opow y (n - k)) * x ≈ nsmul (choose n k) (opow x k * opow y (n - k) * x) :=134              nsmul_mul_left _ _ _135          _ ≈ nsmul (choose n k) (opow x k * (opow y (n - k) * x)) := nsmul_congr (mul_assoc _ _ _) _136          _ ≈ nsmul (choose n k) (opow x k * (x * opow y (n - k))) := nsmul_congr (mul_congr_right _ (hyx _)) _137          _ ≈ nsmul (choose n k) (opow x k * x * opow y (n - k)) := nsmul_congr (eq_symm (mul_assoc _ _ _)) _)138    have hby : binom x y n * y ≈ osum (fun k => nsmul (choose n k) (opow x k * opow y (n - k + 1))) (n + 1) :=139      eq_trans (osum_mul_right _ _ _) (osum_congr _ fun k _ =>140        calc nsmul (choose n k) (opow x k * opow y (n - k)) * y ≈ nsmul (choose n k) (opow x k * opow y (n - k) * y) :=141              nsmul_mul_left _ _ _142          _ ≈ nsmul (choose n k) (opow x k * (opow y (n - k) * y)) := nsmul_congr (mul_assoc _ _ _) _)143    -- the target, split at its first term and expanded by Pascal's rule144    have htarget : binom x y (n + 1) ≈145        opow y (n + 1) + (osum (fun k => nsmul (choose n k) (opow x (k + 1) * opow y (n - k))) (n + 1) +146          osum (fun k => nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))) (n + 1)) :=147      calc binom x y (n + 1) ≈ nsmul (choose (n + 1) 0) (opow x 0 * opow y (n + 1 - 0)) +148            osum (fun k => nsmul (choose (n + 1) (k + 1)) (opow x (k + 1) * opow y (n + 1 - (k + 1)))) (n + 1) :=149            osum_succ_left _ _150        _ ≈ opow y (n + 1) + osum (fun k => nsmul (choose n k) (opow x (k + 1) * opow y (n - k)) +151              nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))) (n + 1) := by152            refine add_congr ?_ (osum_congr _ fun k _ => ?_)153            · show nsmul 1 (1 * opow y (n + 1)) ≈ opow y (n + 1)154              exact eq_trans (zero_add _) (one_mul _)155            · rw [Nat.succ_sub_succ n k, choose_succ_succ]156              exact add_nsmul _ _ _157        _ ≈ opow y (n + 1) + (osum (fun k => nsmul (choose n k) (opow x (k + 1) * opow y (n - k))) (n + 1) +158              osum (fun k => nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))) (n + 1)) :=159            add_congr_right _ (osum_add _ _ _)160    -- `binom n · y` is the first target term plus the second sum: shift, and the last term of the second sum vanishes161    have hshift : osum (fun k => nsmul (choose n k) (opow x k * opow y (n - k + 1))) (n + 1) ≈162        opow y (n + 1) + osum (fun k => nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))) (n + 1) :=163      calc osum (fun k => nsmul (choose n k) (opow x k * opow y (n - k + 1))) (n + 1)164          ≈ nsmul (choose n 0) (opow x 0 * opow y (n - 0 + 1)) +165              osum (fun k => nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - (k + 1) + 1))) n :=166            osum_succ_left _ _167        _ ≈ opow y (n + 1) + osum (fun k => nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))) n := by168            refine add_congr ?_ (osum_congr _ fun k hk => ?_)169            · rw [choose_zero_right, Nat.sub_zero]170              show nsmul 1 (1 * opow y (n + 1)) ≈ opow y (n + 1)171              exact eq_trans (zero_add _) (one_mul _)172            · show nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - (k + 1) + 1)) ≈173                nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))174              rw [sub_succ_add_one hk]175              exact eq_refl _176        _ ≈ opow y (n + 1) + (osum (fun k => nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))) n +177              nsmul (choose n (n + 1)) (opow x (n + 1) * opow y (n - n))) := by178            refine add_congr_right _ (eq_symm (eq_trans (add_congr_right _ ?_) (add_zero _)))179            rw [choose_eq_zero_of_lt n (n + 1) (Nat.lt_succ_self n)]180            exact eq_refl _181    calc opow (x + y) (n + 1) ≈ binom x y n * x + binom x y n * y := hstep182      _ ≈ osum (fun k => nsmul (choose n k) (opow x (k + 1) * opow y (n - k))) (n + 1) +183            (opow y (n + 1) + osum (fun k => nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))) (n + 1)) :=184          add_congr hbx (eq_trans hby hshift)185      _ ≈ opow y (n + 1) + (osum (fun k => nsmul (choose n k) (opow x (k + 1) * opow y (n - k))) (n + 1) +186            osum (fun k => nsmul (choose n (k + 1)) (opow x (k + 1) * opow y (n - k))) (n + 1)) :=187          add_left_comm _ _ _188      _ ≈ binom x y (n + 1) := eq_symm htarget189190theorem choose_self : ∀ n, choose n n = 1191  | 0 => rfl192  | n + 1 => by rw [choose_succ_succ, choose_self n, choose_eq_zero_of_lt n (n + 1) (Nat.lt_succ_self n)]193194/-! ## Characteristic `p` and the Frobenius -/195196/-- The middle binomial coefficients vanish in characteristic `p` (`p • 1 ≈ 0`) on the frame's shell. -/197theorem nsmul_choose_prime {p κ : Nat} [Pos p] {g : Shell p} (F : Shell.Frame p κ g) (hch : nsmul p (1 : R) ≈ 0)198    {k : Nat} (h0 : 0 < k) (hk : k < p) (z : R) : nsmul (choose p k) z ≈ 0 := by199  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec p Pos.pos (choose p k)200  rw [choose_mod_prime F h0 hk, Nat.add_zero] at hq201  calc nsmul (choose p k) z ≈ nsmul (p * q) z := eq_of_eq (by rw [← hq])202    _ ≈ nsmul p (nsmul q z) := mul_nsmul _ _ _203    _ ≈ nsmul p 1 * nsmul q z := nsmul_eq_mul_one _ _204    _ ≈ 0 * nsmul q z := mul_congr_left _ hch205    _ ≈ 0 := zero_mul _206207/-- The Frobenius is additive on commuting elements in characteristic `p`: `(x + y)^p ≈ x^p + y^p`. -/208theorem frobenius_add {p κ : Nat} [Pos p] {g : Shell p} (F : Shell.Frame p κ g) (hch : nsmul p (1 : R) ≈ 0) {x y : R}209    (h : Comm x y) : opow (x + y) p ≈ opow x p + opow y p := by210  obtain ⟨p', hp'⟩ : ∃ p', p = p' + 1 := ⟨p - 1, (FRC.Nat.sub_add_cancel (Pos.pos : 0 < p)).symm⟩211  have hmid : ∀ k, k < p' → nsmul (choose p (k + 1)) (opow x (k + 1) * opow y (p - (k + 1))) ≈ 0 := fun k hk =>212    nsmul_choose_prime F hch (Nat.zero_lt_succ k) (hp' ▸ Nat.succ_lt_succ hk) _213  calc opow (x + y) p ≈ binom x y p := binomial h p214    _ ≈ nsmul (choose p 0) (opow x 0 * opow y (p - 0)) +215          osum (fun k => nsmul (choose p (k + 1)) (opow x (k + 1) * opow y (p - (k + 1)))) p := osum_succ_left _ _216    _ ≈ opow y p + (osum (fun k => nsmul (choose p (k + 1)) (opow x (k + 1) * opow y (p - (k + 1)))) p' +217          nsmul (choose p (p' + 1)) (opow x (p' + 1) * opow y (p - (p' + 1)))) := by218        refine add_congr ?_ (eq_of_eq (by rw [hp']; rfl))219        rw [choose_zero_right, Nat.sub_zero]220        show nsmul 1 (1 * opow y p) ≈ opow y p221        exact eq_trans (zero_add _) (one_mul _)222    _ ≈ opow y p + (0 + opow x p) := by223        refine add_congr_right _ (add_congr (osum_eq_zero p' hmid) ?_)224        rw [← hp', choose_self, Nat.sub_self]225        show nsmul 1 (opow x p * 1) ≈ opow x p226        exact eq_trans (zero_add _) (mul_one _)227    _ ≈ opow x p + opow y p := eq_trans (add_congr_right _ (zero_add _)) (add_comm _ _)228229/-- `(−1)^{2j} ≈ 1` and `(−1)^{2j+1} ≈ −1`. -/230theorem opow_neg_one_even : ∀ j, opow (-1 : R) (2 * j) ≈ 1231  | 0 => eq_refl 1232  | j + 1 => by233    rw [Nat.mul_succ]234    calc opow (-1 : R) (2 * j + 1) * -1 ≈ opow (-1 : R) (2 * j) * -1 * -1 := eq_refl _235      _ ≈ 1 * -1 * -1 := mul_congr_left _ (mul_congr_left _ (opow_neg_one_even j))236      _ ≈ -1 * -1 := mul_congr_left _ (one_mul _)237      _ ≈ 1 * 1 := neg_mul_neg _ _238      _ ≈ 1 := one_mul 1239240theorem opow_neg_one_odd (j : Nat) : opow (-1 : R) (2 * j + 1) ≈ -1 :=241  eq_trans (mul_congr_left _ (opow_neg_one_even j)) (one_mul _)242243/-- 8:F7, 8:D10 — the translations are unipotent: on the frame's shell (`p = 4κ + 1`), in characteristic `p`,244`t^p ≈ 1` gives `(t − 1)^p ≈ t^p + (−1)^p ≈ 1 − 1 ≈ 0` (`t` and `−1` commute; the Frobenius is additive). -/245theorem translation_nilpotent {p κ : Nat} [Pos p] {g : Shell p} (F : Shell.Frame p κ g) (hch : nsmul p (1 : R) ≈ 0)246    {t : R} (ht : opow t p ≈ 1) : opow (t + -1) p ≈ 0 := by247  have hodd : opow (-1 : R) p ≈ -1 := by248    have : p = 2 * (2 * κ) + 1 := by rw [F.cap, ← Nat.mul_assoc]249    rw [this]; exact opow_neg_one_odd _250  calc opow (t + -1) p ≈ opow t p + opow (-1) p := frobenius_add F hch (Comm.neg_right (Comm.one_left t).symm)251    _ ≈ 1 + -1 := add_congr ht hodd252    _ ≈ 0 := add_neg 1253254/-- 8:D10 — a unipotent step has order dividing `p`: `(u − 1)^p ≈ 0` gives `u^p ≈ 1`, and a phase times a255unipotent, `u ≈ φ + N` with `φ` central and `N^p ≈ 0`, `N` commuting with `φ`, has `u^p ≈ φ^p`. -/256theorem opow_of_nilpotent_shift {p κ : Nat} [Pos p] {g : Shell p} (F : Shell.Frame p κ g) (hch : nsmul p (1 : R) ≈ 0)257    {u φ N : R} (hu : u ≈ φ + N) (hφ : Comm φ N) (hN : opow N p ≈ 0) : opow u p ≈ opow φ p :=258  calc opow u p ≈ opow (φ + N) p := opow_congr hu p259    _ ≈ opow φ p + opow N p := frobenius_add F hch hφ260    _ ≈ opow φ p + 0 := add_congr_right _ hN261    _ ≈ opow φ p := add_zero _262263end FRC.Dirac.Operator264