ReleaseFiltered.lean

1 import KomorebiVerification.PaperII.WeightedTransfer
2 
3 /-!
4 # Complete filtered inversion at inverse-limit scope
5 
6 The quotient at depth `n` is the additive quotient by the relation
7 `x - y ∈ Fⁿ`.  Its transition maps are induced by the identity.  Thus the
8 `Complete` hypothesis below is exactly bijectivity of the canonical map to
9 compatible residue families, rather than an assumed Neumann-series result.
10 No norm, metrizability hypothesis or finite-dimensional hypothesis is used.
11 -/
12 
13 set_option autoImplicit false
14 
15 namespace Komorebi.PaperII.ReleaseFiltered
16 
17 open scoped BigOperators
18 open Komorebi.PaperII.WeightedTransfer
19 
20 universe u v
21 
22 /-- An exhaustive multiplicative ideal filtration. The two ideal actions follow
23 from multiplicativity and `all_mem`. -/
24 structure IdealFiltration (R : Type u) [Ring R] extends MultiplicativeFiltration R where
25   all_mem : ∀ x : R, Mem 0 x
26 
27 namespace IdealFiltration
28 
29 variable {R : Type u} [Ring R] (F : IdealFiltration R)
30 
31 theorem sub_mem {n : ℕ} {x y : R} (hx : F.Mem n x) (hy : F.Mem n y) :
32     F.Mem n (x - y) := by
33   simpa only [sub_eq_add_neg] using F.add_mem hx (F.neg_mem hy)
34 
35 theorem left_mem (x : R) {n : ℕ} {y : R} (hy : F.Mem n y) :
36     F.Mem n (x * y) := by
37   simpa only [Nat.zero_add] using F.mul_mem (F.all_mem x) hy
38 
39 theorem right_mem {n : ℕ} {x : R} (hx : F.Mem n x) (y : R) :
40     F.Mem n (x * y) := by
41   simpa only [Nat.add_zero] using F.mul_mem hx (F.all_mem y)
42 
43 /-- The usual residue equivalence modulo the filtration ideal. -/
44 def residueSetoid (n : ℕ) : Setoid R where
45   r x y := F.Mem n (x - y)
46   iseqv := ⟨by intro x; simpa using F.zero_mem n,
47     by intro x y h; simpa only [neg_sub] using F.neg_mem h,
48     by
49       intro x y z hxy hyz
50       have h := F.add_mem hxy hyz
51       simpa only [sub_add_sub_cancel] using h⟩
52 
53 /-- The residue set underlying the quotient ring `R/Fⁿ`. -/
54 def Residue (n : ℕ) := Quotient (F.residueSetoid n)
55 
56 def residue (n : ℕ) (x : R) : F.Residue n := Quotient.mk _ x
57 
58 theorem residue_eq_iff (n : ℕ) (x y : R) :
59     F.residue n x = F.residue n y ↔ F.Mem n (x - y) :=
60   by
61     constructor
62     · intro h
63       exact @Quotient.exact R (F.residueSetoid n) x y h
64     · intro h
65       exact @Quotient.sound R (F.residueSetoid n) x y h
66 
67 /-- Transition from a finer quotient to a coarser quotient. -/
68 def reduce {m n : ℕ} (h : m ≤ n) : F.Residue n → F.Residue m :=
69   Quotient.map id (by intro x y hxy; exact F.antitone h hxy)
70 
71 /-- Compatible residue families: the underlying set of the inverse limit. -/
72 def ResidueLimit :=
73   {x : ∀ n : ℕ, F.Residue n // ∀ m n (h : m ≤ n), F.reduce h (x n) = x m}
74 
75 /-- The canonical map from the ring to its inverse limit of residues. -/
76 def toResidueLimit (x : R) : F.ResidueLimit :=
77   ⟨fun n ↦ F.residue n x, by intro m n h; rfl⟩
78 
79 /-- Exact inverse-limit completeness and separation. -/
80 def Complete : Prop := Function.Bijective F.toResidueLimit
81 
82 /-- Injectivity of the canonical inverse-limit map is separation. -/
83 theorem separated (hF : F.Complete) {x : R} (hx : ∀ n, F.Mem n x) : x = 0 := by
84   apply hF.1
85   apply Subtype.ext
86   funext n
87   apply (F.residue_eq_iff n x 0).2
88   simpa only [sub_zero] using hx n
89 
90 /-- Every coherent sequence of representatives lifts to an element at all depths. -/
91 theorem lift_coherent (hF : F.Complete) (s : ℕ → R)
92     (hs : ∀ m n, m ≤ n → F.Mem m (s n - s m)) :
93     ∃ x : R, ∀ n, F.Mem n (x - s n) := by
94   let z : F.ResidueLimit := ⟨fun n ↦ F.residue n (s n), by
95     intro m n h
96     apply Quotient.sound
97     exact hs m n h⟩
98   obtain ⟨x, hx⟩ := hF.2 z
99   refine ⟨x, ?_⟩
100   intro n
101   apply (F.residue_eq_iff n x (s n)).1
102   exact congrFun (congrArg Subtype.val hx) n
103 
104 /-- Powers of a filtration-one element gain one degree at each multiplication. -/
105 theorem pow_mem {a : R} (ha : F.Mem 1 a) (n : ℕ) : F.Mem n (a ^ n) := by
106   induction n with
107   | zero => simpa only [pow_zero] using F.one_mem
108   | succ n ih =>
109       simpa only [pow_succ, Nat.succ_eq_add_one] using F.mul_mem ih ha
110 
111 /-- The finite geometric candidates form a coherent family of approximations. -/
112 theorem geometric_coherent {a : R} (ha : F.Mem 1 a) :
113     ∀ m n, m ≤ n →
114       F.Mem m (finiteGeometricInverse a n - finiteGeometricInverse a m) := by
115   intro m n hmn
116   obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
117   clear hmn
118   induction k with
119   | zero => simpa using F.zero_mem m
120   | succ k ih =>
121       have hp : F.Mem m ((-a) ^ (m + k)) :=
122         F.antitone (Nat.le_add_right m k) (F.pow_mem (F.neg_mem ha) (m + k))
123       have hs := F.add_mem ih hp
124       simpa only [finiteGeometricInverse, Nat.add_succ, Finset.sum_range_succ,
125         add_sub_right_comm] using hs
126 
127 /-- The two finite geometric residual identities, with no commutativity assumption. -/
128 theorem geometric_residual (a : R) (n : ℕ) :
129     finiteGeometricInverse a n * (1 + a) = 1 - (-a) ^ n ∧
130       (1 + a) * finiteGeometricInverse a n = 1 - (-a) ^ n := by
131   constructor
132   · simpa only [finiteGeometricInverse, sub_neg_eq_add] using geom_sum_mul_neg (-a) n
133   · simpa only [finiteGeometricInverse, sub_neg_eq_add] using mul_neg_geom_sum (-a) n
134 
135 /-- A filtration-convergent Neumann inverse in the full inverse-limit-complete ring.
136 The congruences are the definition of convergence for the filtration topology. -/
137 theorem exists_geometric_inverse (hF : F.Complete) {a : R} (ha : F.Mem 1 a) :
138     ∃ S : R, TwoSidedInverse (1 + a) S ∧
139       ∀ n, F.Mem n (S - finiteGeometricInverse a n) := by
140   obtain ⟨S, hS⟩ := F.lift_coherent hF (finiteGeometricInverse a) (F.geometric_coherent ha)
141   refine ⟨S, ⟨?_, ?_⟩, hS⟩
142   · apply sub_eq_zero.mp
143     apply F.separated hF
144     intro n
145     have hh := F.sub_mem (F.right_mem (hS n) (1 + a)) (F.pow_mem (F.neg_mem ha) n)
146     have he := (geometric_residual a n).1
147     have hid : (S - finiteGeometricInverse a n) * (1 + a) - (-a) ^ n =
148         S * (1 + a) - 1 := by
149       rw [sub_mul, he]
150       abel
151     simpa only [hid] using hh
152   · apply sub_eq_zero.mp
153     apply F.separated hF
154     intro n
155     have hh := F.sub_mem (F.left_mem (1 + a) (hS n)) (F.pow_mem (F.neg_mem ha) n)
156     have he := (geometric_residual a n).2
157     have hid : (1 + a) * (S - finiteGeometricInverse a n) - (-a) ^ n =
158         (1 + a) * S - 1 := by
159       rw [mul_sub, he]
160       abel
161     simpa only [hid] using hh
162 
163 
164 /-- Finite sums preserve a fixed filtration level. -/
165 theorem sum_mem {ι : Type v} (s : Finset ι) (f : ι → R) (n : ℕ)
166     (h : ∀ i ∈ s, F.Mem n (f i)) : F.Mem n (∑ i ∈ s, f i) := by
167   classical
168   induction s using Finset.induction_on with
169   | empty => simpa using F.zero_mem n
170   | @insert i s hi ih =>
171       rw [Finset.sum_insert hi]
172       exact F.add_mem (h i (Finset.mem_insert_self _ _))
173         (ih (by intro j hj; exact h j (Finset.mem_insert_of_mem hj)))
174 
175 /-- Termwise congruent finite sums are congruent. -/
176 theorem sum_sub_mem {ι : Type v} (s : Finset ι) (f g : ι → R) (n : ℕ)
177     (h : ∀ i ∈ s, F.Mem n (f i - g i)) :
178     F.Mem n ((∑ i ∈ s, f i) - ∑ i ∈ s, g i) := by
179   rw [← Finset.sum_sub_distrib]
180   exact F.sum_mem s (fun i ↦ f i - g i) n h
181 
182 /-- The raw length-`n` word sum differs from its weight-pruned sum only in
183 filtration depth `L`; this is a statement in the original ring. -/
184 theorem pow_sub_retained_mem {E : Type v} [Fintype E]
185     (weight : E → ℕ) (edge : E → R)
186     (hedge : ∀ e, F.Mem (weight e) (edge e)) (L n : ℕ) :
187     F.Mem L ((∑ e : E, edge e) ^ n - retainedFixedWordSum weight edge L n) := by
188   classical
189   rw [← sum_fixedWordProduct_eq_pow edge n]
190   simp only [retainedFixedWordSum, Finset.sum_filter]
191   apply F.sum_sub_mem
192   intro word _
193   by_cases hlow : wordWeight weight (List.ofFn word) < L
194   · simp only [hlow, ↓reduceIte, sub_self]
195     exact F.zero_mem L
196   · simp only [hlow, ↓reduceIte, sub_zero]
197     exact F.antitone (Nat.le_of_not_gt hlow)
198       (F.toMultiplicativeFiltration.wordProduct_mem weight edge hedge _)
199 
200 /-- Geometric truncation and weighted truncation are congruent in the ring. -/
201 theorem geometric_sub_pruned_mem {E : Type v} [Fintype E]
202     (weight : E → ℕ) (edge : E → R)
203     (hedge : ∀ e, F.Mem (weight e) (edge e)) (L N : ℕ) :
204     F.Mem L (finiteGeometricInverse (∑ e : E, edge e) N -
205       prunedWordInverse weight edge L N) := by
206   unfold finiteGeometricInverse prunedWordInverse
207   apply F.sum_sub_mem
208   intro n _
209   rw [neg_pow, ← mul_sub]
210   exact F.left_mem ((-1 : R) ^ n) (F.pow_sub_retained_mem weight edge hedge L n)
211 
212 
213 /-- Sequential convergence in the filtration topology. The ideals form a
214 countable neighborhood basis at zero. -/
215 def Converges (s : ℕ → R) (x : R) : Prop :=
216   ∀ L, ∃ N, ∀ n, N ≤ n → F.Mem L (x - s n)
217 
218 /-- Depth-indexed approximation congruences imply filtration convergence. -/
219 theorem converges_of_depth_congruences (s : ℕ → R) (x : R)
220     (h : ∀ n, F.Mem n (x - s n)) : F.Converges s x := by
221   intro L
222   refine ⟨L, ?_⟩
223   intro n hn
224   exact F.antitone hn (h n)
225 
226 /-- Filtration ideals are closed: a limit of elements in `Fᴸ` stays in `Fᴸ`. -/
227 theorem mem_of_converges (s : ℕ → R) (x : R) (hx : F.Converges s x)
228     (L : ℕ) (hs : ∀ n, F.Mem L (s n)) : F.Mem L x := by
229   obtain ⟨N, hN⟩ := hx L
230   have h := F.add_mem (hN N le_rfl) (hs N)
231   simpa only [sub_add_cancel] using h
232 
233 /-- Positive edge weights ensure that no retained word is omitted by the
234 standard length cutoff. Thus the finite candidate sums all words below depth. -/
235 theorem retained_length_lt {E : Type v} (weight : E → ℕ)
236     (hpositive : ∀ e, 1 ≤ weight e) (word : List E) (L : ℕ)
237     (hweight : wordWeight weight word < L) : word.length < L :=
238   lt_of_le_of_lt (length_le_wordWeight weight hpositive word) hweight
239 
240 /-- Inverse stability at every filtration depth, including depth zero. -/
241 theorem inverse_stability (T U Tinv Uinv : R)
242     (hT : TwoSidedInverse T Tinv) (hU : TwoSidedInverse U Uinv)
243     (L : ℕ) (h : F.Mem L (T - U)) : F.Mem L (Tinv - Uinv) := by
244   have he : Tinv - Uinv = Tinv * (U - T) * Uinv := by
245     rw [mul_sub, sub_mul]
246     simp only [mul_assoc, hU.right_inv, mul_one]
247     rw [← mul_assoc, hT.left_inv, one_mul]
248   rw [he]
249   exact F.right_mem (F.left_mem Tinv (by simpa only [neg_sub] using F.neg_mem h)) Uinv
250 
251 
252 /-- Every signed diagonal word has the declared filtration lower bound. -/
253 theorem signed_diagonal_word_mem {E : Type v} (weight : E → ℕ) (edge : E → R)
254     (hedge : ∀ e, F.Mem (weight e) (edge e)) (Dinv : R) (word : List E) :
255     F.Mem (wordWeight weight word)
256       (((-1 : R) ^ word.length * wordProduct edge word) * Dinv) := by
257   exact F.right_mem (F.left_mem _
258     (F.toMultiplicativeFiltration.wordProduct_mem weight edge hedge word)) Dinv
259 
260 /-- Reversing a word changes chronological versus written order but not weight. -/
261 theorem wordWeight_reverse {E : Type v} (weight : E → ℕ) (word : List E) :
262     wordWeight weight word.reverse = wordWeight weight word := by
263   simp only [wordWeight, List.map_reverse, List.sum_reverse]
264 
265 /-- A complete weighted normalized transfer has a two-sided inverse whose
266 error from the explicit finite word expression lies in the requested ideal. -/
267 theorem exists_weighted_inverse (hF : F.Complete)
268     {E : Type v} [Fintype E] (weight : E → ℕ) (edge : E → R)
269     (hpositive : ∀ e, 1 ≤ weight e)
270     (hedge : ∀ e, F.Mem (weight e) (edge e)) :
271     ∃ S : R, TwoSidedInverse (1 + ∑ e : E, edge e) S ∧
272       ∀ L, F.Mem L (S - prunedWordInverse weight edge L L) := by
273   have ha : F.Mem 1 (∑ e : E, edge e) := by
274     apply F.sum_mem
275     intro e _
276     exact F.antitone (hpositive e) (hedge e)
277   obtain ⟨S, hS, hcong⟩ := F.exists_geometric_inverse hF ha
278   refine ⟨S, hS, ?_⟩
279   intro L
280   have h := F.add_mem (hcong L) (F.geometric_sub_pruned_mem weight edge hedge L L)
281   simpa only [sub_add_sub_cancel] using h
282 
283 /-- Multiplying the normalized inverse by the supplied diagonal factor gives
284 both inverse equations without commutativity. -/
285 theorem diagonal_inverse (D Dinv H S : R) (hD : TwoSidedInverse D Dinv)
286     (hS : TwoSidedInverse (1 + Dinv * H) S) :
287     TwoSidedInverse (D + H) (S * Dinv) := by
288   constructor
289   · calc
290       (S * Dinv) * (D + H) = S * (Dinv * D + Dinv * H) := by
291         simp only [mul_add, mul_assoc]
292       _ = S * (1 + Dinv * H) := by rw [hD.left_inv]
293       _ = 1 := hS.left_inv
294   · have hfactor : D + H = D * (1 + Dinv * H) := by
295       rw [mul_add, mul_one, ← mul_assoc, hD.right_inv, one_mul]
296     rw [hfactor]
297     calc
298       (D * (1 + Dinv * H)) * (S * Dinv) =
299           D * (((1 + Dinv * H) * S) * Dinv) := by simp only [mul_assoc]
300       _ = 1 := by rw [hS.right_inv, one_mul, hD.right_inv]
301 
302 /-- Full weighted diagonal-plus-transfer inverse at manuscript scope. The
303 finite precision candidates have both residuals in `Fᴸ` in the original ring. -/
304 theorem exists_diagonal_weighted_inverse (hF : F.Complete)
305     (D Dinv H : R) (hD : TwoSidedInverse D Dinv)
306     {E : Type v} [Fintype E] (weight : E → ℕ) (edge : E → R)
307     (htransfer : Dinv * H = ∑ e : E, edge e)
308     (hpositive : ∀ e, 1 ≤ weight e)
309     (hedge : ∀ e, F.Mem (weight e) (edge e)) :
310     ∃ Tinv : R, TwoSidedInverse (D + H) Tinv ∧
311       ∀ L, let R_L := prunedDiagonalTransferInverse weight edge Dinv L L
312         F.Mem L (Tinv - R_L) ∧
313           F.Mem L ((D + H) * R_L - 1) ∧ F.Mem L (R_L * (D + H) - 1) := by
314   obtain ⟨S, hS, hcong⟩ := F.exists_weighted_inverse hF weight edge hpositive hedge
315   have hSn : TwoSidedInverse (1 + Dinv * H) S := by simpa only [htransfer] using hS
316   have hT := diagonal_inverse D Dinv H S hD hSn
317   refine ⟨S * Dinv, hT, ?_⟩
318   intro L
319   dsimp only
320   have hc : F.Mem L (S * Dinv - prunedDiagonalTransferInverse weight edge Dinv L L) := by
321     simpa only [prunedDiagonalTransferInverse, sub_mul] using F.right_mem (hcong L) Dinv
322   refine ⟨hc, ?_, ?_⟩
323   · have hh := F.neg_mem (F.left_mem (D + H) hc)
324     simpa only [mul_sub, hT.right_inv, neg_sub] using hh
325   · have hh := F.neg_mem (F.right_mem hc (D + H))
326     simpa only [sub_mul, hT.left_inv, neg_sub] using hh
327 
328 
329 /-- The depth-indexed word expansion converges to the full diagonal inverse. -/
330 theorem exists_diagonal_weighted_inverse_converges (hF : F.Complete)
331     (D Dinv H : R) (hD : TwoSidedInverse D Dinv)
332     {E : Type v} [Fintype E] (weight : E → ℕ) (edge : E → R)
333     (htransfer : Dinv * H = ∑ e : E, edge e)
334     (hpositive : ∀ e, 1 ≤ weight e)
335     (hedge : ∀ e, F.Mem (weight e) (edge e)) :
336     ∃ Tinv : R, TwoSidedInverse (D + H) Tinv ∧
337       F.Converges (fun L ↦ prunedDiagonalTransferInverse weight edge Dinv L L) Tinv := by
338   obtain ⟨Tinv, hT, hcong⟩ :=
339     F.exists_diagonal_weighted_inverse hF D Dinv H hD weight edge htransfer hpositive hedge
340   exact ⟨Tinv, hT, F.converges_of_depth_congruences _ _ (fun L ↦ (hcong L).1)⟩
341 
342 
343 /-- Direct manuscript wrapper: the raw transfers `N_e` are normalized by the
344 supplied inverse of `D`, and their filtration bounds are derived automatically. -/
345 theorem weighted_inverse_from_raw_edges (hF : F.Complete)
346     (D Dinv : R) (hD : TwoSidedInverse D Dinv)
347     {E : Type v} [Fintype E] (weight : E → ℕ) (transfer : E → R)
348     (hpositive : ∀ e, 1 ≤ weight e)
349     (htransfer : ∀ e, F.Mem (weight e) (transfer e)) :
350     ∃ Tinv : R, TwoSidedInverse (D + ∑ e : E, transfer e) Tinv ∧
351       (∀ L, let R_L :=
352         prunedDiagonalTransferInverse weight (fun e ↦ Dinv * transfer e) Dinv L L
353         F.Mem L (Tinv - R_L) ∧
354           F.Mem L ((D + ∑ e : E, transfer e) * R_L - 1) ∧
355           F.Mem L (R_L * (D + ∑ e : E, transfer e) - 1)) ∧
356       F.Converges (fun L ↦
357         prunedDiagonalTransferInverse weight (fun e ↦ Dinv * transfer e) Dinv L L) Tinv := by
358   obtain ⟨Tinv, hT, hcong⟩ := F.exists_diagonal_weighted_inverse hF D Dinv
359     (∑ e : E, transfer e) hD weight (fun e ↦ Dinv * transfer e)
360     (Finset.mul_sum _ _ _) hpositive (fun e ↦ F.left_mem Dinv (htransfer e))
361   exact ⟨Tinv, hT, hcong,
362     F.converges_of_depth_congruences _ _ (fun L ↦ (hcong L).1)⟩
363 
364 end IdealFiltration
365 end Komorebi.PaperII.ReleaseFiltered

Back to source controls