Theme/Elim.lean — FrcCore

1import FrcCore.Theme.Det2import FrcCore.Theme.Packed3/-!4# FrcCore.Theme.Elim — Gaussian elimination over the coefficient field (the operator theme)56The computation of the determinant of `Theme/Det`: the first-column lemma (`det M = M₀₀ · det (minor 0)` when the7heads below vanish), the clearing of the first column by iterated row additions with the pivot's inverse, the pivot8search, and `detG` with the row count as fuel, equal to `det` on square matrices over `K` (`detG_eq_det`), on the frame9with `ν` a nonsquare. The inverse of a nonzero residue is `x^(p−2)` (Fermat, `mul_invF`), the inverse in `K` the10conjugate over the norm (`mul_inv`), the norm nonzero by the anisotropy of the quadratic form. The kernel decides11determinants through `detG`: `n³` field operations where the expansion would take `n!`. `Theme/Cayley.lean` applies the kernel criterion12to the Cayley denominator `I − αH` of 8-dirac. No axioms.13-/14namespace FRC.Dirac.Det1516open FRC FRC.Extension FRC.Dirac FRC.Dirac.Hermitian17open FRC.Dirac.Mat (nth)1819variable {p : Nat} [Pos p] {ν : Shell p}2021/-! ## The first column -/2223/-- When every row below the first has head zero, the determinant is the first head times the first minor. -/24theorem det_first_col (M : Mat p ν) (hM : 0 < M.length) (h : ∀ i, 0 < i → i < M.length → head (row M i) = 0) :25    det M = head (row M 0) * det (minor M 0) := by26  rw [det_expand M hM, length_form_one hM, Nat.add_comm (M.length - 1) 1, ← sumFrom_split _ 1 (M.length - 1) 0]27  show term det M 0 + 0 + sumFrom (term det M) (M.length - 1) (0 + 1) = _28  rw [add_zero, show sumFrom (term det M) (M.length - 1) (0 + 1) = 0 by29    rw [← sumFrom_zero_fn (M.length - 1) (0 + 1)]30    exact sumFrom_congr _ _ fun j hj hj' => by31      unfold term32      rw [h j hj (by rw [length_form_one hM, Nat.add_comm]; exact hj'), mul_zero, zero_mul]]33  unfold term; rw [add_zero, show (sgn 0 : Ext p ν) = 1 from rfl, Ext.one_mul]3435/-- A zero first column: the determinant vanishes. -/36theorem det_zero_col (M : Mat p ν) (hM : 0 < M.length) (h : ∀ i, i < M.length → head (row M i) = 0) : det M = 0 := by37  rw [det_first_col M hM fun i _ hi => h i hi, h 0 hM, zero_mul]3839/-! ## Clearing the first column below the pivot -/4041/-- Row `k` with `−(head k · ainv)` times row `0` added. -/42def clearRow (M : Mat p ν) (ainv : Ext p ν) (k : Nat) : Mat p ν :=43  setAt M k (radd (row M k) (rsmul (-(head (row M k) * ainv)) (row M 0)))4445/-- Rows `1 … k` cleared in turn. -/46def clearUpto (ainv : Ext p ν) : Nat → Mat p ν → Mat p ν47  | 0, M => M48  | k + 1, M => clearRow (clearUpto ainv k M) ainv (k + 1)4950theorem length_clearRow (M : Mat p ν) (ainv : Ext p ν) (k : Nat) : (clearRow M ainv k).length = M.length := length_setAt _ _ _51theorem length_clearUpto (ainv : Ext p ν) : ∀ (k : Nat) (M : Mat p ν), (clearUpto ainv k M).length = M.length52  | 0, _ => rfl53  | k + 1, M => (length_clearRow _ _ _).trans (length_clearUpto ainv k M)5455theorem square_setAt (M : Mat p ν) (hS : Square M) (i : Nat) (r : List (Ext p ν)) (hr : r.length = M.length) :56    Square (setAt M i r) := fun j hj => by57  rw [length_setAt] at hj ⊢58  match Nat.decEq i j with59  | .isTrue e => subst e; rw [row_setAt_eq _ _ _ hj]; exact hr60  | .isFalse e => rw [row_setAt_ne _ _ _ _ e]; exact hS j hj6162theorem square_clearRow (M : Mat p ν) (hS : Square M) (ainv : Ext p ν) (k : Nat) (hk : k < M.length) (h0 : 0 < M.length) :63    Square (clearRow M ainv k) :=64  square_setAt M hS k _ (by rw [length_radd _ _ (by rw [length_rsmul]; exact (hS k hk).trans (hS 0 h0).symm)]; exact hS k hk)6566theorem square_clearUpto (ainv : Ext p ν) : ∀ (k : Nat) (M : Mat p ν), Square M → k < M.length → Square (clearUpto ainv k M)67  | 0, _, hS, _ => hS68  | k + 1, M, hS, hk =>69    square_clearRow _ (square_clearUpto ainv k M hS (Nat.lt_of_succ_lt hk)) ainv (k + 1)70      (by rw [length_clearUpto]; exact hk) (by rw [length_clearUpto]; exact Nat.lt_of_le_of_lt (Nat.zero_le _) hk)7172/-- Clearing rows `1 … k` leaves the determinant unchanged. -/73theorem det_clearUpto (ainv : Ext p ν) : ∀ (k : Nat) (M : Mat p ν), Square M → k < M.length → det (clearUpto ainv k M) = det M74  | 0, _, _, _ => rfl75  | k + 1, M, hS, hk => by76    show det (clearRow (clearUpto ainv k M) ainv (k + 1)) = det M77    unfold clearRow78    rw [det_addRow _ (square_clearUpto ainv k M hS (Nat.lt_of_succ_lt hk)) (k + 1) 0 (Nat.succ_ne_zero k)79      (by rw [length_clearUpto]; exact hk) (by rw [length_clearUpto]; exact Nat.lt_of_le_of_lt (Nat.zero_le _) hk)]80    exact det_clearUpto ainv k M hS (Nat.lt_of_succ_lt hk)8182/-- Rows beyond `k`, and row `0`, are untouched. -/83theorem row_clearUpto_of_lt (ainv : Ext p ν) : ∀ (k : Nat) (M : Mat p ν) (i : Nat), k < i → row (clearUpto ainv k M) i = row M i84  | 0, _, _, _ => rfl85  | k + 1, M, i, h => by86    show row (clearRow (clearUpto ainv k M) ainv (k + 1)) i = row M i87    unfold clearRow88    rw [row_setAt_ne _ _ _ _ (Nat.ne_of_lt h)]; exact row_clearUpto_of_lt ainv k M i (Nat.lt_of_succ_lt h)89theorem row_clearUpto_zero (ainv : Ext p ν) : ∀ (k : Nat) (M : Mat p ν), row (clearUpto ainv k M) 0 = row M 090  | 0, _ => rfl91  | k + 1, M => by92    show row (clearRow (clearUpto ainv k M) ainv (k + 1)) 0 = row M 093    unfold clearRow94    rw [row_setAt_ne _ _ _ _ (Nat.succ_ne_zero k)]; exact row_clearUpto_zero ainv k M9596/-- With `ainv` the inverse of the first head, the cleared rows have head zero. -/97theorem head_clearUpto (ainv : Ext p ν) (M : Mat p ν) (hS : Square M) (ha : head (row M 0) * ainv = 1) :98    ∀ (k : Nat), k < M.length → ∀ i, 0 < i → i ≤ k → head (row (clearUpto ainv k M) i) = 099  | 0, _, _, hi, hik => absurd (Nat.lt_of_lt_of_le hi hik) (Nat.lt_irrefl 0)100  | k + 1, hk, i, hi, hik => by101    show head (row (clearRow (clearUpto ainv k M) ainv (k + 1)) i) = 0102    unfold clearRow103    match Nat.decEq (k + 1) i with104    | .isTrue e =>105      subst e106      rw [row_setAt_eq _ _ _ (by rw [length_clearUpto]; exact hk), row_clearUpto_zero,107        row_clearUpto_of_lt ainv k M (k + 1) (Nat.lt_succ_self k),108        head_radd _ _ (by rw [length_rsmul]; exact (hS (k + 1) hk).trans (hS 0 (Nat.lt_of_le_of_lt (Nat.zero_le _) hk)).symm),109        head_rsmul, ← Hermitian.neg_mul, Ext.mul_assoc, Ext.mul_comm ainv, ha, Ext.mul_one, add_neg]110    | .isFalse e =>111      rw [row_setAt_ne _ _ _ _ e]112      exact head_clearUpto ainv M hS ha k (Nat.lt_of_succ_lt hk) i hi (Nat.lt_of_le_of_ne hik (Ne.symm e) |> Nat.le_of_lt_succ)113114/-! ## Inverses on the frame -/115116open FRC.Shell (Frame)117open FRC.Shell.Frame (IsSquare aniso_tx)118119/-- Powers by repeated squaring, with fuel: `powBin a f n = a ^ n` once `f ≥ log₂ n` (`powBin_eq` for every `f`), and the120kernel unfolds `log₂ n` levels where `Shell.pow` unfolds `n`. -/121def powBin : Shell p → Nat → Nat → Shell p122  | a, 0, n => a ^ n123  | _, _ + 1, 0 => 1124  | a, f + 1, n + 1 => (if (n + 1) % 2 = 1 then a else 1) * powBin (a * a) f ((n + 1) / 2)125126theorem lt_two_cases : ∀ r : Nat, r < 2 → r = 0 ∨ r = 1127  | 0, _ => Or.inl rfl128  | 1, _ => Or.inr rfl129  | _ + 2, h => absurd h (Nat.not_lt_of_le (Nat.le_add_left 2 _))130131theorem pow_two' (a : Shell p) : a ^ 2 = a * a := by rw [Shell.pow_succ, Shell.pow_one]132133theorem powBin_eq (a : Shell p) : ∀ (f n : Nat), powBin a f n = a ^ n134  | 0, _ => rfl135  | _ + 1, 0 => rfl136  | f + 1, n + 1 => by137    show (if (n + 1) % 2 = 1 then a else 1) * powBin (a * a) f ((n + 1) / 2) = a ^ (n + 1)138    rw [powBin_eq (a * a) f, ← pow_two', ← Shell.pow_mul]139    have e := FRC.Dirac.Packed.div_add_mod' 2 (by decide) (n + 1)140    match lt_two_cases _ (Nat.mod_lt (n + 1) (by decide)) with141    | Or.inl h0 =>142      rw [h0, ite_eq_right (by decide), Shell.one_mul]; rw [h0, Nat.add_zero] at e; exact congrArg (a ^ ·) e.symm143    | Or.inr h1 =>144      rw [h1, ite_eq_left rfl, Shell.mul_comm, ← Shell.pow_succ]; rw [h1] at e; exact congrArg (a ^ ·) e.symm145146/-- The inverse of a nonzero residue, `x^(p−2)` (Fermat), computed by repeated squaring; `0` at `0`. -/147def invF (x : Shell p) : Shell p := powBin x p (p - 2)148149theorem invF_eq_pow (x : Shell p) : invF x = x ^ (p - 2) := powBin_eq x p (p - 2)150151theorem mul_invF {κ : Nat} {g : Shell p} (F : Frame p κ g) {x : Shell p} (hx : x ≠ 0) : x * invF x = 1 := by152  rw [invF_eq_pow]153  obtain ⟨y, hy⟩ := F.exists_inv hx154  have h2 : 2 ≤ p := F.one_lt_p155  have h1 : p - 2 + 1 = p - 1 := by156    have := FRC.Nat.sub_add_cancel h2157    calc p - 2 + 1 = p - 2 + 2 - 1 := rfl158      _ = p - 1 := by rw [this]159  have hp : p - 1 + 1 = p := FRC.Nat.sub_add_cancel (Nat.le_of_lt F.one_lt_p)160  show x * x ^ (p - 2) = 1161  rw [Shell.mul_comm, ← Shell.pow_succ, h1, ← Shell.mul_one (x ^ (p - 1)), ← hy, ← Shell.mul_assoc, ← Shell.pow_succ,162    hp, F.fermat x, hy]163164/-- The inverse in `K`: the conjugate over the norm. -/165def inv (z : Ext p ν) : Ext p ν := Ext.conj z * Ext.ofShell (invF (Ext.norm z))166167theorem norm_ne_zero {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) {z : Ext p ν} (hz : z ≠ 0) :168    Ext.norm z ≠ 0 := fun h => by169  have e : z.re * z.re = ν * (z.im * z.im) := by170    have := Shell.eq_neg_of_add_eq_zero h171    rw [Shell.neg_neg] at this; exact this172  obtain ⟨hi, hr⟩ := aniso_tx F hν e173  exact hz (Ext.ext hr hi)174175theorem mul_inv {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) {z : Ext p ν} (hz : z ≠ 0) : z * inv z = 1 := by176  show z * (Ext.conj z * Ext.ofShell (invF (Ext.norm z))) = 1177  rw [← Ext.mul_assoc, Ext.mul_conj, Ext.ofShell_mul, mul_invF F (norm_ne_zero F hν hz)]; rfl178179/-! ## The pivot and Gaussian elimination -/180181/-- The least row index `≥ i` with a nonzero head, within `f` rows. -/182def pivotAux (M : Mat p ν) : Nat → Nat → Option Nat183  | 0, _ => none184  | f + 1, i => if head (row M i) = 0 then pivotAux M f (i + 1) else some i185186theorem pivotAux_none (M : Mat p ν) : ∀ (f i : Nat), pivotAux M f i = none → ∀ j, i ≤ j → j < i + f → head (row M j) = 0187  | 0, _, _, _, hj, hj' => absurd (Nat.lt_of_le_of_lt hj hj') (Nat.lt_irrefl _)188  | f + 1, i, h, j, hj, hj' => by189    unfold pivotAux at h190    match decEq (head (row M i)) 0 with191    | .isTrue e =>192      rw [ite_eq_left e] at h193      match Nat.decEq i j with194      | .isTrue e' => subst e'; exact e195      | .isFalse e' =>196        exact pivotAux_none M f (i + 1) h j (Nat.lt_of_le_of_ne hj e') (Nat.add_right_comm i 1 f ▸ hj')197    | .isFalse e => rw [ite_eq_right e] at h; exact nomatch h198199theorem pivotAux_some (M : Mat p ν) : ∀ (f i k : Nat), pivotAux M f i = some k →200    i ≤ k ∧ k < i + f ∧ head (row M k) ≠ 0 ∧ ∀ j, i ≤ j → j < k → head (row M j) = 0201  | 0, _, _, h => nomatch h202  | f + 1, i, k, h => by203    unfold pivotAux at h204    match decEq (head (row M i)) 0 with205    | .isTrue e =>206      rw [ite_eq_left e] at h207      obtain ⟨h1, h2, h3, h4⟩ := pivotAux_some M f (i + 1) k h208      refine ⟨Nat.le_of_succ_le h1, Nat.add_right_comm i 1 f ▸ h2, h3, fun j hj hjk => ?_⟩209      match Nat.decEq i j with210      | .isTrue e' => subst e'; exact e211      | .isFalse e' => exact h4 j (Nat.lt_of_le_of_ne hj e') hjk212    | .isFalse e =>213      rw [ite_eq_right e] at h214      cases h215      exact ⟨Nat.le_refl i, Nat.lt_add_of_pos_right (Nat.succ_pos f), e,216        fun j hj hjk => absurd (Nat.lt_of_le_of_lt hj hjk) (Nat.lt_irrefl _)⟩217218/-- The matrix with row `k` added to row `0` when `k ≠ 0`, so that its first head is the pivot. -/219def pivotFix (M : Mat p ν) : Nat → Mat p ν220  | 0 => M221  | k + 1 => setAt M 0 (radd (row M 0) (rsmul 1 (row M (k + 1))))222223/-- Gaussian elimination along the first column, the row count as fuel: the determinant with `n³` operations. -/224def detG : Nat → Mat p ν → Ext p ν225  | 0, _ => 1226  | n + 1, M =>227    match pivotAux M (n + 1) 0 with228    | none => 0229    | some k =>230      let M' := pivotFix M k231      let a := head (row M' 0)232      a * detG n (minor (clearUpto (inv a) n M') 0)233234theorem length_tail_of_pos {α : Type} : ∀ (l : List α), 0 < l.length → l.tail.length + 1 = l.length235  | [], h => absurd h (Nat.lt_irrefl 0)236  | _ :: _, _ => rfl237238theorem square_minor (M : Mat p ν) (hS : Square M) (j : Nat) (hj : j < M.length) : Square (minor M j) := fun i hi => by239  have hl := length_minor M j hj240  have hiM : i + 1 < M.length := by rw [← hl]; exact Nat.succ_lt_succ hi241  match Nat.decLt i j with242  | .isTrue hij =>243    rw [row_minor_lt M j i hij]244    exact Nat.succ.inj ((length_tail_of_pos _ (by rw [hS i (Nat.lt_of_succ_lt hiM)]; exact Nat.lt_of_le_of_lt (Nat.zero_le _) hiM)).trans245      ((hS i (Nat.lt_of_succ_lt hiM)).trans hl.symm))246  | .isFalse hij =>247    rw [row_minor_ge M j i (Nat.le_of_not_lt hij)]248    exact Nat.succ.inj ((length_tail_of_pos _ (by rw [hS (i + 1) hiM]; exact Nat.lt_of_le_of_lt (Nat.zero_le _) hiM)).trans249      ((hS (i + 1) hiM).trans hl.symm))250251theorem length_pivotFix (M : Mat p ν) : ∀ k, (pivotFix M k).length = M.length252  | 0 => rfl253  | _ + 1 => length_setAt _ _ _254255theorem square_pivotFix (M : Mat p ν) (hS : Square M) : ∀ k, k < M.length → Square (pivotFix M k)256  | 0, _ => hS257  | k + 1, hk =>258    square_setAt M hS 0 _ (by259      rw [length_radd _ _ (by rw [length_rsmul]; exact (hS 0 (Nat.lt_of_le_of_lt (Nat.zero_le _) hk)).trans (hS (k + 1) hk).symm)]260      exact hS 0 (Nat.lt_of_le_of_lt (Nat.zero_le _) hk))261262theorem det_pivotFix (M : Mat p ν) (hS : Square M) : ∀ k, k < M.length → det (pivotFix M k) = det M263  | 0, _ => rfl264  | k + 1, hk => det_addRow M hS 0 (k + 1) (Nat.succ_ne_zero k).symm (Nat.lt_of_le_of_lt (Nat.zero_le _) hk) hk 1265266theorem head_pivotFix (M : Mat p ν) (hS : Square M) : ∀ k, k < M.length → (∀ j, j < k → head (row M j) = 0) →267    head (row (pivotFix M k) 0) = head (row M k)268  | 0, _, _ => rfl269  | k + 1, hk, h0 => by270    show head (row (setAt M 0 _) 0) = _271    rw [row_setAt_eq _ _ _ (Nat.lt_of_le_of_lt (Nat.zero_le _) hk),272      head_radd _ _ (by rw [length_rsmul]; exact (hS 0 (Nat.lt_of_le_of_lt (Nat.zero_le _) hk)).trans (hS (k + 1) hk).symm),273      head_rsmul, h0 0 (Nat.succ_pos k), zero_add, Ext.one_mul]274275/-- The elimination computes the determinant. -/276theorem detG_eq_det {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) :277    ∀ (n : Nat) (M : Mat p ν), Square M → M.length = n → detG n M = det M278  | 0, [], _, _ => rfl279  | 0, _ :: _, _, h => absurd h (Nat.succ_ne_zero _)280  | n + 1, M, hS, hM => by281    have hpos : 0 < M.length := hM ▸ Nat.succ_pos n282    show (match pivotAux M (n + 1) 0 with283      | none => 0284      | some k => head (row (pivotFix M k) 0) * detG n (minor (clearUpto (inv (head (row (pivotFix M k) 0))) n (pivotFix M k)) 0)) = det M285    match hpiv : pivotAux M (n + 1) 0 with286    | none =>287      show (0 : Ext p ν) = det M288      exact (det_zero_col M hpos fun i hi => pivotAux_none M (n + 1) 0 hpiv i (Nat.zero_le i) (by rw [Nat.zero_add, ← hM]; exact hi)).symm289    | some k =>290      show head (row (pivotFix M k) 0) * detG n (minor (clearUpto (inv (head (row (pivotFix M k) 0))) n (pivotFix M k)) 0) = det M291      obtain ⟨_, hk, hk0, hleast⟩ := pivotAux_some M (n + 1) 0 k hpiv292      have hkM : k < M.length := by rw [hM]; exact Nat.lt_of_lt_of_eq hk (Nat.zero_add _)293      have hS' : Square (pivotFix M k) := square_pivotFix M hS k hkM294      have hlen' : (pivotFix M k).length = n + 1 := (length_pivotFix M k).trans hM295      have ha : head (row (pivotFix M k) 0) ≠ 0 := by296        rw [head_pivotFix M hS k hkM fun j hj => hleast j (Nat.zero_le j) hj]; exact hk0297      have hinv := mul_inv F hν ha298      have hn : n < (pivotFix M k).length := by rw [hlen']; exact Nat.lt_succ_self n299      have hC : Square (clearUpto (inv (head (row (pivotFix M k) 0))) n (pivotFix M k)) := square_clearUpto _ n _ hS' hn300      have hCl : (clearUpto (inv (head (row (pivotFix M k) 0))) n (pivotFix M k)).length = n + 1 := (length_clearUpto _ _ _).trans hlen'301      rw [detG_eq_det F hν n _ (square_minor _ hC 0 (hCl ▸ Nat.succ_pos n))302        (Nat.succ.inj (show (minor _ 0).length + 1 = n + 1 by rw [length_minor _ 0 (hCl ▸ Nat.succ_pos n)]; exact hCl)),303        ← det_pivotFix M hS k hkM, ← det_clearUpto (inv (head (row (pivotFix M k) 0))) n _ hS' hn,304        det_first_col _ (hCl ▸ Nat.succ_pos n) (fun i hi hi' => head_clearUpto _ _ hS' hinv n hn i hi305          (Nat.le_of_lt_succ (Nat.lt_of_lt_of_eq hi' hCl))), row_clearUpto_zero]306307/-! ## The kernel: the determinant vanishes exactly on the singular matrices -/308309/-- The dot product of two lists (the shorter one decides). -/310def dotL : List (Ext p ν) → List (Ext p ν) → Ext p ν311  | [], _ => 0312  | _ :: _, [] => 0313  | a :: r, x :: v => a * x + dotL r v314315/-- `v` lies in the kernel of `M`: every row is orthogonal to it. -/316def InKer (M : Mat p ν) (v : List (Ext p ν)) : Prop := ∀ j, dotL (row M j) v = 0317/-- The zero vector, entrywise. -/318def IsZero (v : List (Ext p ν)) : Prop := ∀ i, nth 0 v i = 0319320theorem dotL_nil_right : ∀ r : List (Ext p ν), dotL r [] = 0321  | [] => rfl322  | _ :: _ => rfl323324theorem dotL_radd : ∀ (r s v : List (Ext p ν)), r.length = s.length → dotL (radd r s) v = dotL r v + dotL s v325  | [], [], _, _ => (add_zero _).symm326  | [], _ :: _, _, h => absurd h (Nat.ne_of_lt (Nat.succ_pos _))327  | _ :: _, [], _, h => absurd h (Nat.ne_of_gt (Nat.succ_pos _))328  | _ :: _, _ :: _, [], _ => (add_zero _).symm329  | a :: r, b :: s, x :: v, h => by330    show (a + b) * x + dotL (radd r s) v = a * x + dotL r v + (b * x + dotL s v)331    rw [dotL_radd r s v (Nat.succ.inj h), add_mul, add_add_add_comm]332333theorem dotL_rsmul (c : Ext p ν) : ∀ (r v : List (Ext p ν)), dotL (rsmul c r) v = c * dotL r v334  | [], _ => (mul_zero c).symm335  | _ :: _, [] => (mul_zero c).symm336  | a :: r, x :: v => by337    show c * a * x + dotL (rsmul c r) v = c * (a * x + dotL r v)338    rw [dotL_rsmul c r v, mul_add, Ext.mul_assoc]339340theorem dotL_cons_head : ∀ (r : List (Ext p ν)) (x : Ext p ν) (w : List (Ext p ν)), 0 < r.length →341    dotL r (x :: w) = head r * x + dotL r.tail w342  | [], _, _, h => absurd h (Nat.lt_irrefl 0)343  | _ :: _, _, _, _ => rfl344345theorem inKer_setAt_iff (M : Mat p ν) (i k : Nat) (hik : i ≠ k) (c : Ext p ν) (v : List (Ext p ν)) (hi : i < M.length)346    (hl : (row M i).length = (row M k).length) :347    InKer (setAt M i (radd (row M i) (rsmul c (row M k)))) v ↔ InKer M v := by348  constructor349  · intro h j350    match Nat.decEq i j with351    | .isTrue e =>352      subst e353      have hk := h k354      have hi' := h i355      rw [row_setAt_eq _ _ _ hi, dotL_radd _ _ _ (by rw [length_rsmul]; exact hl), dotL_rsmul] at hi'356      rw [row_setAt_ne _ _ _ _ hik] at hk357      rw [hk, mul_zero, add_zero] at hi'; exact hi'358    | .isFalse e => have := h j; rw [row_setAt_ne _ _ _ _ e] at this; exact this359  · intro h j360    match Nat.decEq i j with361    | .isTrue e =>362      subst e363      rw [row_setAt_eq _ _ _ hi, dotL_radd _ _ _ (by rw [length_rsmul]; exact hl), dotL_rsmul, h i, h k, mul_zero, add_zero]364    | .isFalse e => rw [row_setAt_ne _ _ _ _ e]; exact h j365366theorem inKer_clearUpto_iff (ainv : Ext p ν) : ∀ (k : Nat) (M : Mat p ν), Square M → k < M.length → ∀ v,367    (InKer (clearUpto ainv k M) v ↔ InKer M v)368  | 0, _, _, _, _ => Iff.rfl369  | k + 1, M, hS, hk, v =>370    have hS' := square_clearUpto ainv k M hS (Nat.lt_of_succ_lt hk)371    have hk' : k + 1 < (clearUpto ainv k M).length := by rw [length_clearUpto]; exact hk372    have h0' : 0 < (clearUpto ainv k M).length := Nat.lt_of_le_of_lt (Nat.zero_le _) hk'373    by374      show InKer (clearRow (clearUpto ainv k M) ainv (k + 1)) v ↔ InKer M v375      unfold clearRow376      exact (inKer_setAt_iff _ (k + 1) 0 (Nat.succ_ne_zero k) _ v hk' ((hS' _ hk').trans (hS' 0 h0').symm)).trans377        (inKer_clearUpto_iff ainv k M hS (Nat.lt_of_succ_lt hk) v)378379theorem inKer_pivotFix_iff (M : Mat p ν) (hS : Square M) : ∀ (k : Nat), k < M.length → ∀ v, (InKer (pivotFix M k) v ↔ InKer M v)380  | 0, _, _ => Iff.rfl381  | k + 1, hk, v =>382    inKer_setAt_iff M 0 (k + 1) (Nat.succ_ne_zero k).symm 1 v (Nat.lt_of_le_of_lt (Nat.zero_le _) hk)383      ((hS 0 (Nat.lt_of_le_of_lt (Nat.zero_le _) hk)).trans (hS (k + 1) hk).symm)384385theorem row_beyond (M : Mat p ν) : ∀ (j : Nat), M.length ≤ j → row M j = []386  | _, _ => by387    unfold row388    exact aux M _ ‹_›389where390  aux : ∀ (l : Mat p ν) (j : Nat), l.length ≤ j → nth [] l j = []391    | [], _, _ => rfl392    | _ :: _, 0, h => absurd h (Nat.not_succ_le_zero _)393    | _ :: l, j + 1, h => aux l j (Nat.le_of_succ_le_succ h)394395theorem dotL_zero_right : ∀ (r w : List (Ext p ν)), IsZero w → dotL r w = 0396  | [], _, _ => rfl397  | _ :: _, [], _ => rfl398  | a :: r, x :: w, h => by399    show a * x + dotL r w = 0400    rw [show x = 0 from h 0, mul_zero, dotL_zero_right r w fun i => h (i + 1), add_zero]401402/-- The kernel of a matrix whose first column is `(a, 0, …, 0)`: the first row's equation and the kernel of the minor. -/403theorem inKer_cons_iff (C : Mat p ν) (hS : Square C) (hC : 0 < C.length)404    (hz : ∀ i, 0 < i → i < C.length → head (row C i) = 0) (x : Ext p ν) (w : List (Ext p ν)) :405    InKer C (x :: w) ↔ (head (row C 0) * x + dotL (row C 0).tail w = 0 ∧ InKer (minor C 0) w) := by406  have hr0 : 0 < (row C 0).length := by rw [hS 0 hC]; exact hC407  constructor408  · intro h409    refine ⟨by rw [← dotL_cons_head _ _ _ hr0]; exact h 0, fun j => ?_⟩410    match Nat.decLt (j + 1) C.length with411    | .isTrue hj =>412      have hj' := h (j + 1)413      rw [dotL_cons_head _ _ _ (by rw [hS (j + 1) hj]; exact hC), hz (j + 1) (Nat.succ_pos j) hj, zero_mul, zero_add] at hj'414      rw [row_minor_ge C 0 j (Nat.zero_le j)]; exact hj'415    | .isFalse hj =>416      rw [row_beyond (minor C 0) j (by417        have := length_minor C 0 hC418        exact Nat.le_of_succ_le_succ (show (minor C 0).length + 1 ≤ j + 1 by rw [this]; exact Nat.le_of_not_lt hj))]419      rfl420  · intro ⟨h0, hm⟩ j421    match j with422    | 0 => rw [dotL_cons_head _ _ _ hr0]; exact h0423    | j + 1 =>424      match Nat.decLt (j + 1) C.length with425      | .isTrue hj =>426        rw [dotL_cons_head _ _ _ (by rw [hS (j + 1) hj]; exact hC), hz (j + 1) (Nat.succ_pos j) hj, zero_mul, zero_add,427          ← row_minor_ge C 0 j (Nat.zero_le j)]428        exact hm j429      | .isFalse hj => rw [row_beyond C (j + 1) (Nat.le_of_not_lt hj)]; rfl430431/-- Whether every entry vanishes, decided. -/432def allZero : List (Ext p ν) → Bool433  | [] => true434  | x :: w => decide (x = 0) && allZero w435436theorem isZero_of_allZero : ∀ w : List (Ext p ν), allZero w = true → IsZero w437  | [], _, _ => rfl438  | x :: w, h, i => by439    have hx : decide (x = 0) = true := FRC.Shell.Frame.and_true_left h440    have hw := isZero_of_allZero w (FRC.Shell.Frame.and_true_right h)441    match i with442    | 0 => exact of_decide_eq_true hx443    | i + 1 => exact hw i444445theorem not_isZero_of_allZero_false : ∀ w : List (Ext p ν), allZero w = false → ¬ IsZero w446  | [], h, _ => nomatch h447  | x :: w, h, hz => by448    match hd : decide (x = 0) with449    | true =>450      have hw : allZero w = false := by451        unfold allZero at h; rw [hd] at h; exact h452      exact not_isZero_of_allZero_false w hw fun i => hz (i + 1)453    | false => exact of_decide_eq_false hd (hz 0)454455theorem mul_left_cancel_zero {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) {a y : Ext p ν} (ha : a ≠ 0)456    (h : a * y = 0) : y = 0 := by457  rw [← Ext.one_mul y, ← mul_inv F hν ha, Ext.mul_comm a, Ext.mul_assoc, h, mul_zero]458459theorem ext_one_ne_zero {κ : Nat} {g : Shell p} (F : Frame p κ g) : (1 : Ext p ν) ≠ 0 := fun h => F.one_ne_zero (Ext.re_congr h)460461/-- A nontrivial kernel vector forces the determinant to vanish. -/462theorem det_eq_zero_of_inKer {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) :463    ∀ (n : Nat) (M : Mat p ν), Square M → M.length = n → ∀ v : List (Ext p ν), v.length = n → InKer M v → ¬ IsZero v → det M = 0464  | 0, _, _, _, [], _, _, hnz => absurd (fun _ => rfl) hnz465  | 0, _, _, _, _ :: _, hv, _, _ => absurd hv (Nat.succ_ne_zero _)466  | n + 1, M, hS, hM, v, hv, hker, hnz => by467    have hpos : 0 < M.length := hM ▸ Nat.succ_pos n468    match hpiv : pivotAux M (n + 1) 0 with469    | none => exact det_zero_col M hpos fun i hi => pivotAux_none M (n + 1) 0 hpiv i (Nat.zero_le i) (by rw [Nat.zero_add, ← hM]; exact hi)470    | some k =>471      obtain ⟨_, hk, hk0, hleast⟩ := pivotAux_some M (n + 1) 0 k hpiv472      have hkM : k < M.length := by rw [hM]; exact Nat.lt_of_lt_of_eq hk (Nat.zero_add _)473      have hS' : Square (pivotFix M k) := square_pivotFix M hS k hkM474      have hlen' : (pivotFix M k).length = n + 1 := (length_pivotFix M k).trans hM475      have ha : head (row (pivotFix M k) 0) ≠ 0 := by476        rw [head_pivotFix M hS k hkM fun j hj => hleast j (Nat.zero_le j) hj]; exact hk0477      have hinv := mul_inv F hν ha478      have hn : n < (pivotFix M k).length := by rw [hlen']; exact Nat.lt_succ_self n479      let C := clearUpto (inv (head (row (pivotFix M k) 0))) n (pivotFix M k)480      have hC : Square C := square_clearUpto _ n _ hS' hn481      have hCl : C.length = n + 1 := (length_clearUpto _ _ _).trans hlen'482      have hCpos : 0 < C.length := hCl ▸ Nat.succ_pos n483      have hz : ∀ i, 0 < i → i < C.length → head (row C i) = 0 := fun i hi hi' =>484        head_clearUpto _ _ hS' hinv n hn i hi (Nat.le_of_lt_succ (Nat.lt_of_lt_of_eq hi' hCl))485      have hkerC : InKer C v := (inKer_clearUpto_iff _ n _ hS' hn v).mpr ((inKer_pivotFix_iff M hS k hkM v).mpr hker)486      have hdet : det M = head (row C 0) * det (minor C 0) := by487        rw [← det_pivotFix M hS k hkM, ← det_clearUpto (inv (head (row (pivotFix M k) 0))) n _ hS' hn]488        exact det_first_col C hCpos hz489      have hhead : head (row C 0) = head (row (pivotFix M k) 0) := by rw [row_clearUpto_zero]490      match v, hv with491      | x :: w, hv =>492        obtain ⟨h0, hm⟩ := (inKer_cons_iff C hC hCpos hz x w).mp hkerC493        match hw : allZero w with494        | false =>495          rw [hdet, det_eq_zero_of_inKer F hν n (minor C 0) (square_minor C hC 0 hCpos)496            (Nat.succ.inj (show (minor C 0).length + 1 = n + 1 by rw [length_minor C 0 hCpos]; exact hCl))497            w (Nat.succ.inj hv) hm (not_isZero_of_allZero_false w hw), mul_zero]498        | true =>499          have hw' := isZero_of_allZero w hw500          rw [dotL_zero_right _ _ hw', add_zero, hhead] at h0501          have hx : x = 0 := mul_left_cancel_zero F hν ha h0502          exact absurd (fun i => match i with | 0 => hx | i + 1 => hw' i) hnz503504/-- A vanishing determinant yields a nontrivial kernel vector. -/505theorem exists_inKer_of_det_eq_zero {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) :506    ∀ (n : Nat) (M : Mat p ν), Square M → M.length = n → det M = 0 → ∃ v : List (Ext p ν), v.length = n ∧ ¬ IsZero v ∧ InKer M v507  | 0, [], _, _, h => absurd h (ext_one_ne_zero F)508  | 0, _ :: _, _, hM, _ => absurd hM (Nat.succ_ne_zero _)509  | n + 1, M, hS, hM, hdet0 => by510    have hpos : 0 < M.length := hM ▸ Nat.succ_pos n511    match hpiv : pivotAux M (n + 1) 0 with512    | none =>513      have hz : ∀ i, i < M.length → head (row M i) = 0 := fun i hi =>514        pivotAux_none M (n + 1) 0 hpiv i (Nat.zero_le i) (by rw [Nat.zero_add, ← hM]; exact hi)515      refine ⟨1 :: List.replicate n 0, congrArg (· + 1) (length_replicate n), fun h => ext_one_ne_zero F (h 0), fun j => ?_⟩516      match Nat.decLt j M.length with517      | .isTrue hj =>518        rw [dotL_cons_head _ _ _ (by rw [hS j hj]; exact hpos), hz j hj, zero_mul, zero_add]519        exact dotL_zero_right _ _ (isZero_replicate n)520      | .isFalse hj => rw [row_beyond M j (Nat.le_of_not_lt hj)]; rfl521    | some k =>522      obtain ⟨_, hk, hk0, hleast⟩ := pivotAux_some M (n + 1) 0 k hpiv523      have hkM : k < M.length := by rw [hM]; exact Nat.lt_of_lt_of_eq hk (Nat.zero_add _)524      have hS' : Square (pivotFix M k) := square_pivotFix M hS k hkM525      have hlen' : (pivotFix M k).length = n + 1 := (length_pivotFix M k).trans hM526      have ha : head (row (pivotFix M k) 0) ≠ 0 := by527        rw [head_pivotFix M hS k hkM fun j hj => hleast j (Nat.zero_le j) hj]; exact hk0528      have hinv := mul_inv F hν ha529      have hn : n < (pivotFix M k).length := by rw [hlen']; exact Nat.lt_succ_self n530      let C := clearUpto (inv (head (row (pivotFix M k) 0))) n (pivotFix M k)531      have hC : Square C := square_clearUpto _ n _ hS' hn532      have hCl : C.length = n + 1 := (length_clearUpto _ _ _).trans hlen'533      have hCpos : 0 < C.length := hCl ▸ Nat.succ_pos n534      have hz : ∀ i, 0 < i → i < C.length → head (row C i) = 0 := fun i hi hi' =>535        head_clearUpto _ _ hS' hinv n hn i hi (Nat.le_of_lt_succ (Nat.lt_of_lt_of_eq hi' hCl))536      have hhead : head (row C 0) = head (row (pivotFix M k) 0) := by rw [row_clearUpto_zero]537      have hdet : det M = head (row C 0) * det (minor C 0) := by538        rw [← det_pivotFix M hS k hkM, ← det_clearUpto (inv (head (row (pivotFix M k) 0))) n _ hS' hn]539        exact det_first_col C hCpos hz540      have hminor : det (minor C 0) = 0 := by541        rw [hdet, hhead] at hdet0; exact mul_left_cancel_zero F hν ha hdet0542      obtain ⟨w, hwl, hwnz, hwk⟩ := exists_inKer_of_det_eq_zero F hν n (minor C 0) (square_minor C hC 0 hCpos)543        (Nat.succ.inj (show (minor C 0).length + 1 = n + 1 by rw [length_minor C 0 hCpos]; exact hCl)) hminor544      let x : Ext p ν := -(inv (head (row (pivotFix M k) 0)) * dotL (row C 0).tail w)545      refine ⟨x :: w, congrArg (· + 1) hwl, fun h => hwnz fun i => h (i + 1), ?_⟩546      refine (inKer_pivotFix_iff M hS k hkM _).mp ((inKer_clearUpto_iff (inv (head (row (pivotFix M k) 0))) n _ hS' hn _).mp ?_)547      refine (inKer_cons_iff C hC hCpos hz x w).mpr ⟨?_, hwk⟩548      show head (row C 0) * -(inv (head (row (pivotFix M k) 0)) * dotL (row C 0).tail w) + dotL (row C 0).tail w = 0549      rw [hhead, ← Hermitian.mul_neg, ← Ext.mul_assoc, hinv, Ext.one_mul, neg_add]550where551  isZero_replicate : ∀ n : Nat, IsZero (List.replicate n (0 : Ext p ν))552    | 0, _ => rfl553    | n + 1, 0 => rfl554    | n + 1, i + 1 => isZero_replicate n i555  length_replicate : ∀ n : Nat, (List.replicate n (0 : Ext p ν)).length = n556    | 0 => rfl557    | n + 1 => congrArg (· + 1) (length_replicate n)558559/-- The determinant vanishes exactly on the singular matrices. -/560theorem det_eq_zero_iff {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) (M : Mat p ν) (hS : Square M) :561    det M = 0 ↔ ∃ v : List (Ext p ν), v.length = M.length ∧ ¬ IsZero v ∧ InKer M v :=562  ⟨exists_inKer_of_det_eq_zero F hν M.length M hS rfl,563   fun ⟨v, hv, hnz, hker⟩ => det_eq_zero_of_inKer F hν M.length M hS rfl v hv hker hnz⟩564565/-! ## Decided -/566567/-- `I − kwH` for the Hermitian `H = [[0, w], [−w, 0]]`. -/568def skewCayley (ν : Shell p) (k : Shell p) : Mat p ν :=569  let α : Ext p ν := ⟨0, k⟩570  let w : Ext p ν := ⟨0, 1⟩571  [[1, -(α * w)], [α * w, 1]]572573/-- [value] — on `𝔽₁₃` (`ν = 2`): the elimination and the expansion agree on `det(I − kwH) = 1 + k²ν²` for every `k`, and574the kernel criterion reads off the two singular parameters `k = 4, 9`. -/575theorem skew_det_values :576    (∀ k : Shell 13, detG 2 (skewCayley 2 k) = 1 + Ext.ofShell (k * 2 * (k * 2))) ∧577    (∀ k : Shell 13, det (skewCayley 2 k) = 1 + Ext.ofShell (k * 2 * (k * 2))) ∧578    (∀ k : Shell 13, detG 2 (skewCayley 2 k) = 0 ↔ (k = 4 ∨ k = 9)) := by579  decide +kernel580581end FRC.Dirac.Det582