Theme/Cayley.lean — FrcCore

1import FrcCore.Theme.Elim2/-!3# FrcCore.Theme.Cayley — the Cayley denominator `I − αH` (the operator theme)45The kernel criterion of `Theme/Elim` applied to the denominator of the Cayley transform, `I − αH` on the list6matrices of `Theme/Dirac` (`Mat.ident`, `Mat.add`, `Mat.neg`, `Mat.smul`): `det (I − αH) = 0` exactly when `α·Hv = v`7for some `v ≠ 0`, and for `α ≠ 0` exactly when `α⁻¹` is an eigenvalue of `H` (8:T1's step from the determinant to the8eigenvalues, for every matrix over `K`); `det I = 1`, so `α = 0` is always admissible. The rows of `Mat.ident` are9reached through `rangeS`, the structural form of `List.range`, whose core lemmas carry `propext`. On `𝔽₁₃` the10decided instance exhibits the two singular parameters of the skew Hamiltonian with their eigenvectors. No axioms.11-/1213namespace FRC.Dirac.Det1415open FRC FRC.Extension FRC.Dirac FRC.Dirac.Hermitian16open FRC.Dirac.Mat (nth)17open FRC.Shell (Frame)18open FRC.Shell.Frame (IsSquare)1920variable {p : Nat} [Pos p] {ν : Shell p}2122/-! ## The identity, the unit rows and the rows of `I − αH` -/232425/-- `Mv`: the matrix applied to a vector, one dot product per row. -/26def mulVec (M : Mat p ν) (v : List (Ext p ν)) : List (Ext p ν) := M.map (fun r => dotL r v)2728/-- `I − αH`, the denominator of the Cayley transform (8-dirac, Def. C14: `α` is admissible when it is invertible). -/29def cayleyDen (α : Ext p ν) (H : Mat p ν) : Mat p ν := Mat.add (Mat.ident H.length) (Mat.neg (Mat.smul α H))3031/-- `[0, 1, …, n−1]` by appending (the structural form of `List.range`). -/32def rangeS : Nat → List Nat33  | 0 => []34  | n + 1 => rangeS n ++ [n]3536/-- The `i`-th unit row of length `n`. -/37def unitRow (n i : Nat) : List (Ext p ν) := (rangeS n).map (fun j => if i = j then 1 else 0)3839theorem range_loop_eq : ∀ (n : Nat) (acc : List Nat), List.range.loop n acc = List.range.loop n [] ++ acc40  | 0, _ => rfl41  | n + 1, acc => by42    show List.range.loop n (n :: acc) = List.range.loop n [n] ++ acc43    rw [range_loop_eq n (n :: acc), range_loop_eq n [n], append_assoc']; rfl4445theorem range_eq_rangeS : ∀ n : Nat, List.range n = rangeS n46  | 0 => rfl47  | n + 1 => by48    show List.range.loop n [n] = rangeS n ++ [n]49    rw [range_loop_eq n [n]]; exact congrArg (· ++ [n]) (range_eq_rangeS n)5051theorem length_rangeS : ∀ n : Nat, (rangeS n).length = n52  | 0 => rfl53  | n + 1 => by show (rangeS n ++ [n]).length = n + 1; rw [length_append', length_rangeS n]; rfl5455theorem length_unitRow (n i : Nat) : (unitRow (ν := ν) n i).length = n := by56  show ((rangeS n).map _).length = n; rw [length_map, length_rangeS]5758theorem nth_rangeS : ∀ (n i : Nat), i < n → nth 0 (rangeS n) i = i59  | 0, _, h => absurd h (Nat.not_lt_zero _)60  | n + 1, i, h => by61    show nth 0 (rangeS n ++ [n]) i = i62    match Nat.lt_or_ge i n with63    | Or.inl hi => rw [nth_append_lt 0 _ _ i (by rw [length_rangeS]; exact hi)]; exact nth_rangeS n i hi64    | Or.inr hi =>65      have e : i = n := Nat.le_antisymm (Nat.le_of_lt_succ h) hi66      have := nth_append_len 0 (rangeS n) n67      rw [length_rangeS] at this68      rw [e]; exact this6970/-- `dotL (r ++ [c]) v = dotL r v + c · v_{|r|}` when `v` reaches that far. -/71theorem dotL_append_single : ∀ (r : List (Ext p ν)) (c : Ext p ν) (v : List (Ext p ν)), r.length < v.length →72    dotL (r ++ [c]) v = dotL r v + c * nth 0 v r.length73  | [], c, x :: _, _ => by show c * x + 0 = 0 + c * x; rw [add_zero, zero_add]74  | [], _, [], h => absurd h (Nat.lt_irrefl 0)75  | _ :: _, _, [], h => absurd h (Nat.not_lt_zero _)76  | a :: r, c, x :: v, h => by77    show a * x + dotL (r ++ [c]) v = a * x + dotL r v + c * nth 0 v r.length78    rw [dotL_append_single r c v (Nat.lt_of_succ_lt_succ h), add_assoc]7980theorem dotL_unitRow_ge : ∀ (n i : Nat) (v : List (Ext p ν)), n ≤ i → n ≤ v.length → dotL (unitRow n i) v = 081  | 0, _, _, _, _ => rfl82  | n + 1, i, v, hi, hv => by83    show dotL ((rangeS n ++ [n]).map _) v = 084    rw [map_append_single]85    have hl : ((rangeS n).map fun j => if i = j then (1 : Ext p ν) else 0).length < v.length := by86      rw [length_map, length_rangeS]; exact hv87    rw [dotL_append_single _ _ v hl]88    show dotL (unitRow n i) v + (if i = n then 1 else 0) * _ = 089    rw [dotL_unitRow_ge n i v (Nat.le_of_succ_le hi) (Nat.le_of_succ_le hv), ite_eq_right (Nat.ne_of_gt hi), zero_mul, add_zero]9091/-- The unit row reads off the `i`-th entry. -/92theorem dotL_unitRow : ∀ (n i : Nat) (v : List (Ext p ν)), i < n → n ≤ v.length → dotL (unitRow n i) v = nth 0 v i93  | 0, _, _, h, _ => absurd h (Nat.not_lt_zero _)94  | n + 1, i, v, hi, hv => by95    show dotL ((rangeS n ++ [n]).map _) v = nth 0 v i96    rw [map_append_single]97    have hl : ((rangeS n).map fun j => if i = j then (1 : Ext p ν) else 0).length < v.length := by98      rw [length_map, length_rangeS]; exact hv99    rw [dotL_append_single _ _ v hl]100    show dotL (unitRow n i) v + (if i = n then 1 else 0) * nth 0 v ((rangeS n).map _).length = nth 0 v i101    rw [length_map, length_rangeS]102    match Nat.lt_or_ge i n with103    | Or.inl h => rw [dotL_unitRow n i v h (Nat.le_of_succ_le hv), ite_eq_right (Nat.ne_of_lt h), zero_mul, add_zero]104    | Or.inr h =>105      have e : i = n := Nat.le_antisymm (Nat.le_of_lt_succ hi) h106      rw [dotL_unitRow_ge n i v h (Nat.le_of_succ_le hv), ite_eq_left e, Ext.one_mul, zero_add, e]107108theorem length_ident (n : Nat) : (Mat.ident (p := p) (ν := ν) n).length = n := by109  show ((List.range n).map _).length = n; rw [length_map, range_eq_rangeS, length_rangeS]110111theorem row_ident (n i : Nat) (h : i < n) : row (Mat.ident (p := p) (ν := ν) n) i = unitRow n i := by112  show nth [] ((List.range n).map fun i => (List.range n).map fun j => if i = j then (1 : Ext p ν) else 0) i = unitRow n i113  rw [nth_map_lt (fun i => (List.range n).map fun j => if i = j then (1 : Ext p ν) else 0) 0 [] _ i114        (by rw [range_eq_rangeS, length_rangeS]; exact h), range_eq_rangeS, nth_rangeS n i h]115  rfl116117theorem zipWith_add_eq_radd : ∀ (r s : List (Ext p ν)), List.zipWith (· + ·) r s = radd r s118  | [], _ => rfl119  | _ :: _, [] => rfl120  | _ :: r, _ :: s => congrArg (_ :: ·) (zipWith_add_eq_radd r s)121122theorem map_neg_smul (α : Ext p ν) : ∀ r : List (Ext p ν), (r.map (α * ·)).map (- ·) = rsmul (-α) r123  | [] => rfl124  | a :: r => by show -(α * a) :: _ = (-α * a) :: _; rw [neg_mul, map_neg_smul α r]; rfl125126theorem length_cayleyDen (α : Ext p ν) (H : Mat p ν) : (cayleyDen α H).length = H.length := by127  show (List.zipWith _ (Mat.ident H.length) (Mat.neg (Mat.smul α H))).length = H.length128  rw [length_zipWith', length_ident]129  show (Mat.ident H.length).length = ((H.map _).map _).length130  rw [length_ident, length_map, length_map]131132theorem row_cayleyDen (α : Ext p ν) (H : Mat p ν) (j : Nat) (hj : j < H.length) :133    row (cayleyDen α H) j = radd (unitRow H.length j) (rsmul (-α) (row H j)) := by134  show nth [] (List.zipWith (fun r s => List.zipWith (· + ·) r s) (Mat.ident H.length) (Mat.neg (Mat.smul α H))) j = _135  have h2 : j < (Mat.neg (Mat.smul α H)).length := by136    show j < ((H.map _).map _).length; rw [length_map, length_map]; exact hj137  rw [nth_zipWith (fun r s => List.zipWith (· + ·) r s) [] [] [] _ _ j (by rw [length_ident]; exact hj) h2]138  show List.zipWith (· + ·) (row (Mat.ident H.length) j) (nth [] ((H.map (fun r => r.map (α * ·))).map (fun r => r.map (- ·))) j) = _139  have h1 : j < (H.map (fun r => r.map (α * ·))).length := by rw [length_map]; exact hj140  rw [zipWith_add_eq_radd, row_ident _ _ hj, nth_map_lt (fun r : List (Ext p ν) => r.map (- ·)) [] [] _ j h1,141    nth_map_lt (fun r : List (Ext p ν) => r.map (α * ·)) [] [] _ j hj, map_neg_smul]142  rfl143144theorem square_cayleyDen (α : Ext p ν) (H : Mat p ν) (hS : Square H) : Square (cayleyDen α H) := fun j hj => by145  rw [length_cayleyDen] at hj ⊢146  rw [row_cayleyDen α H j hj, length_radd, length_unitRow]147  rw [length_unitRow, length_rsmul]; exact (hS j hj).symm148149theorem length_mulVec (H : Mat p ν) (v : List (Ext p ν)) : (mulVec H v).length = H.length := length_map _ H150151theorem nth_mulVec (H : Mat p ν) (v : List (Ext p ν)) (j : Nat) : nth 0 (mulVec H v) j = dotL (row H j) v := by152  show nth 0 (H.map fun r => dotL r v) j = dotL (nth [] H j) v153  exact nth_map (fun r => dotL r v) [] H j154155theorem nth_rsmul (c : Ext p ν) (v : List (Ext p ν)) (j : Nat) : nth 0 (rsmul c v) j = c * nth 0 v j := by156  show nth 0 (v.map (c * ·)) j = c * nth 0 v j157  rw [← mul_zero c]; exact nth_map (c * ·) 0 v j158159/-! ## The eigenvalue criterion -/160161/-- `v` lies in the kernel of `I − αH` exactly when `α · Hv = v`. -/162theorem inKer_cayleyDen_iff (α : Ext p ν) (H : Mat p ν) (hS : Square H) (v : List (Ext p ν)) (hv : v.length = H.length) :163    InKer (cayleyDen α H) v ↔ rsmul α (mulVec H v) = v := by164  have key : ∀ j, j < H.length → (dotL (row (cayleyDen α H) j) v = 0 ↔ α * dotL (row H j) v = nth 0 v j) := fun j hj => by165    rw [row_cayleyDen α H j hj, dotL_radd _ _ _ (by rw [length_unitRow, length_rsmul]; exact (hS j hj).symm),166      dotL_rsmul, dotL_unitRow _ _ _ hj (Nat.le_of_eq hv.symm), ← neg_mul]167    exact ⟨fun h => by168             have this : nth 0 v j + -(α * dotL (row H j) v) + α * dotL (row H j) v = 0 + α * dotL (row H j) v :=169               congrArg (· + α * dotL (row H j) v) h170             rw [add_assoc, neg_add, add_zero, zero_add] at this; exact this.symm,171           fun h => by rw [← h, add_neg]⟩172  constructor173  · intro hk174    refine ext_nth 0 _ _ (by rw [length_rsmul, length_mulVec, hv]) fun j hj => ?_175    rw [length_rsmul, length_mulVec] at hj176    rw [nth_rsmul, nth_mulVec H v j]; exact (key j hj).1 (hk j)177  · intro h j178    match Nat.lt_or_ge j H.length with179    | Or.inl hj =>180      refine (key j hj).2 ?_181      have this : nth 0 (rsmul α (mulVec H v)) j = nth 0 v j := congrArg (fun l => nth 0 l j) h182      rw [nth_rsmul, nth_mulVec H v j] at this; exact this183    | Or.inr hj => rw [row_beyond _ j (by rw [length_cayleyDen]; exact hj)]; rfl184185/-- The Cayley denominator is singular exactly when `1` is an eigenvalue of `αH`: `det(I − αH) = 0 ↔ ∃ v ≠ 0, α·Hv = v`. -/186theorem cayleyDen_singular_iff {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) (α : Ext p ν) (H : Mat p ν) (hS : Square H) :187    det (cayleyDen α H) = 0 ↔ ∃ v : List (Ext p ν), v.length = H.length ∧ ¬ IsZero v ∧ rsmul α (mulVec H v) = v := by188  refine Iff.trans (det_eq_zero_iff F hν _ (square_cayleyDen α H hS)) ?_189  rw [length_cayleyDen]190  exact ⟨fun ⟨v, hv, hz, hk⟩ => ⟨v, hv, hz, (inKer_cayleyDen_iff α H hS v hv).1 hk⟩,191         fun ⟨v, hv, hz, he⟩ => ⟨v, hv, hz, (inKer_cayleyDen_iff α H hS v hv).2 he⟩⟩192193/-- 8:C17 — for `α ≠ 0` the excluded parameters are the inverses of the eigenvalues: `det(I − αH) = 0 ↔ ∃ v ≠ 0, Hv = α⁻¹v`,194for every square matrix over `K` (item (ii) of the classification). -/195theorem cayleyDen_singular_iff_eigen {κ : Nat} {g : Shell p} (F : Frame p κ g) (hν : ¬IsSquare ν) {α : Ext p ν} (hα : α ≠ 0)196    (H : Mat p ν) (hS : Square H) :197    det (cayleyDen α H) = 0 ↔ ∃ v : List (Ext p ν), v.length = H.length ∧ ¬ IsZero v ∧ mulVec H v = rsmul (inv α) v := by198  refine Iff.trans (cayleyDen_singular_iff F hν α H hS) ?_199  have hinv : inv α * α = 1 := by rw [Ext.mul_comm]; exact mul_inv F hν hα200  have rs : ∀ (c d : Ext p ν) (w : List (Ext p ν)), rsmul c (rsmul d w) = rsmul (c * d) w := fun c d w => by201    show (w.map (d * ·)).map (c * ·) = w.map ((c * d) * ·)202    exact map_map_mul c d w203  have one : ∀ w : List (Ext p ν), rsmul 1 w = w := fun w => by204    show w.map (1 * ·) = w; exact map_one_mul w205  exact ⟨fun ⟨v, hv, hz, he⟩ => ⟨v, hv, hz, by206            have := congrArg (rsmul (inv α)) he207            rw [rs, hinv, one] at this; exact this⟩,208         fun ⟨v, hv, hz, he⟩ => ⟨v, hv, hz, by rw [he, rs, mul_inv F hν hα, one]⟩⟩209where210  map_map_mul (c d : Ext p ν) : ∀ w : List (Ext p ν), (w.map (d * ·)).map (c * ·) = w.map ((c * d) * ·)211    | [] => rfl212    | x :: w => by show c * (d * x) :: _ = c * d * x :: _; rw [Ext.mul_assoc, map_map_mul c d w]213  map_one_mul : ∀ w : List (Ext p ν), w.map ((1 : Ext p ν) * ·) = w214    | [] => rfl215    | x :: w => by show 1 * x :: _ = x :: _; rw [Ext.one_mul, map_one_mul w]216217/-! ## `det I = 1` -/218219theorem rangeS_succ_eq_map : ∀ n : Nat, rangeS (n + 1) = 0 :: (rangeS n).map Nat.succ220  | 0 => rfl221  | n + 1 => by222    show rangeS (n + 1) ++ [n + 1] = 0 :: (rangeS n ++ [n]).map Nat.succ223    rw [rangeS_succ_eq_map n, map_append_single]; rfl224225theorem ite_succ (i j : Nat) : (if i + 1 = j + 1 then (1 : Ext p ν) else 0) = if i = j then 1 else 0 :=226  match Nat.decEq i j with227  | isTrue h => by rw [h, ite_eq_left rfl, ite_eq_left rfl]228  | isFalse h => by rw [ite_eq_right h, ite_eq_right (fun e => h (Nat.succ.inj e))]229230/-- The first minor of the identity is the identity one size down. -/231theorem minor_ident_zero (n : Nat) : minor (Mat.ident (p := p) (ν := ν) (n + 1)) 0 = Mat.ident n := by232  show ((removeAt ((List.range (n + 1)).map fun i => (List.range (n + 1)).map fun j => if i = j then (1 : Ext p ν) else 0) 0).map List.tail) = _233  rw [range_eq_rangeS, rangeS_succ_eq_map]234  show ((((rangeS n).map Nat.succ).map fun i => (0 :: (rangeS n).map Nat.succ).map fun j => if i = j then (1 : Ext p ν) else 0).map List.tail) = _235  rw [map_map', map_map']236  show ((rangeS n).map fun i => ((rangeS n).map Nat.succ).map fun j => if i + 1 = j then (1 : Ext p ν) else 0) = (List.range n).map _237  rw [range_eq_rangeS]238  exact map_congr' (fun i => by rw [map_map']; exact map_congr' (fun j => ite_succ i j) _) _239240theorem head_unitRow_succ (n i : Nat) : head (unitRow (ν := ν) (n + 1) i) = if i = 0 then 1 else 0 := by241  show head ((rangeS (n + 1)).map _) = _242  rw [rangeS_succ_eq_map]; rfl243244/-- `det I = 1`. -/245theorem det_ident : ∀ n : Nat, det (Mat.ident (p := p) (ν := ν) n) = 1246  | 0 => det_nil247  | n + 1 => by248    have hl : 0 < (Mat.ident (p := p) (ν := ν) (n + 1)).length := by rw [length_ident]; exact Nat.succ_pos n249    rw [det_first_col _ hl (fun i hi hi' => by250          rw [length_ident] at hi'251          rw [row_ident _ _ hi', head_unitRow_succ, ite_eq_right (Nat.ne_of_gt hi)]),252      row_ident _ _ (Nat.succ_pos n), head_unitRow_succ, ite_eq_left rfl, Ext.one_mul, minor_ident_zero, det_ident n]253254/-- 8:C17 — `α = 0` is always admissible: `det(I − 0·H) = 1` (the admissible set contains zero). -/255theorem det_cayleyDen_zero (H : Mat p ν) (hS : Square H) : det (cayleyDen 0 H) = 1 := by256  have e : cayleyDen 0 H = Mat.ident H.length := by257    refine ext_nth [] _ _ (by rw [length_cayleyDen, length_ident]) fun j hj => ?_258    rw [length_cayleyDen] at hj259    show row (cayleyDen 0 H) j = row (Mat.ident H.length) j260    rw [row_cayleyDen 0 H j hj, row_ident _ _ hj]261    have hz : rsmul (-0 : Ext p ν) (row H j) = List.replicate (row H j).length 0 := by262      rw [neg_zero']; exact rsmul_zero _263    rw [hz, hS j hj]; exact radd_replicate_zero _ _ (length_unitRow _ _)264  rw [e, det_ident]265where266  neg_zero' : (-0 : Ext p ν) = 0 := Ext.ext Shell.neg_zero Shell.neg_zero267  rsmul_zero : ∀ r : List (Ext p ν), rsmul 0 r = List.replicate r.length 0268    | [] => rfl269    | x :: r => by show (0 * x) :: rsmul 0 r = 0 :: List.replicate r.length 0; rw [zero_mul, rsmul_zero r]270  radd_replicate_zero : ∀ (r : List (Ext p ν)) (n : Nat), r.length = n → radd r (List.replicate n 0) = r271    | [], 0, _ => rfl272    | [], _ + 1, h => absurd h (Nat.ne_of_lt (Nat.succ_pos _))273    | _ :: _, 0, h => absurd h (Nat.ne_of_gt (Nat.succ_pos _))274    | x :: r, n + 1, h => by show (x + 0) :: radd r (List.replicate n 0) = x :: r; rw [add_zero, radd_replicate_zero r n (Nat.succ.inj h)]275276/-! ## Decided -/277278/-- The skew Hamiltonian `H = [[0, w], [−w, 0]]`. -/279def skewH (ν : Shell p) : Mat p ν := [[0, ⟨0, 1⟩], [-⟨0, 1⟩, 0]]280281/-- 8:C17 [value] — on `𝔽₁₃` (`ν = 2`): `I − kwH` is `skewCayley`; the Cayley denominator is singular exactly at `k = 4, 9`,282and at `k = 4` the vector `(8, 1)` is fixed by `αH`, at `k = 9` the vector `(5, 1)`. -/283theorem skew_cayleyDen_values :284    (∀ k : Shell 13, cayleyDen (⟨0, k⟩ : Ext 13 2) (skewH 2) = skewCayley 2 k) ∧285    (∀ k : Shell 13, detG 2 (cayleyDen (⟨0, k⟩ : Ext 13 2) (skewH 2)) = 0 ↔ (k = 4 ∨ k = 9)) ∧286    rsmul (⟨0, 4⟩ : Ext 13 2) (mulVec (skewH 2) [8, 1]) = [8, 1] ∧287    rsmul (⟨0, 9⟩ : Ext 13 2) (mulVec (skewH 2) [5, 1]) = [5, 1] := by288  decide +kernel289290291/-- The real symmetric block `[[a, b], [b, −a]]`, a self-adjoint operator on `K²` with `χ = x² − (a² + b²)`. -/292def symH (ν : Shell p) (a b : Shell p) : Mat p ν := [[⟨a, 0⟩, ⟨b, 0⟩], [⟨b, 0⟩, ⟨-a, 0⟩]]293294/-- Whether the block `(a, b)` excludes some trace-zero parameter: `det(I − kwH) = 0` for some `k`. -/295def symExcluded (ν : Shell p) (a b : Nat) : Bool :=296  (List.range p).any fun k =>297    decide (detG 2 (cayleyDen (⟨0, Shell.ofNat k⟩ : Ext p ν) (symH ν (Shell.ofNat a) (Shell.ofNat b))) = 0)298299/-- The paper's kinetic-plus-potential Hamiltonian `−Δ + V_id` on the cycle of `p` sites (8:E8's instance), as a list matrix. -/300def kinV (p : Nat) [Pos p] (ν : Shell p) : Mat p ν :=301  (List.range p).map fun i => (List.range p).map fun j =>302    nth 0 (kineticRow p ν) ((j + p - i) % p) + if i = j then ⟨Shell.ofNat i, 0⟩ else 0303304/-- 8:C17 [value] — on `𝔽₁₃` (`ν = 2`): for every real symmetric block `[[a, b], [b, −a]]` and every `k`, `I − kwH` is305singular exactly when `k²·ν·(a² + b²) = 1`; exactly 72 of the 169 blocks exclude a parameter (those with `a² + b²` a306nonsquare), each of them two. -/307theorem sym_cayleyDen_values13 :308    (∀ a b k : Shell 13, detG 2 (cayleyDen (⟨0, k⟩ : Ext 13 2) (symH 2 a b)) = 0 ↔ k * k * 2 * (a * a + b * b) = 1) ∧309    count2 13 (symExcluded (2 : Shell 13)) = 72 := by310  decide +kernel311312/-- 8:C17 [value] — the skew Hamiltonian on `𝔽₁₇₃` (`ν = 2`): the two excluded parameters are `k = 40, 133`, the roots of313`(kν)² = −1`. -/314theorem skew_cayleyDen_values173 :315    ∀ k : Shell 173, detG 2 (cayleyDen (⟨0, k⟩ : Ext 173 2) (skewH 2)) = 0 ↔ (k = 40 ∨ k = 133) := by316  decide +kernel317318/-- 8:C17 [value] — the skew Hamiltonian on `𝔽₁₅₄₉` (`ν = 2`): the two excluded parameters are `k = 44, 1505`. -/319theorem skew_cayleyDen_values1549 :320    ∀ k : Shell 1549, detG 2 (cayleyDen (⟨0, k⟩ : Ext 1549 2) (skewH 2)) = 0 ↔ (k = 44 ∨ k = 1505) := by321  decide +kernel322323/-- 8:C17 [value] — on `𝔽₁₃`: the paper's `−Δ + V_id` is fully admissible, `det(I − kwH) ≠ 0` for every `k`, read off the324general determinant by elimination. -/325theorem kinV_full13 : ∀ k : Shell 13, detG 13 (cayleyDen (⟨0, k⟩ : Ext 13 2) (kinV 13 2)) ≠ 0 := by326  decide +kernel327328end FRC.Dirac.Det329