SingleOperatorGraph.lean

1 import KomorebiVerification.MathlibImports
2 import KomorebiVerification.PathGraphKrylov
3 import KomorebiVerification.SeedRankBasics
4 
5 /-!
6 # Single-operator and graph seed rank
7 
8 This file isolates the algebraic content of the single-operator results in
9 Paper I.  Generation by `k[T]` is represented literally: each seed may be
10 acted on by an arbitrary polynomial in `T`, and the resulting vectors are
11 added.  The main theorem proves the maximum-geometric-multiplicity formula
12 from explicit primary-decomposition data.  Keeping the decomposition data as
13 hypotheses cleanly separates the elementary generator argument checked here
14 from the classical Jordan/primary-decomposition theorem.
15 
16 The final section gives graph-facing consequences, including the already
17 constructive all-size path certificate and an exact two-seed criterion for
18 cycles from their standard spectral certificate.
19 -/
20 
21 set_option autoImplicit false
22 
23 namespace Komorebi.SingleOperatorGraph
24 
25 open scoped BigOperators
26 open Polynomial
27 
28 universe u v w
29 
30 section PolynomialGeneration
31 
32 variable {k : Type u} [Field k]
33 variable {X : Type v} [AddCommGroup X] [Module k X]
34 
35 /-- Evaluate a polynomial in `T` at a vector `x`. -/
36 noncomputable def evalVector (T : Module.End k X) (x : X) : k[X] →ₗ[k] X :=
37   (LinearMap.applyₗ x).comp (aeval T).toLinearMap
38 
39 @[simp]
40 theorem evalVector_apply (T : Module.End k X) (x : X) (p : k[X]) :
41     evalVector T x p = aeval T p x :=
42   rfl
43 
44 /-- The presentation map for a finite or infinite family of operator seeds. -/
45 noncomputable def seedPresentation {ι : Type w} (T : Module.End k X)
46     (v : ι → X) : (ι →₀ k[X]) →ₗ[k] X :=
47   Finsupp.lsum k fun i ↦ evalVector T (v i)
48 
49 /-- All polynomial translates of a family of seeds. -/
50 noncomputable def orbitFamily {ι : Type w} (T : Module.End k X) (v : ι → X) :
51     ι × k[X] → X :=
52   fun ip ↦ aeval T ip.2 (v ip.1)
53 
54 /-- A family generates under the polynomial algebra `k[T]`. -/
55 def FamilyGenerates {ι : Type w} (T : Module.End k X) (v : ι → X) : Prop :=
56   Submodule.span k (Set.range (orbitFamily T v)) = ⊤
57 
58 /-- There are at most `r` operator seeds. -/
59 def SeedNumberLE (T : Module.End k X) (r : ℕ) : Prop :=
60   ∃ v : Fin r → X, FamilyGenerates T v
61 
62 /-- Intertwining `T` with a scalar automatically intertwines every polynomial in `T`. -/
63 theorem eval_intertwining_of_map_T_eq_smul
64     {Y : Type w} [AddCommGroup Y] [Module k Y]
65     (T : Module.End k X) (q : X →ₗ[k] Y) (eigenvalue : k)
66     (hT : ∀ x : X, q (T x) = eigenvalue • q x) :
67     ∀ (p : k[X]) (x : X),
68       q (aeval T p x) = p.eval eigenvalue • q x := by
69   have hpow : ∀ (n : ℕ) (x : X),
70       q ((T ^ n) x) = eigenvalue ^ n • q x := by
71     intro n x
72     induction n with
73     | zero => simp
74     | succ n ih =>
75         rw [pow_succ', Module.End.mul_apply, hT, ih]
76         simp [pow_succ', smul_smul]
77   intro p x
78   induction p using Polynomial.induction_on' with
79   | add p q hp hq => simp [map_add, hp, hq, add_smul]
80   | monomial n a =>
81       simp [aeval_monomial, hpow, smul_smul]
82 
83 /-- Polynomial functional calculus on a single eigenvector. -/
84 theorem aeval_apply_of_eigenvector
85     (T : Module.End k X) (eigenvalue : k) (x : X)
86     (hx : T x = eigenvalue • x) (p : k[X]) :
87     aeval T p x = p.eval eigenvalue • x := by
88   have hpow : ∀ n : ℕ, (T ^ n) x = eigenvalue ^ n • x := by
89     intro n
90     induction n with
91     | zero => simp
92     | succ n ih =>
93         rw [pow_succ', Module.End.mul_apply, ih, map_smul, hx]
94         simp [pow_succ', smul_smul, mul_comm]
95   induction p using Polynomial.induction_on' with
96   | add p q hp hq => simp [map_add, hp, hq, add_smul]
97   | monomial n a => simp [aeval_monomial, hpow, smul_smul, mul_comm]
98 
99 /--
100 A scalar quotient gives the geometric-multiplicity lower bound.  This is the
101 precise Nakayama-style obstruction used in the paper: after passing to a
102 quotient on which `T` is the scalar `λ`, every polynomial orbit of one seed
103 collapses to the line through that seed's image.
104 -/
105 theorem finrank_le_card_of_generates_of_scalar_factor
106     {Y : Type w} [AddCommGroup Y] [Module k Y] [FiniteDimensional k Y]
107     {ι : Type*} [Fintype ι]
108     (T : Module.End k X) (v : ι → X) (q : X →ₗ[k] Y) (hq : Function.Surjective q)
109     (eigenvalue : k)
110     (hintertwine : ∀ (p : k[X]) (x : X),
111       q (aeval T p x) = p.eval eigenvalue • q x)
112     (hgen : FamilyGenerates T v) :
113     Module.finrank k Y ≤ Fintype.card ι := by
114   have hspan : Submodule.span k (Set.range fun i ↦ q (v i)) = ⊤ := by
115     apply top_unique
116     intro y _hy
117     obtain ⟨x, rfl⟩ := hq y
118     have hx : x ∈ Submodule.span k (Set.range (orbitFamily T v)) := by
119       rw [hgen]
120       trivial
121     refine Submodule.span_induction (p := fun z _ ↦
122       q z ∈ Submodule.span k (Set.range fun i ↦ q (v i))) ?_ ?_ ?_ ?_ hx
123     · intro z hz
124       obtain ⟨⟨i, p⟩, rfl⟩ := hz
125       change q (aeval T p (v i)) ∈ _
126       rw [hintertwine]
127       exact Submodule.smul_mem _ _
128         (Submodule.subset_span (Set.mem_range_self i))
129     · simp
130     · intro x y _ _ hx hy
131       simpa using Submodule.add_mem _ hx hy
132     · intro a x _ hx
133       simpa using Submodule.smul_mem _ a hx
134   exact finrank_le_of_span_eq_top (R := k) hspan
135 
136 /-- The geometric-multiplicity obstruction in coordinate form. -/
137 theorem multiplicity_le_of_generates
138     {ι : Type*} [Fintype ι]
139     (T : Module.End k X) (v : ι → X) (m : ℕ)
140     (q : X →ₗ[k] (Fin m → k)) (hq : Function.Surjective q) (eigenvalue : k)
141     (hintertwine : ∀ (p : k[X]) (x : X),
142       q (aeval T p x) = p.eval eigenvalue • q x)
143     (hgen : FamilyGenerates T v) :
144     m ≤ Fintype.card ι := by
145   simpa [Module.finrank_pi] using
146     finrank_le_card_of_generates_of_scalar_factor T v q hq eigenvalue hintertwine hgen
147 
148 /-- The span of polynomial translates is invariant under the operator. -/
149 theorem operator_mem_span_orbit_of_mem
150     {ι : Type*} (T : Module.End k X) (v : ι → X) {x : X}
151     (hx : x ∈ Submodule.span k (Set.range (orbitFamily T v))) :
152     T x ∈ Submodule.span k (Set.range (orbitFamily T v)) := by
153   classical
154   refine Submodule.span_induction (p := fun z _ ↦
155     T z ∈ Submodule.span k (Set.range (orbitFamily T v))) ?_ ?_ ?_ ?_ hx
156   · intro z hz
157     obtain ⟨⟨i, p⟩, rfl⟩ := hz
158     apply Submodule.subset_span
159     refine ⟨(i, Polynomial.X * p), ?_⟩
160     simp [orbitFamily, map_mul, Module.End.mul_apply]
161   · simp
162   · intro x y _ _ hx hy
163     simpa using Submodule.add_mem _ hx hy
164   · intro a x _ hx
165     simpa using Submodule.smul_mem _ a hx
166 
167 /--
168 The polynomial-orbit span is closed under every polynomial in `T`, not only
169 under `T` itself.  This is the key closure fact behind the comparison with the
170 actual image algebra `k[T]` below.
171 -/
172 theorem aeval_mem_span_orbit_of_mem
173     {iota : Type*} (T : Module.End k X) (v : iota → X) (p : k[X]) {x : X}
174     (hx : x ∈ Submodule.span k (Set.range (orbitFamily T v))) :
175     aeval T p x ∈ Submodule.span k (Set.range (orbitFamily T v)) := by
176   classical
177   refine Submodule.span_induction (p := fun z _ ↦
178     aeval T p z ∈ Submodule.span k (Set.range (orbitFamily T v))) ?_ ?_ ?_ ?_ hx
179   · intro z hz
180     obtain ⟨⟨i, q⟩, rfl⟩ := hz
181     apply Submodule.subset_span
182     refine ⟨(i, p * q), ?_⟩
183     simp [orbitFamily, map_mul, Module.End.mul_apply]
184   · simp
185   · intro x y _ _ hx hy
186     simpa using Submodule.add_mem _ hx hy
187   · intro a x _ hx
188     simpa using Submodule.smul_mem _ a hx
189 
190 /-- The concrete image algebra generated by the single operator `T`. -/
191 def operatorAlgebra (T : Module.End k X) : Subalgebra k (Module.End k X) :=
192   Algebra.adjoin k {T}
193 
194 /--
195 The algebraic span of a seed family over the genuine image algebra `k[T]`,
196 after restriction of scalars to `k`, is exactly its polynomial-orbit span.
197 This proves the comparison rather than postulating it.
198 -/
199 theorem restrictScalars_span_operatorAlgebra_eq_span_orbit
200     {iota : Type*} (T : Module.End k X) (v : iota → X) :
201     (Submodule.span (operatorAlgebra T) (Set.range v)).restrictScalars k =
202       Submodule.span k (Set.range (orbitFamily T v)) := by
203   classical
204   let P : Submodule (operatorAlgebra T) X :=
205     { carrier := Submodule.span k (Set.range (orbitFamily T v))
206       zero_mem' := Submodule.zero_mem _
207       add_mem' := fun hx hy ↦ Submodule.add_mem _ hx hy
208       smul_mem' := by
209         intro a x hx
210         have ha : (a : Module.End k X) ∈ Algebra.adjoin k ({T} : Set (Module.End k X)) :=
211           a.property
212         rw [Algebra.adjoin_singleton_eq_range_aeval] at ha
213         obtain ⟨p, hp⟩ := ha
214         have hpx := aeval_mem_span_orbit_of_mem T v p hx
215         change (a : Module.End k X) x ∈
216           Submodule.span k (Set.range (orbitFamily T v))
217         rw [← hp]
218         exact hpx }
219   apply le_antisymm
220   · change Submodule.span (operatorAlgebra T) (Set.range v) ≤ P
221     apply Submodule.span_le.2
222     rintro _ ⟨i, rfl⟩
223     change v i ∈ Submodule.span k (Set.range (orbitFamily T v))
224     apply Submodule.subset_span
225     refine ⟨(i, 1), ?_⟩
226     simp [orbitFamily]
227   · apply Submodule.span_le.2
228     rintro _ ⟨⟨i, p⟩, rfl⟩
229     change aeval T p (v i) ∈
230       (Submodule.span (operatorAlgebra T) (Set.range v)).restrictScalars k
231     let a : operatorAlgebra T :=
232       ⟨aeval T p, Polynomial.aeval_mem_adjoin_singleton k T⟩
233     have hv : v i ∈ Submodule.span (operatorAlgebra T) (Set.range v) :=
234       Submodule.subset_span (Set.mem_range_self i)
235     have hav := Submodule.smul_mem
236       (Submodule.span (operatorAlgebra T) (Set.range v)) a hv
237     change a • v i ∈ Submodule.span (operatorAlgebra T) (Set.range v)
238     exact hav
239 
240 /--
241 A seed family generates by polynomial orbits iff it generates as a module over
242 the actual image algebra `k[T]`.
243 -/
244 theorem familyGenerates_iff_operatorAlgebra_familyGenerates
245     {iota : Type*} (T : Module.End k X) (v : iota → X) :
246     FamilyGenerates T v ↔
247       Komorebi.SeedRankBasics.FamilyGenerates (operatorAlgebra T) X v := by
248   rw [FamilyGenerates, Komorebi.SeedRankBasics.FamilyGenerates,
249     Komorebi.SeedRankBasics.Generates,
250     ← restrictScalars_span_operatorAlgebra_eq_span_orbit T v]
251   exact Submodule.restrictScalars_eq_top_iff k (operatorAlgebra T) X
252 
253 /-- The corresponding exact comparison for the natural `at most n` predicate. -/
254 theorem seedNumberLE_iff_operatorAlgebra_family
255     (T : Module.End k X) (n : ℕ) :
256     SeedNumberLE T n ↔
257       ∃ v : Fin n → X,
258         Komorebi.SeedRankBasics.FamilyGenerates (operatorAlgebra T) X v := by
259   simp only [SeedNumberLE, familyGenerates_iff_operatorAlgebra_familyGenerates]
260 
261 /--
262 An exact natural-valued polynomial seed number is the canonical
263 `seedFinrank` of the image algebra `k[T]`.  Finite generation is derived from
264 the upper-bound half of `hLeast`; it is not an additional assumption.
265 -/
266 theorem operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast
267     (T : Module.End k X) (R : ℕ)
268     (hLeast : IsLeast {r : ℕ | SeedNumberLE T r} R) :
269     Komorebi.SeedRankBasics.seedFinrank (operatorAlgebra T) X = R := by
270   classical
271   obtain ⟨v, hvPolynomial⟩ := hLeast.1
272   have hvAlgebra :=
273     (familyGenerates_iff_operatorAlgebra_familyGenerates T v).mp hvPolynomial
274   change Submodule.span (operatorAlgebra T) (Set.range v) = ⊤ at hvAlgebra
275   have hfg : (⊤ : Submodule (operatorAlgebra T) X).FG := by
276     rw [Submodule.fg_def]
277     exact ⟨Set.range v, Set.finite_range v, hvAlgebra⟩
278   let _ : Module.Finite (operatorAlgebra T) X := Module.finite_def.mpr hfg
279   apply Nat.le_antisymm
280   · change (⊤ : Submodule (operatorAlgebra T) X).spanFinrank ≤ R
281     rw [← hvAlgebra]
282     refine (Submodule.spanFinrank_span_le_ncard_of_finite
283       (Set.finite_range v)).trans ?_
284     rw [← Nat.card_coe_set_eq]
285     simpa using Finite.card_range_le v
286   · obtain ⟨s, hsCard, hsSpan⟩ :=
287       Submodule.FG.exists_span_finset_card_eq_spanFinrank
288         (R := operatorAlgebra T) (M := X) Module.Finite.fg_top
289     let w : Fin s.card → X := fun i ↦ ((s.equivFin).symm i : s)
290     have hrange : Set.range w = (s : Set X) := by
291       ext x
292       constructor
293       · rintro ⟨i, rfl⟩
294         exact ((s.equivFin).symm i).property
295       · intro hx
296         refine ⟨s.equivFin ⟨x, hx⟩, ?_⟩
297         simp [w]
298     have hwAlgebra :
299         Komorebi.SeedRankBasics.FamilyGenerates (operatorAlgebra T) X w := by
300       change Submodule.span (operatorAlgebra T) (Set.range w) = ⊤
301       rw [hrange, hsSpan]
302     have hwPolynomial : FamilyGenerates T w :=
303       (familyGenerates_iff_operatorAlgebra_familyGenerates T w).mpr hwAlgebra
304     have hmin : R ≤ s.card := hLeast.2 ⟨w, hwPolynomial⟩
305     rw [Komorebi.SeedRankBasics.seedFinrank, ← hsCard]
306     exact hmin
307 
308 /--
309 Cardinal-valued form of the same bridge: the canonical seed rank of `X` as a
310 module over the image algebra `k[T]` is the finite cardinal `R`.
311 -/
312 theorem operatorAlgebra_seedRank_eq_of_seedNumber_isLeast
313     (T : Module.End k X) (R : ℕ)
314     (hLeast : IsLeast {r : ℕ | SeedNumberLE T r} R) :
315     Komorebi.SeedRankBasics.seedRank (operatorAlgebra T) X = (R : Cardinal) := by
316   classical
317   obtain ⟨v, hvPolynomial⟩ := hLeast.1
318   have hvAlgebra :=
319     (familyGenerates_iff_operatorAlgebra_familyGenerates T v).mp hvPolynomial
320   change Submodule.span (operatorAlgebra T) (Set.range v) = ⊤ at hvAlgebra
321   have hfg : (⊤ : Submodule (operatorAlgebra T) X).FG := by
322     rw [Submodule.fg_def]
323     exact ⟨Set.range v, Set.finite_range v, hvAlgebra⟩
324   let _ : Module.Finite (operatorAlgebra T) X := Module.finite_def.mpr hfg
325   rw [Komorebi.SeedRankBasics.seedRank_eq_seedFinrank,
326     operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast T R hLeast]
327 
328 /-- A spanning Krylov orbit is, in particular, a one-seed polynomial presentation. -/
329 theorem familyGenerates_singleton_of_pow_span_eq_top
330     (T : Module.End k X) (x : X)
331     (hpow : Submodule.span k (Set.range fun n : ℕ ↦ (T ^ n) x) = ⊤) :
332     FamilyGenerates T (fun _ : Fin 1 ↦ x) := by
333   rw [FamilyGenerates]
334   apply top_unique
335   rw [← hpow]
336   apply Submodule.span_le.2
337   rintro _ ⟨n, rfl⟩
338   apply Submodule.subset_span
339   refine ⟨((0 : Fin 1), Polynomial.X ^ n), ?_⟩
340   simp [orbitFamily]
341 
342 /-- A nonzero module cannot be generated by the empty seed family. -/
343 theorem not_seedNumberLE_zero [Nontrivial X] (T : Module.End k X) :
344     ¬ SeedNumberLE T 0 := by
345   rintro ⟨v, hv⟩
346   have hempty : Set.range (orbitFamily T v) = ∅ := by
347     ext x
348     simp
349   rw [FamilyGenerates, hempty, Submodule.span_empty] at hv
350   exact bot_ne_top hv
351 
352 /-- On a nonzero module, a cyclic vector makes one the exact seed number. -/
353 theorem seedNumber_one_isLeast_of_cyclic [Nontrivial X]
354     (T : Module.End k X) (hcyclic : SeedNumberLE T 1) :
355     IsLeast {r : ℕ | SeedNumberLE T r} 1 := by
356   constructor
357   · exact hcyclic
358   · intro r hr
359     have hr0 : r ≠ 0 := by
360       intro h
361       subst r
362       exact not_seedNumberLE_zero T hr
363     omega
364 
365 /-- The zero module has exact operator seed number zero, matching the paper's convention. -/
366 theorem seedNumber_zero_isLeast_of_subsingleton [Subsingleton X]
367     (T : Module.End k X) :
368     IsLeast {r : ℕ | SeedNumberLE T r} 0 := by
369   constructor
370   · refine ⟨Fin.elim0, ?_⟩
371     rw [FamilyGenerates]
372     subsingleton
373   · intro r _hr
374     exact Nat.zero_le r
375 
376 end PolynomialGeneration
377 
378 section PrimaryDecomposition
379 
380 variable {k : Type u} [Field k]
381 variable {X : Type v} [AddCommGroup X] [Module k X]
382 variable {Λ : Type w} [Fintype Λ]
383 
384 /--
385 The `a`th padded sum of the `a`th cyclic block generator in every primary
386 packet.  Blocks with index at most `a` contribute zero.
387 -/
388 noncomputable def paddedBlockSum (R : ℕ) (multiplicity : Λ → ℕ)
389     (blockGenerator : ∀ eigen : Λ, Fin (multiplicity eigen) → X)
390     (a : Fin R) : X :=
391   ∑ eigen : Λ,
392     if h : a.val < multiplicity eigen then
393       blockGenerator eigen ⟨a.val, h⟩
394     else 0
395 
396 /--
397 The upper half of the Jordan argument.  If all cyclic block generators
398 generate, and polynomial primary projectors recover every block generator
399 from the corresponding padded sum, then `R` padded sums generate.
400 -/
401 theorem paddedBlockSums_generate
402     (T : Module.End k X) (R : ℕ) (multiplicity : Λ → ℕ)
403     (blockGenerator : ∀ eigen : Λ, Fin (multiplicity eigen) → X)
404     (hbound : ∀ eigen, multiplicity eigen ≤ R)
405     (hblocks : FamilyGenerates T
406       (fun z : Σ eigen : Λ, Fin (multiplicity eigen) =>
407         blockGenerator z.1 z.2))
408     (hextract : ∀ (eigen : Λ) (j : Fin (multiplicity eigen)),
409       ∃ p : k[X],
410         aeval T p
411           (paddedBlockSum R multiplicity blockGenerator
412             ⟨j.val, lt_of_lt_of_le j.isLt (hbound eigen)⟩) =
413           blockGenerator eigen j) :
414     FamilyGenerates T (paddedBlockSum R multiplicity blockGenerator) := by
415   classical
416   rw [FamilyGenerates]
417   apply top_unique
418   intro x _hx
419   have hx : x ∈ Submodule.span k
420       (Set.range (orbitFamily T
421         (fun z : Σ eigen : Λ, Fin (multiplicity eigen) =>
422           blockGenerator z.1 z.2))) := by
423     rw [hblocks]
424     trivial
425   refine Submodule.span_induction (p := fun z _ ↦
426     z ∈ Submodule.span k
427       (Set.range (orbitFamily T
428         (paddedBlockSum R multiplicity blockGenerator)))) ?_ ?_ ?_ ?_ hx
429   · intro z hz
430     obtain ⟨⟨⟨eigen, j⟩, q⟩, rfl⟩ := hz
431     obtain ⟨p, hp⟩ := hextract eigen j
432     let a : Fin R := ⟨j.val, lt_of_lt_of_le j.isLt (hbound eigen)⟩
433     have horbit :
434         aeval T (q * p)
435             (paddedBlockSum R multiplicity blockGenerator a) ∈
436           Set.range (orbitFamily T
437             (paddedBlockSum R multiplicity blockGenerator)) := by
438       exact ⟨(a, q * p), rfl⟩
439     apply Submodule.subset_span at horbit
440     rw [orbitFamily]
441     change aeval T q (blockGenerator eigen j) ∈ _
442     rw [← hp, ← Module.End.mul_apply, ← map_mul]
443     exact horbit
444   · exact Submodule.zero_mem _
445   · intro x y _ _ hx hy
446     exact Submodule.add_mem _ hx hy
447   · intro c x _ hx
448     exact Submodule.smul_mem _ c hx
449 
450 /--
451 Exact single-operator seed number from explicit primary/Jordan data.
452 
453 `q eigen` is the semisimple top
454 `X_eigen / (T-eigenvalue)X_eigen`; its dimension is the number of Jordan
455 blocks.  `hextract` is supplied by the Chinese-remainder primary projectors.
456 Thus these hypotheses are precisely the two classical decomposition facts
457 used in the paper, while both generator inequalities are proved here.
458 -/
459 theorem singleOperator_seedNumber_isLeast_of_primary_decomposition
460     (T : Module.End k X) (R : ℕ)
461     (multiplicity : Λ → ℕ) (eigenvalue : Λ → k)
462     (blockGenerator : ∀ eigen : Λ, Fin (multiplicity eigen) → X)
463     (hbound : ∀ eigen, multiplicity eigen ≤ R)
464     (maxEigen : Λ) (hmax : multiplicity maxEigen = R)
465     (hblocks : FamilyGenerates T
466       (fun z : Σ eigen : Λ, Fin (multiplicity eigen) =>
467         blockGenerator z.1 z.2))
468     (hextract : ∀ (eigen : Λ) (j : Fin (multiplicity eigen)),
469       ∃ p : k[X],
470         aeval T p
471           (paddedBlockSum R multiplicity blockGenerator
472             ⟨j.val, lt_of_lt_of_le j.isLt (hbound eigen)⟩) =
473           blockGenerator eigen j)
474     (q : ∀ eigen : Λ, X →ₗ[k] (Fin (multiplicity eigen) → k))
475     (hq : ∀ eigen, Function.Surjective (q eigen))
476     (hqT : ∀ (eigen : Λ) (p : k[X]) (x : X),
477       q eigen (aeval T p x) = p.eval (eigenvalue eigen) • q eigen x) :
478     IsLeast {r : ℕ | SeedNumberLE T r} R := by
479   constructor
480   · exact ⟨paddedBlockSum R multiplicity blockGenerator,
481       paddedBlockSums_generate T R multiplicity blockGenerator hbound hblocks hextract⟩
482   · intro r hr
483     obtain ⟨v, hv⟩ := hr
484     have hle := multiplicity_le_of_generates T v (multiplicity maxEigen)
485       (q maxEigen) (hq maxEigen) (eigenvalue maxEigen) (hqT maxEigen) hv
486     simpa [hmax] using hle
487 
488 /--
489 Literal canonical-invariant form of the primary-decomposition theorem.  The
490 two equalities transfer the proved natural minimum to Mathlib's
491 `spanFinrank`/`spanRank` definitions for the genuine image algebra `k[T]`.
492 -/
493 theorem singleOperator_operatorAlgebra_seedRanks_eq_of_primary_decomposition
494     (T : Module.End k X) (R : ℕ)
495     (multiplicity : Λ → ℕ) (eigenvalue : Λ → k)
496     (blockGenerator : ∀ eigen : Λ, Fin (multiplicity eigen) → X)
497     (hbound : ∀ eigen, multiplicity eigen ≤ R)
498     (maxEigen : Λ) (hmax : multiplicity maxEigen = R)
499     (hblocks : FamilyGenerates T
500       (fun z : Σ eigen : Λ, Fin (multiplicity eigen) ↦
501         blockGenerator z.1 z.2))
502     (hextract : ∀ (eigen : Λ) (j : Fin (multiplicity eigen)),
503       ∃ p : k[X],
504         aeval T p
505           (paddedBlockSum R multiplicity blockGenerator
506             ⟨j.val, lt_of_lt_of_le j.isLt (hbound eigen)⟩) =
507           blockGenerator eigen j)
508     (q : ∀ eigen : Λ, X →ₗ[k] (Fin (multiplicity eigen) → k))
509     (hq : ∀ eigen, Function.Surjective (q eigen))
510     (hqT : ∀ (eigen : Λ) (p : k[X]) (x : X),
511       q eigen (aeval T p x) = p.eval (eigenvalue eigen) • q eigen x) :
512     Komorebi.SeedRankBasics.seedFinrank (operatorAlgebra T) X = R ∧
513       Komorebi.SeedRankBasics.seedRank (operatorAlgebra T) X = (R : Cardinal) := by
514   let hLeast := singleOperator_seedNumber_isLeast_of_primary_decomposition
515     T R multiplicity eigenvalue blockGenerator hbound maxEigen hmax hblocks
516       hextract q hq hqT
517   exact ⟨operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast T R hLeast,
518     operatorAlgebra_seedRank_eq_of_seedNumber_isLeast T R hLeast⟩
519 
520 /-- One operator is cyclic when one polynomial seed suffices. -/
521 def HasCyclicVector (T : Module.End k X) : Prop :=
522   SeedNumberLE T 1
523 
524 /-- Every represented eigenspace has dimension one. -/
525 def AllGeometricMultiplicitiesOne (geometricMultiplicity : Λ → ℕ) : Prop :=
526   ∀ eigen, geometricMultiplicity eigen = 1
527 
528 /-- The represented Jordan form has exactly one block for every eigenvalue. -/
529 def OneJordanBlockPerEigenvalue (blockMultiplicity : Λ → ℕ) : Prop :=
530   ∀ eigen, blockMultiplicity eigen = 1
531 
532 /-- A positive exact seed number is one exactly when the operator is cyclic. -/
533 theorem hasCyclicVector_iff_seedNumber_eq_one
534     (T : Module.End k X) (R : ℕ) (hR : 0 < R)
535     (hLeast : IsLeast {r : ℕ | SeedNumberLE T r} R) :
536     HasCyclicVector T ↔ R = 1 := by
537   constructor
538   · intro hcyc
539     exact Nat.eq_one_of_dvd_one (Nat.dvd_one.mpr (Nat.le_antisymm (hLeast.2 hcyc) hR))
540   · rintro rfl
541     exact hLeast.1
542 
543 omit [Fintype Λ] in
544 /--
545 The exact cyclic/nonderogatory criterion in block language.  Positivity says
546 that every listed eigenvalue actually occurs; `hmax` says one of them realizes
547 the maximum geometric multiplicity.
548 -/
549 theorem hasCyclicVector_iff_one_block_per_eigenvalue
550     (T : Module.End k X) (R : ℕ) (multiplicity : Λ → ℕ)
551     (hpositive : ∀ eigen, 0 < multiplicity eigen)
552     (hbound : ∀ eigen, multiplicity eigen ≤ R)
553     (maxEigen : Λ) (hmax : multiplicity maxEigen = R)
554     (hLeast : IsLeast {r : ℕ | SeedNumberLE T r} R) :
555     HasCyclicVector T ↔ ∀ eigen, multiplicity eigen = 1 := by
556   have hR : 0 < R := by simpa [← hmax] using hpositive maxEigen
557   rw [hasCyclicVector_iff_seedNumber_eq_one T R hR hLeast]
558   constructor
559   · intro hOne eigen
560     apply Nat.le_antisymm
561     · simpa [hOne] using hbound eigen
562     · exact hpositive eigen
563   · intro hall
564     exact hmax.symm.trans (hall maxEigen)
565 
566 omit [Fintype Λ] in
567 /--
568 Four-way cyclic-matrix criterion once the standard canonical-form polynomial
569 bridge is supplied.  The bridge is exactly the classical statement that the
570 minimal and characteristic polynomials agree iff there is one Jordan block
571 for each eigenvalue.
572 -/
573 theorem cyclic_matrix_criterion_of_primary_decomposition
574     [FiniteDimensional k X]
575     (T : Module.End k X) (R : ℕ) (multiplicity : Λ → ℕ)
576     (hpositive : ∀ eigen, 0 < multiplicity eigen)
577     (hbound : ∀ eigen, multiplicity eigen ≤ R)
578     (maxEigen : Λ) (hmax : multiplicity maxEigen = R)
579     (hLeast : IsLeast {r : ℕ | SeedNumberLE T r} R)
580     (hpoly : minpoly k T = T.charpoly ↔
581       ∀ eigen, multiplicity eigen = 1) :
582     HasCyclicVector T ↔
583       (∀ eigen, multiplicity eigen = 1) ∧ minpoly k T = T.charpoly := by
584   rw [hasCyclicVector_iff_one_block_per_eigenvalue
585     T R multiplicity hpositive hbound maxEigen hmax hLeast]
586   constructor
587   · intro h
588     exact ⟨h, hpoly.mpr h⟩
589   · exact fun h ↦ h.1
590 
591 omit [Fintype Λ] in
592 /--
593 The cyclic-matrix criterion as a literal four-condition equivalence chain:
594 cyclic vector, geometric multiplicity one, one Jordan block per eigenvalue,
595 and equality of minimal and characteristic polynomials.  The middle bridge
596 records the canonical-form fact that geometric multiplicity counts Jordan
597 blocks; the final bridge is the remaining minpoly/charpoly classification
598 fact.
599 -/
600 theorem cyclic_matrix_four_way_iff_of_primary_decomposition
601     [FiniteDimensional k X]
602     (T : Module.End k X) (R : ℕ)
603     (geometricMultiplicity blockMultiplicity : Λ → ℕ)
604     (hpositive : ∀ eigen, 0 < geometricMultiplicity eigen)
605     (hbound : ∀ eigen, geometricMultiplicity eigen ≤ R)
606     (maxEigen : Λ) (hmax : geometricMultiplicity maxEigen = R)
607     (hLeast : IsLeast {r : ℕ | SeedNumberLE T r} R)
608     (hgeometric_eq_blocks : ∀ eigen,
609       geometricMultiplicity eigen = blockMultiplicity eigen)
610     (hpoly : minpoly k T = T.charpoly ↔
611       OneJordanBlockPerEigenvalue blockMultiplicity) :
612     (HasCyclicVector T ↔
613         AllGeometricMultiplicitiesOne geometricMultiplicity) ∧
614       (AllGeometricMultiplicitiesOne geometricMultiplicity ↔
615         OneJordanBlockPerEigenvalue blockMultiplicity) ∧
616       (OneJordanBlockPerEigenvalue blockMultiplicity ↔
617         minpoly k T = T.charpoly) := by
618   have hcyclic : HasCyclicVector T ↔
619       AllGeometricMultiplicitiesOne geometricMultiplicity := by
620     exact hasCyclicVector_iff_one_block_per_eigenvalue
621       T R geometricMultiplicity hpositive hbound maxEigen hmax hLeast
622   have hmiddle : AllGeometricMultiplicitiesOne geometricMultiplicity ↔
623       OneJordanBlockPerEigenvalue blockMultiplicity := by
624     constructor
625     · intro h eigen
626       rw [← hgeometric_eq_blocks eigen]
627       exact h eigen
628     · intro h eigen
629       rw [hgeometric_eq_blocks eigen]
630       exact h eigen
631   exact ⟨hcyclic, hmiddle, hpoly.symm⟩
632 
633 end PrimaryDecomposition
634 
635 section Diagonalizable
636 
637 variable {k : Type u} [Field k]
638 variable {X : Type v} [AddCommGroup X] [Module k X]
639 variable {Λ : Type w} [Fintype Λ]
640 
641 /-- Every basis is an operator-generating family, using constant polynomials. -/
642 theorem basis_generates_under_operator
643     {I : Type*} [Fintype I] (T : Module.End k X) (b : Module.Basis I k X) :
644     FamilyGenerates T b := by
645   rw [FamilyGenerates]
646   apply top_unique
647   rw [← b.span_eq]
648   apply Submodule.span_mono
649   rintro _ ⟨i, rfl⟩
650   refine ⟨(i, 1), ?_⟩
651   simp [orbitFamily]
652 
653 /-- Coordinates in one eigenspace packet of a basis indexed by eigenvalue and multiplicity. -/
654 noncomputable def basisPacketCoordinate
655     (multiplicity : Λ → ℕ)
656     (b : Module.Basis (Σ eigen : Λ, Fin (multiplicity eigen)) k X)
657     (eigen : Λ) : X →ₗ[k] (Fin (multiplicity eigen) → k) :=
658   LinearMap.pi fun j ↦
659     (Finsupp.lapply (R := k) (M := k)
660       (⟨eigen, j⟩ : Σ eigen : Λ, Fin (multiplicity eigen))).comp
661       b.repr.toLinearMap
662 
663 omit [Fintype Λ] in
664 @[simp]
665 theorem basisPacketCoordinate_apply
666     (multiplicity : Λ → ℕ)
667     (b : Module.Basis (Σ eigen : Λ, Fin (multiplicity eigen)) k X)
668     (eigen : Λ) (x : X) (j : Fin (multiplicity eigen)) :
669     basisPacketCoordinate multiplicity b eigen x j =
670       b.repr x ⟨eigen, j⟩ :=
671   rfl
672 
673 omit [Fintype Λ] in
674 /-- Every basis packet-coordinate map is onto. -/
675 theorem basisPacketCoordinate_surjective
676     (multiplicity : Λ → ℕ)
677     (b : Module.Basis (Σ eigen : Λ, Fin (multiplicity eigen)) k X)
678     (eigen : Λ) :
679     Function.Surjective (basisPacketCoordinate multiplicity b eigen) := by
680   classical
681   intro y
682   let x : X := ∑ j : Fin (multiplicity eigen), y j • b ⟨eigen, j⟩
683   refine ⟨x, ?_⟩
684   funext j
685   simp [basisPacketCoordinate, x, Finsupp.single_apply]
686 
687 omit [Fintype Λ] in
688 /-- Packet coordinates intertwine a diagonal operator with its eigenvalue. -/
689 theorem basisPacketCoordinate_map_T
690     (T : Module.End k X) (multiplicity : Λ → ℕ) (eigenvalue : Λ → k)
691     (b : Module.Basis (Σ eigen : Λ, Fin (multiplicity eigen)) k X)
692     (hEigen : ∀ z : Σ eigen : Λ, Fin (multiplicity eigen),
693       T (b z) = eigenvalue z.1 • b z)
694     (eigen : Λ) (x : X) :
695     basisPacketCoordinate multiplicity b eigen (T x) =
696       eigenvalue eigen • basisPacketCoordinate multiplicity b eigen x := by
697   classical
698   have hmap :
699       (basisPacketCoordinate multiplicity b eigen).comp T =
700         eigenvalue eigen • basisPacketCoordinate multiplicity b eigen := by
701     apply b.ext
702     intro z
703     rcases z with ⟨other, j⟩
704     by_cases h : other = eigen
705     · subst other
706       simp [basisPacketCoordinate, hEigen]
707     · ext a
708       simp [basisPacketCoordinate, hEigen, h]
709   exact LinearMap.congr_fun hmap x
710 
711 /--
712 For a diagonalizable operator, the seed number is the maximum eigenspace
713 multiplicity.  The input `hproject` is an explicit Lagrange spectral-projector
714 certificate; distinct eigenvalues supply it in the usual diagonalization
715 theorem.
716 -/
717 theorem diagonalizable_seedNumber_isLeast
718     (T : Module.End k X) (R : ℕ)
719     (multiplicity : Λ → ℕ) (eigenvalue : Λ → k)
720     (b : Module.Basis (Σ eigen : Λ, Fin (multiplicity eigen)) k X)
721     (hEigen : ∀ z : Σ eigen : Λ, Fin (multiplicity eigen),
722       T (b z) = eigenvalue z.1 • b z)
723     (hbound : ∀ eigen, multiplicity eigen ≤ R)
724     (maxEigen : Λ) (hmax : multiplicity maxEigen = R)
725     (projectorPolynomial : Λ → k[X])
726     (hproject : ∀ (eigen : Λ) (j : Fin (multiplicity eigen)),
727       aeval T (projectorPolynomial eigen)
728         (paddedBlockSum R multiplicity (fun e j ↦ b ⟨e, j⟩)
729           ⟨j.val, lt_of_lt_of_le j.isLt (hbound eigen)⟩) =
730         b ⟨eigen, j⟩) :
731     IsLeast {r : ℕ | SeedNumberLE T r} R := by
732   let q : ∀ eigen : Λ, X →ₗ[k] (Fin (multiplicity eigen) → k) :=
733     fun eigen ↦ basisPacketCoordinate multiplicity b eigen
734   refine singleOperator_seedNumber_isLeast_of_primary_decomposition
735     T R multiplicity eigenvalue (fun eigen j ↦ b ⟨eigen, j⟩)
736     hbound maxEigen hmax ?_ ?_ q ?_ ?_
737   · exact basis_generates_under_operator T b
738   · intro eigen j
739     exact ⟨projectorPolynomial eigen, hproject eigen j⟩
740   · intro eigen
741     exact basisPacketCoordinate_surjective multiplicity b eigen
742   · intro eigen
743     exact eval_intertwining_of_map_T_eq_smul T (q eigen) (eigenvalue eigen)
744       (basisPacketCoordinate_map_T T multiplicity eigenvalue b hEigen eigen)
745 
746 /--
747 The projector certificate in `diagonalizable_seedNumber_isLeast` is automatic
748 when the listed eigenvalues are distinct: Lagrange interpolation constructs
749 the spectral projectors.
750 -/
751 theorem diagonalizable_seedNumber_isLeast_of_distinct_eigenvalues
752     (T : Module.End k X) (R : ℕ)
753     (multiplicity : Λ → ℕ) (eigenvalue : Λ → k)
754     (b : Module.Basis (Σ eigen : Λ, Fin (multiplicity eigen)) k X)
755     (hEigen : ∀ z : Σ eigen : Λ, Fin (multiplicity eigen),
756       T (b z) = eigenvalue z.1 • b z)
757     (heigenvalue : Function.Injective eigenvalue)
758     (hbound : ∀ eigen, multiplicity eigen ≤ R)
759     (maxEigen : Λ) (hmax : multiplicity maxEigen = R) :
760     IsLeast {r : ℕ | SeedNumberLE T r} R := by
761   classical
762   let projectorPolynomial : Λ → k[X] := fun eigen ↦
763     Lagrange.interpolate Finset.univ eigenvalue
764       (fun other ↦ if other = eigen then 1 else 0)
765   have hprojector (eigen other : Λ) :
766       (projectorPolynomial eigen).eval (eigenvalue other) =
767         if other = eigen then 1 else 0 := by
768     dsimp [projectorPolynomial]
769     exact Lagrange.eval_interpolate_at_node
770       (fun other ↦ if other = eigen then 1 else 0)
771       heigenvalue.injOn (Finset.mem_univ other)
772   apply diagonalizable_seedNumber_isLeast T R multiplicity eigenvalue b hEigen
773     hbound maxEigen hmax projectorPolynomial
774   intro eigen j
775   rw [paddedBlockSum, map_sum]
776   rw [Finset.sum_eq_single eigen]
777   · simp only [j.isLt, dite_true]
778     rw [aeval_apply_of_eigenvector T (eigenvalue eigen) (b ⟨eigen, j⟩)
779       (hEigen ⟨eigen, j⟩) (projectorPolynomial eigen)]
780     rw [hprojector]
781     simp
782   · intro other _hmem hne
783     by_cases hj : j.val < multiplicity other
784     · simp only [hj, dite_true]
785       rw [aeval_apply_of_eigenvector T (eigenvalue other)
786         (b ⟨other, ⟨j.val, hj⟩⟩) (hEigen ⟨other, ⟨j.val, hj⟩⟩)
787         (projectorPolynomial eigen)]
788       rw [hprojector]
789       simp [hne]
790     · simp [hj]
791   · simp
792 
793 /-- A symmetric/diagonalizable graph operator inherits the same maximum-eigenspace formula. -/
794 theorem graph_seedNumber_eq_max_eigenspace_multiplicity
795     (adjacency : Module.End k X) (R : ℕ)
796     (multiplicity : Λ → ℕ) (eigenvalue : Λ → k)
797     (eigenbasis : Module.Basis (Σ eigen : Λ, Fin (multiplicity eigen)) k X)
798     (hEigen : ∀ z : Σ eigen : Λ, Fin (multiplicity eigen),
799       adjacency (eigenbasis z) = eigenvalue z.1 • eigenbasis z)
800     (hbound : ∀ eigen, multiplicity eigen ≤ R)
801     (maxEigen : Λ) (hmax : multiplicity maxEigen = R)
802     (projectorPolynomial : Λ → k[X])
803     (hproject : ∀ (eigen : Λ) (j : Fin (multiplicity eigen)),
804       aeval adjacency (projectorPolynomial eigen)
805         (paddedBlockSum R multiplicity (fun e j ↦ eigenbasis ⟨e, j⟩)
806           ⟨j.val, lt_of_lt_of_le j.isLt (hbound eigen)⟩) =
807         eigenbasis ⟨eigen, j⟩) :
808     IsLeast {r : ℕ | SeedNumberLE adjacency r} R :=
809   diagonalizable_seedNumber_isLeast adjacency R multiplicity eigenvalue eigenbasis
810     hEigen hbound maxEigen hmax projectorPolynomial hproject
811 
812 /--
813 Graph seed rank equals maximum eigenspace multiplicity from a diagonalization
814 with distinct eigenvalue labels; spectral projectors are constructed internally.
815 -/
816 theorem graph_seedNumber_eq_max_eigenspace_multiplicity_of_distinct
817     (adjacency : Module.End k X) (R : ℕ)
818     (multiplicity : Λ → ℕ) (eigenvalue : Λ → k)
819     (eigenbasis : Module.Basis (Σ eigen : Λ, Fin (multiplicity eigen)) k X)
820     (hEigen : ∀ z : Σ eigen : Λ, Fin (multiplicity eigen),
821       adjacency (eigenbasis z) = eigenvalue z.1 • eigenbasis z)
822     (heigenvalue : Function.Injective eigenvalue)
823     (hbound : ∀ eigen, multiplicity eigen ≤ R)
824     (maxEigen : Λ) (hmax : multiplicity maxEigen = R) :
825     IsLeast {r : ℕ | SeedNumberLE adjacency r} R :=
826   diagonalizable_seedNumber_isLeast_of_distinct_eigenvalues adjacency R
827     multiplicity eigenvalue eigenbasis hEigen heigenvalue hbound maxEigen hmax
828 
829 end Diagonalizable
830 
831 section PathGraph
832 
833 variable {k : Type u} [Field k]
834 
835 /-- The all-size endpoint Krylov certificate is an exact one-seed result for paths. -/
836 theorem path_endpoint_seedNumber_isLeast_one (n : ℕ) :
837     IsLeast {r : ℕ |
838       SeedNumberLE (Komorebi.PathGraphKrylov.pathStep k n) r} 1 := by
839   have hpow := Komorebi.PathGraphKrylov.endpoint_isCyclic (R := k) n
840   rw [Komorebi.PathGraphKrylov.IsCyclic] at hpow
841   have hcyclic :
842       SeedNumberLE (Komorebi.PathGraphKrylov.pathStep k n) 1 := by
843     refine ⟨fun _ : Fin 1 ↦ Komorebi.PathGraphKrylov.endpoint k n, ?_⟩
844     exact familyGenerates_singleton_of_pow_span_eq_top
845       (Komorebi.PathGraphKrylov.pathStep k n)
846       (Komorebi.PathGraphKrylov.endpoint k n) hpow
847   exact seedNumber_one_isLeast_of_cyclic
848     (Komorebi.PathGraphKrylov.pathStep k n) hcyclic
849 
850 end PathGraph
851 
852 section CycleGraph
853 
854 variable {k : Type u} [Field k]
855 
856 /-- The adjacency operator of the simple cycle on `n + 3` vertices. -/
857 def cycleAdjacency (n : ℕ) : Module.End k (Fin (n + 3) → k) :=
858   LinearMap.pi fun i : Fin (n + 3) ↦
859     (LinearMap.proj ((finRotate (n + 3)).symm i) :
860       (Fin (n + 3) → k) →ₗ[k] k) +
861     (LinearMap.proj (finRotate (n + 3) i) :
862       (Fin (n + 3) → k) →ₗ[k] k)
863 
864 @[simp]
865 theorem cycleAdjacency_apply (n : ℕ) (x : Fin (n + 3) → k)
866     (i : Fin (n + 3)) :
867     cycleAdjacency n x i =
868       x ((finRotate (n + 3)).symm i) + x (finRotate (n + 3) i) := by
869   simp [cycleAdjacency]
870 
871 /-- Adjacency sends a vertex delta to the sum of its two neighboring deltas. -/
872 theorem cycleAdjacency_basisFun (n : ℕ) (j : Fin (n + 3)) :
873     cycleAdjacency (k := k) n (Pi.basisFun k (Fin (n + 3)) j) =
874       Pi.basisFun k (Fin (n + 3)) (finRotate (n + 3) j) +
875         Pi.basisFun k (Fin (n + 3)) ((finRotate (n + 3)).symm j) := by
876   ext i
877   simp [cycleAdjacency, Pi.basisFun_apply, Pi.single_apply,
878     eq_sub_iff_add_eq, eq_comm, add_comm]
879 
880 /-- Two adjacent vertex deltas, used as the canonical two seeds of a cycle. -/
881 noncomputable def cycleSeeds (n : ℕ) : Fin 2 → (Fin (n + 3) → k) :=
882   fun a ↦ Pi.basisFun k (Fin (n + 3)) ⟨a.val, by omega⟩
883 
884 /-- Two adjacent vertices generate every finite simple cycle adjacency module. -/
885 theorem cycleSeeds_generate (n : ℕ) :
886     FamilyGenerates (cycleAdjacency (k := k) n) (cycleSeeds (k := k) n) := by
887   classical
888   let S : Submodule k (Fin (n + 3) → k) :=
889     Submodule.span k (Set.range
890       (orbitFamily (cycleAdjacency (k := k) n) (cycleSeeds (k := k) n)))
891   have hzero : Pi.basisFun k (Fin (n + 3)) (0 : Fin (n + 3)) ∈ S := by
892     apply Submodule.subset_span
893     refine ⟨((0 : Fin 2), 1), ?_⟩
894     simp [orbitFamily, cycleSeeds]
895   have hone : Pi.basisFun k (Fin (n + 3)) (1 : Fin (n + 3)) ∈ S := by
896     apply Submodule.subset_span
897     refine ⟨((1 : Fin 2), 1), ?_⟩
898     simp [orbitFamily, cycleSeeds]
899   have hvertex : ∀ m : ℕ, ∀ hm : m < n + 3,
900       Pi.basisFun k (Fin (n + 3)) ⟨m, hm⟩ ∈ S := by
901     intro m
902     induction m using Nat.twoStepInduction with
903     | zero =>
904         intro hm
905         simpa using hzero
906     | one =>
907         intro hm
908         simpa using hone
909     | more m hm0 hm1 =>
910         intro hm2
911         have hm0' : m < n + 3 := by omega
912         have hm1' : m + 1 < n + 3 := by omega
913         let j0 : Fin (n + 3) := ⟨m, hm0'⟩
914         let j1 : Fin (n + 3) := ⟨m + 1, hm1'⟩
915         let j2 : Fin (n + 3) := ⟨m + 2, hm2⟩
916         have hj0 : Pi.basisFun k (Fin (n + 3)) j0 ∈ S := hm0 hm0'
917         have hj1 : Pi.basisFun k (Fin (n + 3)) j1 ∈ S := hm1 hm1'
918         have hstep : cycleAdjacency (k := k) n
919             (Pi.basisFun k (Fin (n + 3)) j1) ∈ S :=
920           operator_mem_span_orbit_of_mem
921             (cycleAdjacency (k := k) n) (cycleSeeds (k := k) n) hj1
922         have hnext : finRotate (n + 3) j1 = j2 := by
923           simpa [j1, j2] using
924             (finRotate_of_lt (n := n + 2) (k := m + 1) (by omega))
925         have hprev : (finRotate (n + 3)).symm j1 = j0 := by
926           apply Fin.ext
927           rw [coe_finRotate_symm_of_ne_zero]
928           · simp [j0, j1]
929           · exact Fin.ne_of_val_ne (by simp [j1])
930         rw [cycleAdjacency_basisFun, hnext, hprev] at hstep
931         have hsub := Submodule.sub_mem S hstep hj0
932         simpa [j0, j2] using hsub
933   rw [FamilyGenerates]
934   change S = ⊤
935   apply top_unique
936   rw [← (Pi.basisFun k (Fin (n + 3))).span_eq]
937   apply Submodule.span_le.2
938   rintro _ ⟨j, rfl⟩
939   exact hvertex j.val j.isLt
940 
941 /-- The Fourier row with ratio `z` on a cycle. -/
942 def cycleFourierRow (n : ℕ) (z : k) : (Fin (n + 3) → k) →ₗ[k] k where
943   toFun x := ∑ i : Fin (n + 3), z ^ i.val * x i
944   map_add' x y := by
945     simp only [Pi.add_apply, mul_add, Finset.sum_add_distrib]
946   map_smul' a x := by
947     simp only [Pi.smul_apply, smul_eq_mul]
948     rw [Finset.mul_sum]
949     apply Finset.sum_congr rfl
950     intro i hi
951     simp only [RingHom.id_apply]
952     ring
953 
954 @[simp]
955 theorem cycleFourierRow_basisFun (n : ℕ) (z : k) (j : Fin (n + 3)) :
956     cycleFourierRow n z (Pi.basisFun k (Fin (n + 3)) j) = z ^ j.val := by
957   classical
958   simp [cycleFourierRow, Pi.basisFun_apply, Pi.single_apply]
959 
960 /-- The two conjugate Fourier rows associated with `z` and `z⁻¹`. -/
961 def cycleFourierFactor (n : ℕ) (z : k) :
962     (Fin (n + 3) → k) →ₗ[k] (Fin 2 → k) :=
963   LinearMap.pi fun a ↦ if a = 0 then cycleFourierRow n z else cycleFourierRow n z⁻¹
964 
965 @[simp]
966 theorem cycleFourierFactor_zero (n : ℕ) (z : k) (x : Fin (n + 3) → k) :
967     cycleFourierFactor n z x 0 = cycleFourierRow n z x := by
968   simp [cycleFourierFactor]
969 
970 @[simp]
971 theorem cycleFourierFactor_one (n : ℕ) (z : k) (x : Fin (n + 3) → k) :
972     cycleFourierFactor n z x 1 = cycleFourierRow n z⁻¹ x := by
973   simp [cycleFourierFactor]
974 
975 /-- Distinct Fourier characters give an onto two-dimensional scalar factor. -/
976 theorem cycleFourierFactor_surjective (n : ℕ) (z : k) (hz : z ≠ z⁻¹) :
977     Function.Surjective (cycleFourierFactor n z) := by
978   classical
979   intro y
980   let d : k := z - z⁻¹
981   have hd : d ≠ 0 := sub_ne_zero.mpr hz
982   let bcoef : k := (y 0 - y 1) / d
983   let acoef : k := y 0 - z * bcoef
984   let x : Fin (n + 3) → k :=
985     acoef • Pi.basisFun k (Fin (n + 3)) (0 : Fin (n + 3)) +
986       bcoef • Pi.basisFun k (Fin (n + 3)) (1 : Fin (n + 3))
987   refine ⟨x, ?_⟩
988   funext i
989   fin_cases i
990   · change cycleFourierFactor n z x 0 = y 0
991     rw [cycleFourierFactor_zero]
992     simp only [x, map_add, map_smul, cycleFourierRow_basisFun]
993     simp [acoef, bcoef]
994     ring
995   · change cycleFourierFactor n z x 1 = y 1
996     rw [cycleFourierFactor_one]
997     simp only [x, map_add, map_smul, cycleFourierRow_basisFun]
998     simp [Nat.mod_eq_of_lt (by omega : 1 < n + 3)]
999     dsimp [acoef, bcoef]
1000     field_simp [d, hd]
1001     ring
1002 
1003 /-- The elementary root-of-unity recurrence behind the cycle Fourier eigenvectors. -/
1004 theorem cycle_root_neighbor_identity (n : ℕ) (z : k)
1005     (hroot : z ^ (n + 3) = 1) (j : Fin (n + 3)) :
1006     z ^ (finRotate (n + 3) j).val +
1007         z ^ ((finRotate (n + 3)).symm j).val =
1008       (z + z⁻¹) * z ^ j.val := by
1009   have hz0 : z ≠ 0 := by
1010     intro hz
1011     subst z
1012     norm_num at hroot
1013   have hpred : z ^ (n + 2) = z⁻¹ := by
1014     apply (mul_right_cancel₀ hz0)
1015     have hpow := pow_sub_one_mul (n := n + 3) (by omega) z
1016     simp only [show n + 3 - 1 = n + 2 by omega] at hpow
1017     rw [hpow, hroot]
1018     simp [hz0]
1019   have hpred2 : z ^ (n + 1) = (z⁻¹) ^ 2 := by
1020     apply (mul_right_cancel₀ hz0)
1021     rw [← pow_succ, hpred]
1022     field_simp [hz0]
1023   by_cases hlast : j = Fin.last (n + 2)
1024   · subst j
1025     have hprev : ((finRotate (n + 3)).symm (Fin.last (n + 2))).val = n + 1 := by
1026       rw [coe_finRotate_symm_of_ne_zero]
1027       · simp
1028       · exact Fin.ne_of_val_ne (by simp)
1029     rw [finRotate_last, hprev]
1030     simp [hpred, hpred2]
1031     field_simp [hz0]
1032   · by_cases hzero : j = 0
1033     · subst j
1034       have hprev : (finRotate (n + 3)).symm (0 : Fin (n + 3)) =
1035           Fin.last (n + 2) := by
1036         apply (finRotate (n + 3)).injective
1037         simp
1038       rw [finRotate_apply_zero, hprev]
1039       simp [hpred, Nat.mod_eq_of_lt (by omega : 1 < n + 3)]
1040     · have hnext := coe_finRotate_of_ne_last hlast
1041       have hprev := coe_finRotate_symm_of_ne_zero hzero
1042       rw [hnext, hprev]
1043       have hjpos : 0 < j.val := by
1044         apply Nat.pos_of_ne_zero
1045         intro hj
1046         apply hzero
1047         exact Fin.ext hj
1048       have hj : j.val = (j.val - 1) + 1 := by omega
1049       have hj2 : j.val + 1 = (j.val - 1) + 2 := by omega
1050       have hp1 : z ^ (j.val + 1) = z ^ (j.val - 1) * z ^ 2 := by
1051         rw [hj2, pow_add]
1052       have hp0 : z ^ j.val = z ^ (j.val - 1) * z := by
1053         exact (congrArg (fun t : ℕ ↦ z ^ t) hj).trans (pow_succ z (j.val - 1))
1054       rw [hp1, hp0]
1055       field_simp [hz0]
1056 
1057 /-- A root-of-unity Fourier row is a left eigenvector of cycle adjacency. -/
1058 theorem cycleFourierRow_map_adjacency (n : ℕ) (z : k)
1059     (hroot : z ^ (n + 3) = 1) (x : Fin (n + 3) → k) :
1060     cycleFourierRow n z (cycleAdjacency n x) =
1061       (z + z⁻¹) * cycleFourierRow n z x := by
1062   have hmaps :
1063       (cycleFourierRow n z).comp (cycleAdjacency n) =
1064         (z + z⁻¹) • cycleFourierRow n z := by
1065     apply (Pi.basisFun k (Fin (n + 3))).ext
1066     intro j
1067     change cycleFourierRow n z
1068       (cycleAdjacency n (Pi.basisFun k (Fin (n + 3)) j)) =
1069         (z + z⁻¹) * cycleFourierRow n z (Pi.basisFun k (Fin (n + 3)) j)
1070     rw [cycleAdjacency_basisFun]
1071     simp only [map_add, cycleFourierRow_basisFun]
1072     exact cycle_root_neighbor_identity n z hroot j
1073   exact LinearMap.congr_fun hmaps x
1074 
1075 /-- The two Fourier rows form a two-dimensional scalar quotient of cycle adjacency. -/
1076 theorem cycleFourierFactor_map_adjacency (n : ℕ) (z : k)
1077     (hroot : z ^ (n + 3) = 1) (x : Fin (n + 3) → k) :
1078     cycleFourierFactor n z (cycleAdjacency n x) =
1079       (z + z⁻¹) • cycleFourierFactor n z x := by
1080   funext a
1081   fin_cases a
1082   · change cycleFourierRow n z (cycleAdjacency n x) =
1083       (z + z⁻¹) * cycleFourierRow n z x
1084     exact cycleFourierRow_map_adjacency n z hroot x
1085   · change cycleFourierRow n z⁻¹ (cycleAdjacency n x) =
1086       (z + z⁻¹) * cycleFourierRow n z⁻¹ x
1087     rw [cycleFourierRow_map_adjacency]
1088     · simp [add_comm]
1089     · simpa [inv_pow] using congrArg Inv.inv hroot
1090 
1091 /--
1092 For every field containing a non-real `N`th root of unity, the cycle on
1093 `N = n + 3` vertices has exact operator seed number two.
1094 -/
1095 theorem cycle_seedNumber_isLeast_two_of_root (n : ℕ) (z : k)
1096     (hroot : z ^ (n + 3) = 1) (hz : z ≠ z⁻¹) :
1097     IsLeast {r : ℕ | SeedNumberLE (cycleAdjacency (k := k) n) r} 2 := by
1098   constructor
1099   · exact ⟨cycleSeeds (k := k) n, cycleSeeds_generate (k := k) n⟩
1100   · intro r hr
1101     obtain ⟨v, hv⟩ := hr
1102     have hle := multiplicity_le_of_generates
1103       (cycleAdjacency (k := k) n) v 2 (cycleFourierFactor n z)
1104       (cycleFourierFactor_surjective n z hz) (z + z⁻¹)
1105       (eval_intertwining_of_map_T_eq_smul
1106         (cycleAdjacency (k := k) n) (cycleFourierFactor n z) (z + z⁻¹)
1107         (cycleFourierFactor_map_adjacency n z hroot)) hv
1108     simpa using hle
1109 
1110 /-- A primitive root of order at least three is distinct from its inverse. -/
1111 theorem primitiveRoot_ne_inv (n : ℕ) (z : k)
1112     (hprimitive : IsPrimitiveRoot z (n + 3)) : z ≠ z⁻¹ := by
1113   have hz0 : z ≠ 0 := (hprimitive.isUnit (by omega)).ne_zero
1114   have hpred : z ^ (n + 2) = z⁻¹ := by
1115     apply (mul_right_cancel₀ hz0)
1116     have hpow := pow_sub_one_mul (n := n + 3) (by omega) z
1117     simp only [show n + 3 - 1 = n + 2 by omega] at hpow
1118     rw [hpow, hprimitive.pow_eq_one]
1119     simp [hz0]
1120   intro h
1121   have hpowers : z ^ 1 = z ^ (n + 2) := by
1122     calc
1123       z ^ 1 = z := pow_one z
1124       _ = z⁻¹ := h
1125       _ = z ^ (n + 2) := hpred.symm
1126   have hexponents := hprimitive.pow_inj
1127     (i := 1) (j := n + 2) (by omega) (by omega) hpowers
1128   omega
1129 
1130 /-- The canonical complex primitive root used for the cycle spectrum. -/
1131 noncomputable def complexCycleRoot (n : ℕ) : ℂ :=
1132   Complex.exp (2 * Real.pi * Complex.I / (n + 3))
1133 
1134 /-- Every simple complex cycle `C_N`, `N ≥ 3`, has seed rank exactly two. -/
1135 theorem complex_cycle_seedNumber_isLeast_two (n : ℕ) :
1136     IsLeast {r : ℕ |
1137       SeedNumberLE (cycleAdjacency (k := ℂ) n) r} 2 := by
1138   have hprimitive : IsPrimitiveRoot (complexCycleRoot n) (n + 3) := by
1139     simpa [complexCycleRoot] using
1140       Complex.isPrimitiveRoot_exp (n + 3) (by omega)
1141   exact cycle_seedNumber_isLeast_two_of_root n (complexCycleRoot n)
1142     hprimitive.pow_eq_one (primitiveRoot_ne_inv n (complexCycleRoot n) hprimitive)
1143 
1144 end CycleGraph
1145 
1146 end Komorebi.SingleOperatorGraph
1147 
1148 #print axioms Komorebi.SingleOperatorGraph.singleOperator_seedNumber_isLeast_of_primary_decomposition
1149 #print axioms Komorebi.SingleOperatorGraph.restrictScalars_span_operatorAlgebra_eq_span_orbit
1150 #print axioms Komorebi.SingleOperatorGraph.operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast
1151 #print axioms Komorebi.SingleOperatorGraph.operatorAlgebra_seedRank_eq_of_seedNumber_isLeast
1152 #print axioms Komorebi.SingleOperatorGraph.singleOperator_operatorAlgebra_seedRanks_eq_of_primary_decomposition
1153 #print axioms Komorebi.SingleOperatorGraph.cyclic_matrix_criterion_of_primary_decomposition
1154 #print axioms Komorebi.SingleOperatorGraph.cyclic_matrix_four_way_iff_of_primary_decomposition
1155 #print axioms Komorebi.SingleOperatorGraph.graph_seedNumber_eq_max_eigenspace_multiplicity
1156 #print axioms Komorebi.SingleOperatorGraph.graph_seedNumber_eq_max_eigenspace_multiplicity_of_distinct
1157 #print axioms Komorebi.SingleOperatorGraph.path_endpoint_seedNumber_isLeast_one
1158 #print axioms Komorebi.SingleOperatorGraph.complex_cycle_seedNumber_isLeast_two

Back to source controls