ReleaseFilteredPaths.lean

1 import KomorebiVerification.PaperII.ReleaseFiltered
2 import Mathlib.Data.Fintype.Card
3 
4 /-! # Packet-supported word and path expansions
5 
6 Words here use written multiplication order. `IsPath s t word` reads that
7 word from right to left, so it describes the directed path from `s` to `t`
8 whose chronological edge list is `word.reverse`. This is precisely the
9 reversal convention stated in the manuscript.
10 -/
11 
12 set_option autoImplicit false
13 
14 namespace Komorebi.PaperII.ReleaseFilteredPaths
15 
16 open scoped BigOperators
17 open Komorebi.PaperII.WeightedTransfer
18 open Komorebi.PaperII.ReleaseFiltered
19 
20 universe u v w
21 
22 /-- Finite packet idempotents and supported normalized transfer edges. -/
23 structure PacketTransfer (R : Type u) [Ring R] (V : Type v) (E : Type w)
24     [Fintype V] [DecidableEq V] where
25   packet : V → R
26   packet_mul : ∀ i j, packet i * packet j = if i = j then packet i else 0
27   packet_sum : ∑ i, packet i = 1
28   source : E → V
29   target : E → V
30   edge : E → R
31   left_support : ∀ e, packet (target e) * edge e = edge e
32   right_support : ∀ e, edge e * packet (source e) = edge e
33 
34 namespace PacketTransfer
35 
36 variable {R : Type u} [Ring R] {V : Type v} {E : Type w}
37   [Fintype V] [DecidableEq V] (G : PacketTransfer R V E)
38 
39 
40 /-- The manuscript's single sandwich support equation constructs the two
41 support identities used by the path proofs. -/
42 def ofSandwich (packet : V → R)
43     (hpacket : ∀ i j, packet i * packet j = if i = j then packet i else 0)
44     (hsum : ∑ i, packet i = 1) (source target : E → V) (edge : E → R)
45     (hedge : ∀ e, edge e = packet (target e) * edge e * packet (source e)) :
46     PacketTransfer R V E where
47   packet := packet
48   packet_mul := hpacket
49   packet_sum := hsum
50   source := source
51   target := target
52   edge := edge
53   left_support e := by
54     calc
55       packet (target e) * edge e =
56           packet (target e) * (packet (target e) * edge e * packet (source e)) :=
57         congrArg (packet (target e) * ·) (hedge e)
58       _ = packet (target e) * edge e * packet (source e) := by
59         simp only [← mul_assoc, hpacket, ↓reduceIte]
60       _ = edge e := (hedge e).symm
61   right_support e := by
62     calc
63       edge e * packet (source e) =
64           (packet (target e) * edge e * packet (source e)) * packet (source e) :=
65         congrArg (· * packet (source e)) (hedge e)
66       _ = packet (target e) * edge e * packet (source e) := by
67         simp only [mul_assoc, hpacket, ↓reduceIte]
68       _ = edge e := (hedge e).symm
69 
70 /-- Endpoint compatibility in written multiplication order. -/
71 def IsPath (G : PacketTransfer R V E) (s t : V) : List E → Prop
72   | [] => s = t
73   | e :: es => G.target e = t ∧ G.IsPath s (G.source e) es
74 
75 instance instDecidableIsPath (s t : V) (es : List E) : Decidable (G.IsPath s t es) := by
76   induction es generalizing t with
77   | nil => change Decidable (s = t); infer_instance
78   | cons e es ih =>
79       change Decidable (G.target e = t ∧ G.IsPath s (G.source e) es)
80       exact instDecidableAnd
81 
82 
83 /-- Directed paths in chronological order, with the first edge traversed first. -/
84 def ChronologicalPath (G : PacketTransfer R V E) (s t : V) : List E → Prop
85   | [] => s = t
86   | e :: es => G.source e = s ∧ G.ChronologicalPath (G.target e) t es
87 
88 theorem isPath_append_last (s t : V) (word : List E) (e : E) :
89     G.IsPath s t (word ++ [e]) ↔ G.source e = s ∧ G.IsPath (G.target e) t word := by
90   induction word generalizing t with
91   | nil =>
92       change (G.target e = t ∧ s = G.source e) ↔ (G.source e = s ∧ G.target e = t)
93       constructor
94       · rintro ⟨h₁, h₂⟩; exact ⟨h₂.symm, h₁⟩
95       · rintro ⟨h₁, h₂⟩; exact ⟨h₂, h₁.symm⟩
96   | cons f fs ih =>
97       change (G.target f = t ∧ G.IsPath s (G.source f) (fs ++ [e])) ↔
98         (G.source e = s ∧ (G.target f = t ∧ G.IsPath (G.target e) (G.source f) fs))
99       rw [ih]
100       exact and_left_comm
101 
102 /-- Reversal relates the formal written-word convention to the manuscript's
103 chronological directed paths, including the empty path. -/
104 theorem isPath_reverse_iff (s t : V) (word : List E) :
105     G.IsPath s t word.reverse ↔ G.ChronologicalPath s t word := by
106   induction word generalizing s with
107   | nil => rfl
108   | cons e es ih =>
109       rw [List.reverse_cons, G.isPath_append_last]
110       change (G.source e = s ∧ G.IsPath (G.target e) t es.reverse) ↔
111         (G.source e = s ∧ G.ChronologicalPath (G.target e) t es)
112       exact and_congr Iff.rfl (ih (G.target e))
113 
114 theorem packet_mul_edge (t : V) (e : E) :
115     G.packet t * G.edge e = if G.target e = t then G.edge e else 0 := by
116   rw [← G.left_support e, ← mul_assoc, G.packet_mul]
117   by_cases h : G.target e = t
118   · subst t
119     simp only [↓reduceIte, G.left_support]
120   · have ht : t ≠ G.target e := Ne.symm h
121     simp only [ht, h, ↓reduceIte, zero_mul]
122 
123 /-- Every incompatible word vanishes in the sandwiched block, while a compatible
124 word retains the chronological path product (and the source projection). -/
125 theorem block_word_eq (s t : V) (word : List E) :
126     G.packet t * wordProduct G.edge word * G.packet s =
127       if G.IsPath s t word then wordProduct G.edge word * G.packet s else 0 := by
128   induction word generalizing t with
129   | nil =>
130       simp only [wordProduct_nil, mul_one, one_mul, IsPath, G.packet_mul]
131       by_cases h : s = t
132       · subst t; simp
133       · simp [h, Ne.symm h]
134   | cons e es ih =>
135       rw [wordProduct_cons, ← mul_assoc (G.packet t), G.packet_mul_edge]
136       by_cases ht : G.target e = t
137       · simp only [ht, ↓reduceIte]
138         have hid : G.edge e * wordProduct G.edge es * G.packet s =
139             G.edge e * (G.packet (G.source e) * wordProduct G.edge es * G.packet s) := by
140           simp only [← mul_assoc, G.right_support]
141         rw [hid, ih]
142         by_cases hp : G.IsPath s (G.source e) es
143         · simp only [hp, ↓reduceIte, IsPath, ht, and_self]
144         · simp only [hp, ↓reduceIte, IsPath, ht, and_false, mul_zero]
145       · simp only [ht, ↓reduceIte, zero_mul, IsPath, false_and]
146 
147 /-- The signed finite path sum at a fixed weight and length cutoff. -/
148 def pathInverse [Fintype E] (weight : E → ℕ) (s t : V) (L N : ℕ) : R :=
149   ∑ n ∈ Finset.range N, (-1 : R) ^ n *
150     ∑ word : Fin n → E with
151       wordWeight weight (List.ofFn word) < L ∧ G.IsPath s t (List.ofFn word),
152       wordProduct G.edge (List.ofFn word) * G.packet s
153 
154 /-- Filtering the explicit finite inverse by endpoints is exactly taking its
155 packet block; the assertion is algebraic and needs no completeness. -/
156 theorem block_pruned_eq_pathInverse [Fintype E]
157     (weight : E → ℕ) (s t : V) (L N : ℕ) :
158     G.packet t * prunedWordInverse weight G.edge L N * G.packet s =
159       G.pathInverse weight s t L N := by
160   classical
161   simp only [prunedWordInverse, pathInverse, Finset.mul_sum, Finset.sum_mul]
162   apply Finset.sum_congr rfl
163   intro n _
164   have hcentral : G.packet t * (-1 : R) ^ n = (-1 : R) ^ n * G.packet t := by
165     exact (Commute.neg_one_right (G.packet t)).pow_right n
166   rw [← mul_assoc, hcentral, mul_assoc, mul_assoc]
167   simp only [retainedFixedWordSum, Finset.sum_filter, Finset.mul_sum, Finset.sum_mul]
168   apply Finset.sum_congr rfl
169   intro word _
170   by_cases hw : wordWeight weight (List.ofFn word) < L
171   · simp only [hw, ↓reduceIte, true_and]
172     simpa only [mul_assoc, mul_ite, mul_zero] using
173       congrArg (fun x : R ↦ (-1 : R) ^ n * x)
174         (G.block_word_eq s t (List.ofFn word))
175   · simp only [hw, ↓reduceIte, false_and, mul_zero, zero_mul]
176 
177 /-- Completed packet block formula: at every depth it is exactly the finite
178 sum over compatible retained paths modulo that depth. -/
179 theorem complete_block_path_formula [Fintype E]
180     (F : IdealFiltration R) (hF : F.Complete)
181     (weight : E → ℕ) (hpositive : ∀ e, 1 ≤ weight e)
182     (hedge : ∀ e, F.Mem (weight e) (G.edge e)) :
183     ∃ S : R, TwoSidedInverse (1 + ∑ e : E, G.edge e) S ∧
184       ∀ s t L, F.Mem L
185         (G.packet t * S * G.packet s - G.pathInverse weight s t L L) := by
186   obtain ⟨S, hS, hcong⟩ := F.exists_weighted_inverse hF weight G.edge hpositive hedge
187   refine ⟨S, hS, ?_⟩
188   intro s t L
189   have h := F.right_mem (F.left_mem (G.packet t) (hcong L)) (G.packet s)
190   simpa only [mul_sub, sub_mul, G.block_pruned_eq_pathInverse] using h
191 
192 /-- If every valid path has weight at least `d`, every retained block candidate
193 has that same lower filtration bound. -/
194 theorem pathInverse_mem [Fintype E]
195     (F : IdealFiltration R) (weight : E → ℕ)
196     (hedge : ∀ e, F.Mem (weight e) (G.edge e)) (s t : V) (d L N : ℕ)
197     (hmin : ∀ word : List E, G.IsPath s t word → d ≤ wordWeight weight word) :
198     F.Mem d (G.pathInverse weight s t L N) := by
199   classical
200   unfold pathInverse
201   apply F.sum_mem
202   intro n _
203   apply F.left_mem
204   apply F.sum_mem
205   intro word hw
206   have hpath := (Finset.mem_filter.mp hw).2.2
207   apply F.right_mem
208   exact F.antitone (hmin _ hpath)
209     (F.toMultiplicativeFiltration.wordProduct_mem weight G.edge hedge _)
210 
211 /-- The minimum-path filtration bound follows by reducing the completed
212 formula at that depth. -/
213 theorem minimum_path_weight [Fintype E]
214     (F : IdealFiltration R) (weight : E → ℕ)
215     (hedge : ∀ e, F.Mem (weight e) (G.edge e)) (S : R)
216     (hcong : ∀ s t L, F.Mem L
217       (G.packet t * S * G.packet s - G.pathInverse weight s t L L))
218     (s t : V) (d : ℕ)
219     (hmin : ∀ word : List E, G.IsPath s t word → d ≤ wordWeight weight word) :
220     F.Mem d (G.packet t * S * G.packet s) := by
221   have h := F.add_mem (hcong s t d) (G.pathInverse_mem F weight hedge s t d d d hmin)
222   simpa only [sub_add_cancel] using h
223 
224 /-- No directed path means the completed block is zero. -/
225 theorem no_path_block_zero [Fintype E]
226     (F : IdealFiltration R) (hF : F.Complete) (weight : E → ℕ)
227     (hedge : ∀ e, F.Mem (weight e) (G.edge e)) (S : R)
228     (hcong : ∀ s t L, F.Mem L
229       (G.packet t * S * G.packet s - G.pathInverse weight s t L L))
230     (s t : V) (hno : ∀ word : List E, ¬ G.IsPath s t word) :
231     G.packet t * S * G.packet s = 0 := by
232   apply F.separated hF
233   intro d
234   exact G.minimum_path_weight F weight hedge S hcong s t d
235     (by intro word hp; exact False.elim (hno word hp))
236 
237 
238 
239 /-- The vertices encountered from target back to source in written order. -/
240 def vertices (G : PacketTransfer R V E) (t : V) : List E → List V
241   | [] => [t]
242   | e :: es => t :: G.vertices (G.source e) es
243 
244 @[simp] theorem vertices_length (t : V) (word : List E) :
245     (G.vertices t word).length = word.length + 1 := by
246   induction word generalizing t with
247   | nil => rfl
248   | cons e es ih => simp only [vertices, List.length_cons, ih]
249 
250 /-- A visited vertex splits a path into two valid subpaths. -/
251 theorem path_cut_of_vertex_mem (s t v : V) (word : List E)
252     (hp : G.IsPath s t word) (hv : v ∈ G.vertices t word) :
253     ∃ front back : List E, word = front ++ back ∧
254       G.IsPath v t front ∧ G.IsPath s v back := by
255   induction word generalizing t with
256   | nil =>
257       have hvt : v = t := by simpa only [vertices, List.mem_singleton] using hv
258       subst v
259       exact ⟨[], [], rfl, rfl, hp⟩
260   | cons e es ih =>
261       rcases hp with ⟨ht, htail⟩
262       rcases List.mem_cons.mp hv with hvt | hv
263       · subst v
264         exact ⟨[], e :: es, rfl, rfl, ⟨ht, htail⟩⟩
265       · obtain ⟨front, back, heq, hfront, hback⟩ := ih (G.source e) htail hv
266         refine ⟨e :: front, back, ?_, ⟨ht, hfront⟩, hback⟩
267         simp only [List.cons_append, heq]
268 
269 /-- Acyclicity excludes every nonempty closed directed path. -/
270 def Acyclic : Prop := ∀ v (word : List E), word ≠ [] → ¬ G.IsPath v v word
271 
272 /-- An acyclic path cannot repeat a vertex. -/
273 theorem vertices_nodup (hacyc : G.Acyclic) (s t : V) (word : List E)
274     (hp : G.IsPath s t word) : (G.vertices t word).Nodup := by
275   induction word generalizing t with
276   | nil => simp [vertices]
277   | cons e es ih =>
278       rcases hp with ⟨ht, htail⟩
279       apply List.nodup_cons.mpr
280       constructor
281       · intro hv
282         obtain ⟨front, back, _, hfront, _⟩ :=
283           G.path_cut_of_vertex_mem s (G.source e) t es htail hv
284         exact hacyc t (e :: front) (by simp) ⟨ht, hfront⟩
285       · exact ih (G.source e) htail
286 
287 /-- The number of edges of a path in a finite acyclic graph is strictly less
288 than the number of vertices. -/
289 theorem path_length_lt_card (hacyc : G.Acyclic) (s t : V) (word : List E)
290     (hp : G.IsPath s t word) : word.length < Fintype.card V := by
291   have h := (G.vertices_nodup hacyc s t word hp).length_le_card
292   rw [G.vertices_length] at h
293   exact Nat.lt_of_succ_le h
294 
295 /-- If every packet block is zero, the operator itself is zero. -/
296 theorem eq_zero_of_blocks (x : R) (h : ∀ s t, G.packet t * x * G.packet s = 0) : x = 0 := by
297   have hl (t : V) : G.packet t * x = 0 := by
298     calc
299       G.packet t * x = (G.packet t * x) * (∑ s, G.packet s) := by rw [G.packet_sum, mul_one]
300       _ = ∑ s, G.packet t * x * G.packet s := Finset.mul_sum _ _ _
301       _ = 0 := by simp only [h, Finset.sum_const_zero]
302   calc
303     x = (∑ t, G.packet t) * x := by rw [G.packet_sum, one_mul]
304     _ = ∑ t, G.packet t * x := Finset.sum_mul _ _ _
305     _ = 0 := by simp only [hl, Finset.sum_const_zero]
306 
307 /-- Acyclic supported transfer is nilpotent over any ring. Neither positive
308 weights nor a complete filtration is required for this conclusion. -/
309 theorem acyclic_nilpotent [Fintype E] (hacyc : G.Acyclic) :
310     (∑ e : E, G.edge e) ^ Fintype.card V = 0 := by
311   apply G.eq_zero_of_blocks
312   intro s t
313   rw [← sum_fixedWordProduct_eq_pow]
314   simp only [Finset.mul_sum, Finset.sum_mul]
315   apply Finset.sum_eq_zero
316   intro word _
317   rw [G.block_word_eq]
318   have hno : ¬ G.IsPath s t (List.ofFn word) := by
319     intro hp
320     have h := G.path_length_lt_card hacyc s t (List.ofFn word) hp
321     simp only [List.length_ofFn, lt_self_iff_false] at h
322   simp only [hno, ↓reduceIte]
323 
324 /-- The inverse in an acyclic graph is a finite sum in the original ring. -/
325 theorem acyclic_finite_inverse [Fintype E] (hacyc : G.Acyclic) :
326     TwoSidedInverse (1 + ∑ e : E, G.edge e)
327       (finiteGeometricInverse (∑ e : E, G.edge e) (Fintype.card V)) :=
328   finiteGeometricInverse_spec_of_pow_eq_zero _ _ (G.acyclic_nilpotent hacyc)
329 
330 /-- Packet diagonality expressed by commutation with every packet. -/
331 def IsDiagonal (D : R) : Prop := ∀ i, G.packet i * D = D * G.packet i
332 
333 /-- An inverse of a packet-diagonal unit is packet diagonal. -/
334 theorem inverse_diagonal (D Dinv : R) (hD : TwoSidedInverse D Dinv)
335     (hdiag : G.IsDiagonal D) : G.IsDiagonal Dinv := by
336   intro i
337   calc
338     G.packet i * Dinv = (Dinv * D) * (G.packet i * Dinv) := by rw [hD.left_inv, one_mul]
339     _ = Dinv * (D * G.packet i) * Dinv := by simp only [mul_assoc]
340     _ = Dinv * (G.packet i * D) * Dinv := by rw [← hdiag i]
341     _ = Dinv * G.packet i := by simp only [mul_assoc, hD.right_inv, mul_one]
342 
343 /-- Normalizing a supported transfer by a packet-diagonal inverse preserves
344 its two endpoints. -/
345 def normalized (Dinv : R) (hdiag : G.IsDiagonal Dinv) : PacketTransfer R V E where
346   packet := G.packet
347   packet_mul := G.packet_mul
348   packet_sum := G.packet_sum
349   source := G.source
350   target := G.target
351   edge := fun e ↦ Dinv * G.edge e
352   left_support e := by
353     rw [← mul_assoc, hdiag, mul_assoc, G.left_support]
354   right_support e := by
355     rw [mul_assoc, G.right_support]
356 
357 
358 @[simp] theorem normalized_isPath_iff (Dinv : R) (hdiag : G.IsDiagonal Dinv)
359     (s t : V) (word : List E) :
360     (G.normalized Dinv hdiag).IsPath s t word ↔ G.IsPath s t word := by
361   induction word generalizing t with
362   | nil => rfl
363   | cons e es ih =>
364       change (G.target e = t ∧ (G.normalized Dinv hdiag).IsPath s (G.source e) es) ↔
365         (G.target e = t ∧ G.IsPath s (G.source e) es)
366       exact and_congr Iff.rfl (ih (G.source e))
367 
368 
369 /-- A left-supported corner family is recovered by the corresponding packet
370 projection after assembly. -/
371 theorem left_corner_of_sum (dinv : V → R)
372     (hsupport : ∀ i, G.packet i * dinv i = dinv i) (s : V) :
373     G.packet s * (∑ i, dinv i) = dinv s := by
374   rw [Finset.mul_sum]
375   have he (i : V) : G.packet s * dinv i = if s = i then dinv i else 0 := by
376     calc
377       G.packet s * dinv i = (G.packet s * G.packet i) * dinv i := by
378         rw [mul_assoc, hsupport]
379       _ = if s = i then dinv i else 0 := by
380         rw [G.packet_mul]
381         by_cases h : s = i
382         · subst i; simp only [↓reduceIte, hsupport]
383         · simp only [h, ↓reduceIte, zero_mul]
384   simp only [he]
385   simp
386 
387 /-- The analogous right projection recovers a right-supported corner family. -/
388 theorem right_corner_of_sum (dinv : V → R)
389     (hsupport : ∀ i, dinv i * G.packet i = dinv i) (s : V) :
390     (∑ i, dinv i) * G.packet s = dinv s := by
391   rw [Finset.sum_mul]
392   have he (i : V) : dinv i * G.packet s = if i = s then dinv i else 0 := by
393     calc
394       dinv i * G.packet s = dinv i * (G.packet i * G.packet s) := by
395         rw [← mul_assoc, hsupport]
396       _ = if i = s then dinv i else 0 := by
397         rw [G.packet_mul]
398         by_cases h : i = s
399         · simp only [h, ↓reduceIte, hsupport]
400         · simp only [h, ↓reduceIte, mul_zero]
401   simp only [he]
402   simp
403 
404 /-- Global normalization is literally the local target-corner normalization
405 in the manuscript's path factors. -/
406 theorem normalized_edge_eq_target_corner (dinv : V → R)
407     (hsupport : ∀ i, dinv i * G.packet i = dinv i) (e : E) :
408     (∑ i, dinv i) * G.edge e = dinv (G.target e) * G.edge e := by
409   calc
410     (∑ i, dinv i) * G.edge e =
411         ((∑ i, dinv i) * G.packet (G.target e)) * G.edge e := by
412       rw [mul_assoc, G.left_support]
413     _ = dinv (G.target e) * G.edge e := by rw [G.right_corner_of_sum dinv hsupport]
414 
415 /-- Local two-sided corner inverses, extended by zero, assemble into the
416 supplied global diagonal inverse used by the main theorem. -/
417 theorem assembled_corner_inverse (D : R) (hdiag : G.IsDiagonal D) (dinv : V → R)
418     (hleftSupport : ∀ i, G.packet i * dinv i = dinv i)
419     (hrightSupport : ∀ i, dinv i * G.packet i = dinv i)
420     (hleft : ∀ i, dinv i * (G.packet i * D * G.packet i) = G.packet i)
421     (hright : ∀ i, (G.packet i * D * G.packet i) * dinv i = G.packet i) :
422     TwoSidedInverse D (∑ i, dinv i) := by
423   have hl (i : V) : dinv i * D = G.packet i := by
424     have he : dinv i * (G.packet i * D * G.packet i) = dinv i * D := by
425       calc
426         dinv i * (G.packet i * D * G.packet i) =
427             (dinv i * G.packet i) * (D * G.packet i) := by simp only [mul_assoc]
428         _ = dinv i * (G.packet i * D) := by rw [hrightSupport, ← hdiag i]
429         _ = dinv i * D := by rw [← mul_assoc, hrightSupport]
430     exact he.symm.trans (hleft i)
431   have hr (i : V) : D * dinv i = G.packet i := by
432     have he : (G.packet i * D * G.packet i) * dinv i = D * dinv i := by
433       calc
434         (G.packet i * D * G.packet i) * dinv i =
435             (G.packet i * D) * (G.packet i * dinv i) := by simp only [mul_assoc]
436         _ = (D * G.packet i) * dinv i := by rw [hleftSupport, hdiag i]
437         _ = D * dinv i := by rw [mul_assoc, hleftSupport]
438     exact he.symm.trans (hright i)
439   constructor
440   · rw [Finset.sum_mul]
441     simp only [hl, G.packet_sum]
442   · rw [Finset.mul_sum]
443     simp only [hr, G.packet_sum]
444 
445 /-- The packet-diagonal formula in the manuscript implies commutation. -/
446 theorem diagonal_of_block_sum (D : R)
447     (hD : D = ∑ i, G.packet i * D * G.packet i) : G.IsDiagonal D := by
448   intro j
449   have hl : G.packet j * D = G.packet j * D * G.packet j := by
450     conv_lhs => rw [hD]
451     rw [Finset.mul_sum]
452     simp only [← mul_assoc, G.packet_mul]
453     simp
454   have hr : D * G.packet j = G.packet j * D * G.packet j := by
455     conv_lhs => rw [hD]
456     rw [Finset.sum_mul]
457     simp only [mul_assoc, G.packet_mul]
458     simp
459   exact hl.trans hr.symm
460 
461 /-- The full diagonal-plus-transfer packet path formula at every precision.
462 The candidate includes the source corner of `Dinv` at its right endpoint. -/
463 theorem complete_diagonal_block_path_formula [Fintype E]
464     (F : IdealFiltration R) (hF : F.Complete)
465     (D Dinv : R) (hD : TwoSidedInverse D Dinv) (hdiag : G.IsDiagonal D)
466     (weight : E → ℕ) (hpositive : ∀ e, 1 ≤ weight e)
467     (hedge : ∀ e, F.Mem (weight e) (G.edge e)) :
468     let Gnorm := G.normalized Dinv (G.inverse_diagonal D Dinv hD hdiag)
469     ∃ Tinv : R, TwoSidedInverse (D + ∑ e : E, G.edge e) Tinv ∧
470       ∀ s t L, F.Mem L (G.packet t * Tinv * G.packet s -
471         Gnorm.pathInverse weight s t L L * Dinv) := by
472   dsimp only
473   let Gnorm := G.normalized Dinv (G.inverse_diagonal D Dinv hD hdiag)
474   have hnorm : ∀ e, F.Mem (weight e) (Gnorm.edge e) :=
475     fun e ↦ F.left_mem Dinv (hedge e)
476   obtain ⟨S, hS, hcong⟩ := Gnorm.complete_block_path_formula F hF weight hpositive hnorm
477   have hsum : Dinv * (∑ e : E, G.edge e) = ∑ e : E, Gnorm.edge e := by
478     simp only [Gnorm, normalized, Finset.mul_sum]
479   have hSn : TwoSidedInverse (1 + Dinv * ∑ e : E, G.edge e) S := by
480     simpa only [hsum] using hS
481   refine ⟨S * Dinv, IdealFiltration.diagonal_inverse D Dinv _ S hD hSn, ?_⟩
482   intro s t L
483   have h := F.right_mem (hcong s t L) Dinv
484   have hd : Dinv * G.packet s = G.packet s * Dinv :=
485     (G.inverse_diagonal D Dinv hD hdiag s).symm
486   have he : G.packet t * (S * Dinv) * G.packet s =
487       (G.packet t * S * G.packet s) * Dinv := by
488     simp only [mul_assoc, hd]
489   rw [he]
490   simpa only [sub_mul, Gnorm, normalized] using h
491 
492 
493 /-- The minimum weight lower bound for the full diagonal-plus-transfer inverse. -/
494 theorem diagonal_minimum_path_weight [Fintype E]
495     (F : IdealFiltration R) (Dinv : R) (hdiag : G.IsDiagonal Dinv)
496     (weight : E → ℕ) (hedge : ∀ e, F.Mem (weight e) (G.edge e))
497     (Tinv : R)
498     (hcong : ∀ s t L, F.Mem L (G.packet t * Tinv * G.packet s -
499       (G.normalized Dinv hdiag).pathInverse weight s t L L * Dinv))
500     (s t : V) (d : ℕ)
501     (hmin : ∀ word : List E, G.IsPath s t word → d ≤ wordWeight weight word) :
502     F.Mem d (G.packet t * Tinv * G.packet s) := by
503   have hterm := (G.normalized Dinv hdiag).pathInverse_mem F weight
504     (fun e ↦ F.left_mem Dinv (hedge e)) s t d d d
505     (by intro word hp; exact hmin word ((G.normalized_isPath_iff Dinv hdiag s t word).mp hp))
506   have h := F.add_mem (hcong s t d) (F.right_mem hterm Dinv)
507   simpa only [sub_add_cancel] using h
508 
509 /-- Absence of a path forces the full inverse block to vanish. -/
510 theorem diagonal_no_path_block_zero [Fintype E]
511     (F : IdealFiltration R) (hF : F.Complete) (Dinv : R) (hdiag : G.IsDiagonal Dinv)
512     (weight : E → ℕ) (hedge : ∀ e, F.Mem (weight e) (G.edge e))
513     (Tinv : R)
514     (hcong : ∀ s t L, F.Mem L (G.packet t * Tinv * G.packet s -
515       (G.normalized Dinv hdiag).pathInverse weight s t L L * Dinv))
516     (s t : V) (hno : ∀ word : List E, ¬ G.IsPath s t word) :
517     G.packet t * Tinv * G.packet s = 0 := by
518   apply F.separated hF
519   intro d
520   exact G.diagonal_minimum_path_weight F Dinv hdiag weight hedge Tinv hcong s t d
521     (by intro word hp; exact False.elim (hno word hp))
522 
523 /-- The full diagonal-plus-transfer inverse is finite for an acyclic graph,
524 with no filtered-algebra or completeness hypothesis. -/
525 theorem acyclic_diagonal_inverse [Fintype E]
526     (D Dinv : R) (hD : TwoSidedInverse D Dinv) (hdiag : G.IsDiagonal D)
527     (hacyc : G.Acyclic) :
528     TwoSidedInverse (D + ∑ e : E, G.edge e)
529       (diagonalTransferInverse Dinv (∑ e : E, G.edge e) (Fintype.card V)) := by
530   let Gnorm := G.normalized Dinv (G.inverse_diagonal D Dinv hD hdiag)
531   have hnacyc : Gnorm.Acyclic := by
532     intro v word hword hp
533     exact hacyc v word hword
534       ((G.normalized_isPath_iff Dinv (G.inverse_diagonal D Dinv hD hdiag) v v word).mp hp)
535   apply diagonalTransferInverse_spec _ _ _ _ hD
536   have hnil := Gnorm.acyclic_nilpotent hnacyc
537   simpa only [Gnorm, normalized, Finset.mul_sum] using hnil
538 
539 end PacketTransfer
540 end Komorebi.PaperII.ReleaseFilteredPaths

Back to source controls