WeightedTransfer.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Analysis.SpecificLimits.Normed
7 import Mathlib.Algebra.Order.Floor.Div
8 import Mathlib.Data.Fintype.BigOperators
9 import Mathlib.Data.List.OfFn
10 
11 /-!
12 # Paper II: weighted transfer and finite-precision inversion
13 
14 Author: Komorebi P.
15 
16 This module isolates the algebraic content of weighted transfer inversion.  It proves a finite
17 noncommutative geometric-inverse identity, transports that identity through quotient maps, expands
18 powers as finite sums of ordered words, and packages multiplicative-filtration certificates which
19 justify pruning every word whose cumulative weight reaches the requested precision.
20 
21 Positive edge weights turn a precision cutoff into an explicit nilpotence certificate in the
22 quotient, so the resulting inverse is a finite sum.  A separate analytic specialization proves the
23 usual infinite geometric formula in a complete normed ring under the explicit hypothesis
24 `‖Dinv * K‖ < 1`.
25 
26 There is deliberately no theorem asserting unrestricted adic convergence: filtered results below
27 are exact statements at a fixed finite precision, while the sole convergent infinite series uses a
28 norm strictly smaller than one.
29 -/
30 
31 set_option autoImplicit false
32 
33 namespace Komorebi.PaperII.WeightedTransfer
34 
35 open scoped BigOperators
36 
37 universe u v w
38 
39 /-! ## Finite noncommutative geometric inversion -/
40 
41 /-- `y` is simultaneously a left and right inverse of `x`.
42 
43 Keeping both equations in the certificate is important in the noncommutative setting.
44 -/
45 structure TwoSidedInverse {R : Type u} [Mul R] [One R] (x y : R) : Prop where
46   left_inv : y * x = 1
47   right_inv : x * y = 1
48 
49 namespace TwoSidedInverse
50 
51 /-- A ring homomorphism transports a two-sided inverse certificate. -/
52 theorem map {R : Type u} {S : Type v} [Semiring R] [Semiring S]
53     {x y : R} (h : TwoSidedInverse x y) (q : R →+* S) :
54     TwoSidedInverse (q x) (q y) := by
55   constructor
56   · simpa only [map_mul, map_one] using congrArg q h.left_inv
57   · simpa only [map_mul, map_one] using congrArg q h.right_inv
58 
59 end TwoSidedInverse
60 
61 /-- The finite geometric candidate for the inverse of `1 + a`.
62 
63 No commutativity is assumed: this is the ordered sum `1 - a + a² - ⋯` through degree `N - 1`.
64 -/
65 def finiteGeometricInverse {R : Type u} [Ring R] (a : R) (N : ℕ) : R :=
66   ∑ n ∈ Finset.range N, (-a) ^ n
67 
68 /-- If `a ^ N = 0`, the finite geometric candidate is a genuine two-sided inverse of `1 + a`. -/
69 theorem finiteGeometricInverse_spec_of_pow_eq_zero {R : Type u} [Ring R]
70     (a : R) (N : ℕ) (hN : a ^ N = 0) :
71     TwoSidedInverse (1 + a) (finiteGeometricInverse a N) := by
72   have hneg : (-a) ^ N = 0 := by
73     rw [neg_pow, hN, mul_zero]
74   constructor
75   · simpa [finiteGeometricInverse, hneg] using geom_sum_mul_neg (-a) N
76   · simpa [finiteGeometricInverse, hneg] using mul_neg_geom_sum (-a) N
77 
78 /-- Data certifying a concrete nilpotence cutoff for `a`. -/
79 structure NilpotenceCertificate {R : Type u} [Ring R] (a : R) where
80   cutoff : ℕ
81   pow_eq_zero : a ^ cutoff = 0
82 
83 /-- The finite inverse selected by a nilpotence certificate. -/
84 def inverseFromCertificate {R : Type u} [Ring R] (a : R)
85     (certificate : NilpotenceCertificate a) : R :=
86   finiteGeometricInverse a certificate.cutoff
87 
88 /-- A nilpotence certificate produces a verified two-sided inverse. -/
89 theorem inverseFromCertificate_spec {R : Type u} [Ring R] (a : R)
90     (certificate : NilpotenceCertificate a) :
91     TwoSidedInverse (1 + a) (inverseFromCertificate a certificate) := by
92   exact finiteGeometricInverse_spec_of_pow_eq_zero
93     a certificate.cutoff certificate.pow_eq_zero
94 
95 /-- Multiplying a perturbation inverse by `Dinv` gives an inverse of `D + K`. -/
96 private theorem diagonal_inverse_of_perturbation_inverse {R : Type u} [Ring R]
97     (D Dinv K S : R) (hD : TwoSidedInverse D Dinv)
98     (hS : TwoSidedInverse (1 + Dinv * K) S) :
99     TwoSidedInverse (D + K) (S * Dinv) := by
100   constructor
101   · calc
102       (S * Dinv) * (D + K) = S * (Dinv * D + Dinv * K) := by
103         simp only [mul_add, mul_assoc]
104       _ = S * (1 + Dinv * K) := by rw [hD.left_inv]
105       _ = 1 := hS.left_inv
106   · have hfactor : D + K = D * (1 + Dinv * K) := by
107       symm
108       rw [mul_add, mul_one, ← mul_assoc, hD.right_inv, one_mul]
109     rw [hfactor]
110     calc
111       (D * (1 + Dinv * K)) * (S * Dinv) =
112           D * (((1 + Dinv * K) * S) * Dinv) := by
113             simp only [mul_assoc]
114       _ = D * (1 * Dinv) := by rw [hS.right_inv]
115       _ = 1 := by simpa only [one_mul] using hD.right_inv
116 
117 /-- The exact finite candidate for `(D + K)⁻¹` when `Dinv * K` is nilpotent. -/
118 def diagonalTransferInverse {R : Type u} [Ring R]
119     (Dinv K : R) (N : ℕ) : R :=
120   finiteGeometricInverse (Dinv * K) N * Dinv
121 
122 /-- Exact `D + K` inversion in a possibly noncommutative ring, under an explicit nilpotence
123 certificate for `Dinv * K`. -/
124 theorem diagonalTransferInverse_spec {R : Type u} [Ring R]
125     (D Dinv K : R) (N : ℕ) (hD : TwoSidedInverse D Dinv)
126     (hNil : (Dinv * K) ^ N = 0) :
127     TwoSidedInverse (D + K) (diagonalTransferInverse Dinv K N) := by
128   apply diagonal_inverse_of_perturbation_inverse D Dinv K
129   · exact hD
130   · exact finiteGeometricInverse_spec_of_pow_eq_zero (Dinv * K) N hNil
131 
132 /-! ## Exact inversion after passage to finite precision -/
133 
134 /-- If a ring homomorphism kills `a ^ L`, the mapped finite geometric sum is an exact inverse of
135 the mapped `1 + a`.  A quotient map is the primary application, but injectivity or surjectivity is
136 not needed. -/
137 theorem finitePrecisionInverse {R : Type u} {S : Type v} [Ring R] [Ring S]
138     (q : R →+* S) (a : R) (L : ℕ) (hPrecision : q (a ^ L) = 0) :
139     TwoSidedInverse (q (1 + a)) (q (finiteGeometricInverse a L)) := by
140   have hpow : (q a) ^ L = 0 := by
141     simpa only [map_pow] using hPrecision
142   have hmap : q (finiteGeometricInverse a L) = finiteGeometricInverse (q a) L := by
143     simp [finiteGeometricInverse]
144   simpa only [map_add, map_one, hmap] using
145     (finiteGeometricInverse_spec_of_pow_eq_zero (q a) L hpow)
146 
147 /-! ## Analytic specialization -/
148 
149 /-- The analytic geometric inverse.  Its specification below requires `‖a‖ < 1`. -/
150 noncomputable def analyticGeometricInverse {R : Type u} [NormedRing R]
151     (a : R) : R :=
152   ∑' n : ℕ, (-a) ^ n
153 
154 /-- In a complete normed ring, the geometric series is a two-sided inverse when `‖a‖ < 1`. -/
155 theorem analyticGeometricInverse_spec {R : Type u} [NormedRing R] [CompleteSpace R]
156     (a : R) (ha : ‖a‖ < 1) :
157     TwoSidedInverse (1 + a) (analyticGeometricInverse a) := by
158   have hneg : ‖-a‖ < 1 := by simpa only [norm_neg] using ha
159   have hs : Summable (fun n : ℕ ↦ (-a) ^ n) :=
160     summable_geometric_of_norm_lt_one hneg
161   constructor
162   · simpa [analyticGeometricInverse] using hs.tsum_pow_mul_one_sub
163   · simpa [analyticGeometricInverse] using hs.one_sub_mul_tsum_pow
164 
165 /-- The norm-convergent diagonal-plus-transfer candidate. -/
166 noncomputable def analyticDiagonalTransferInverse {R : Type u} [NormedRing R]
167     (Dinv K : R) : R :=
168   analyticGeometricInverse (Dinv * K) * Dinv
169 
170 /-- Analytic `D + K` inversion under the explicit Neumann-series condition
171 `‖Dinv * K‖ < 1`. -/
172 theorem analyticDiagonalTransferInverse_spec {R : Type u}
173     [NormedRing R] [CompleteSpace R] (D Dinv K : R)
174     (hD : TwoSidedInverse D Dinv) (hNorm : ‖Dinv * K‖ < 1) :
175     TwoSidedInverse (D + K) (analyticDiagonalTransferInverse Dinv K) := by
176   apply diagonal_inverse_of_perturbation_inverse D Dinv K
177   · exact hD
178   · exact analyticGeometricInverse_spec (Dinv * K) hNorm
179 
180 /-! ## Finite ordered-word expansion -/
181 
182 /-- Cumulative weight of an ordered transfer word. -/
183 def wordWeight {E : Type u} (weight : E → ℕ) (word : List E) : ℕ :=
184   (word.map weight).sum
185 
186 /-- Ordered, hence generally noncommutative, product attached to a transfer word. -/
187 def wordProduct {E : Type u} {R : Type v} [Monoid R]
188     (edge : E → R) (word : List E) : R :=
189   (word.map edge).prod
190 
191 @[simp] theorem wordWeight_nil {E : Type u} (weight : E → ℕ) :
192     wordWeight weight [] = 0 := rfl
193 
194 @[simp] theorem wordWeight_cons {E : Type u} (weight : E → ℕ)
195     (e : E) (word : List E) :
196     wordWeight weight (e :: word) = weight e + wordWeight weight word := rfl
197 
198 @[simp] theorem wordProduct_nil {E : Type u} {R : Type v} [Monoid R]
199     (edge : E → R) :
200     wordProduct edge [] = 1 := rfl
201 
202 @[simp] theorem wordProduct_cons {E : Type u} {R : Type v} [Monoid R]
203     (edge : E → R) (e : E) (word : List E) :
204     wordProduct edge (e :: word) = edge e * wordProduct edge word := rfl
205 
206 /-- The `n`th power of a finite sum is the sum of the ordered products indexed by all length-`n`
207 words.  The order recorded by `List.ofFn` is retained, so no commutativity hypothesis appears. -/
208 theorem sum_fixedWordProduct_eq_pow {E : Type u} {R : Type v}
209     [Fintype E] [Ring R] (edge : E → R) (n : ℕ) :
210     (∑ word : Fin n → E, wordProduct edge (List.ofFn word)) =
211       (∑ e : E, edge e) ^ n := by
212   induction n with
213   | zero => simp
214   | succ n ih =>
215       let split : E × (Fin n → E) ≃ (Fin (n + 1) → E) :=
216         Fin.consEquiv (fun _ : Fin (n + 1) ↦ E)
217       calc
218         (∑ word : Fin (n + 1) → E, wordProduct edge (List.ofFn word)) =
219             ∑ pair : E × (Fin n → E),
220               wordProduct edge (List.ofFn (split pair)) := by
221                 simpa only using (split.sum_comp
222                   (fun word : Fin (n + 1) → E ↦ wordProduct edge (List.ofFn word))).symm
223         _ = ∑ pair : E × (Fin n → E),
224               edge pair.1 * wordProduct edge (List.ofFn pair.2) := by
225                 apply Finset.sum_congr rfl
226                 intro pair _
227                 simp [split, wordProduct]
228         _ = (∑ e : E, edge e) *
229               (∑ word : Fin n → E, wordProduct edge (List.ofFn word)) := by
230                 rw [Fintype.sum_prod_type]
231                 rw [Finset.sum_mul]
232                 simp only [Finset.mul_sum]
233         _ = (∑ e : E, edge e) ^ (n + 1) := by
234                 rw [ih, pow_succ']
235 
236 /-! ## Multiplicative filtrations and precision certificates -/
237 
238 /-- A decreasing additive filtration whose levels multiply by adding indices.
239 
240 The structure records exactly the closure properties needed for finite-precision transfer words.
241 It makes no completeness or convergence claim.
242 -/
243 structure MultiplicativeFiltration (R : Type u) [Ring R] where
244   Mem : ℕ → R → Prop
245   zero_mem : ∀ n, Mem n 0
246   add_mem : ∀ {n x y}, Mem n x → Mem n y → Mem n (x + y)
247   neg_mem : ∀ {n x}, Mem n x → Mem n (-x)
248   one_mem : Mem 0 1
249   antitone : ∀ {m n x}, m ≤ n → Mem n x → Mem m x
250   mul_mem : ∀ {m n x y}, Mem m x → Mem n y → Mem (m + n) (x * y)
251 
252 namespace MultiplicativeFiltration
253 
254 variable {R : Type u} [Ring R]
255 
256 /-- Membership notation-friendly wrapper. -/
257 def Contains (filtration : MultiplicativeFiltration R) (n : ℕ) (x : R) : Prop :=
258   filtration.Mem n x
259 
260 /-- Products of filtered edge terms lie at the cumulative word weight. -/
261 theorem wordProduct_mem (filtration : MultiplicativeFiltration R)
262     {E : Type v} (weight : E → ℕ) (edge : E → R)
263     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) (word : List E) :
264     filtration.Mem (wordWeight weight word) (wordProduct edge word) := by
265   induction word with
266   | nil => exact filtration.one_mem
267   | cons e word ih =>
268       exact filtration.mul_mem (hedge e) ih
269 
270 end MultiplicativeFiltration
271 
272 /-- A map realizes precision `L` when it kills every element in filtration level `L`. -/
273 structure PrecisionCertificate {R : Type u} {S : Type v} [Ring R] [Ring S]
274     (filtration : MultiplicativeFiltration R) (q : R →+* S) (L : ℕ) : Prop where
275   map_eq_zero : ∀ {x : R}, filtration.Mem L x → q x = 0
276 
277 /-- A transfer word whose cumulative weight reaches `L` vanishes in every realization carrying a
278 precision-`L` certificate. -/
279 theorem wordProduct_vanishes_at_precision {R : Type u} {S : Type v}
280     [Ring R] [Ring S] (filtration : MultiplicativeFiltration R)
281     (q : R →+* S) (L : ℕ) (certificate : PrecisionCertificate filtration q L)
282     {E : Type w} (weight : E → ℕ) (edge : E → R)
283     (hedge : ∀ e, filtration.Mem (weight e) (edge e))
284     (word : List E) (hweight : L ≤ wordWeight weight word) :
285     q (wordProduct edge word) = 0 := by
286   apply certificate.map_eq_zero
287   apply filtration.antitone hweight
288   exact filtration.wordProduct_mem weight edge hedge word
289 
290 /-- Mapping a finite word expansion is unchanged when all words of cumulative weight at least `L`
291 are pruned. -/
292 theorem map_eq_pruned_of_wordExpansion {R : Type u} {S : Type v}
293     [Ring R] [Ring S] (filtration : MultiplicativeFiltration R)
294     (q : R →+* S) (L : ℕ) (certificate : PrecisionCertificate filtration q L)
295     {E : Type w} [DecidableEq E] (weight : E → ℕ) (edge : E → R)
296     (hedge : ∀ e, filtration.Mem (weight e) (edge e))
297     (words : Finset (List E)) (x : R)
298     (hexpansion : x = ∑ word ∈ words, wordProduct edge word) :
299     q x = ∑ word ∈ words.filter (fun word ↦ wordWeight weight word < L),
300       q (wordProduct edge word) := by
301   rw [hexpansion, map_sum]
302   classical
303   rw [Finset.sum_filter]
304   apply Finset.sum_congr rfl
305   intro word hword
306   by_cases hlow : wordWeight weight word < L
307   · simp [hlow]
308   · simp only [hlow, ↓reduceIte]
309     exact wordProduct_vanishes_at_precision
310       filtration q L certificate weight edge hedge word (Nat.le_of_not_gt hlow)
311 
312 /-! ## Explicit pruned word inverses -/
313 
314 /-- The length-`n` part of the word expansion after retaining exactly the words whose cumulative
315 weight is strictly below precision `L`. -/
316 def retainedFixedWordSum {E : Type u} {R : Type v} [Fintype E] [Ring R]
317     (weight : E → ℕ) (edge : E → R) (L n : ℕ) : R :=
318   ∑ word : Fin n → E with wordWeight weight (List.ofFn word) < L,
319     wordProduct edge (List.ofFn word)
320 
321 /-- The explicit signed, weight-pruned word candidate through word length `N - 1`.
322 
323 Unlike `finiteGeometricInverse`, this expression visibly contains only retained transfer words:
324 every summand has cumulative weight strictly below `L`.  The independent length cutoff `N` permits
325 the sharper cutoff obtained from a lower bound on all edge weights. -/
326 def prunedWordInverse {E : Type u} {R : Type v} [Fintype E] [Ring R]
327     (weight : E → ℕ) (edge : E → R) (L N : ℕ) : R :=
328   ∑ n ∈ Finset.range N, (-1 : R) ^ n * retainedFixedWordSum weight edge L n
329 
330 /-- At precision `L`, the full length-`n` word expansion maps to its explicitly retained part. -/
331 theorem map_pow_eq_retainedFixedWordSum {R : Type u} {S : Type v}
332     [Ring R] [Ring S] (filtration : MultiplicativeFiltration R)
333     (q : R →+* S) (L : ℕ) (certificate : PrecisionCertificate filtration q L)
334     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
335     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) (n : ℕ) :
336     q ((∑ e : E, edge e) ^ n) = q (retainedFixedWordSum weight edge L n) := by
337   rw [← sum_fixedWordProduct_eq_pow edge n]
338   simp only [retainedFixedWordSum, map_sum]
339   classical
340   rw [Finset.sum_filter]
341   apply Finset.sum_congr rfl
342   intro word _
343   by_cases hlow : wordWeight weight (List.ofFn word) < L
344   · simp [hlow]
345   · simp only [hlow, ↓reduceIte]
346     exact wordProduct_vanishes_at_precision filtration q L certificate weight edge hedge
347       (List.ofFn word) (Nat.le_of_not_gt hlow)
348 
349 /-- The mapped finite geometric inverse is exactly the mapped explicit pruned-word expression.
350 
351 This is the direct bridge missing from the abstract pruning statement: it derives the expansion
352 from the finite edge sum, keeps the noncommutative word order, inserts the alternating geometric
353 sign, and removes every word of weight at least `L`. -/
354 theorem map_finiteGeometricInverse_eq_prunedWordInverse
355     {R : Type u} {S : Type v} [Ring R] [Ring S]
356     (filtration : MultiplicativeFiltration R)
357     (q : R →+* S) (L N : ℕ) (certificate : PrecisionCertificate filtration q L)
358     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
359     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
360     q (finiteGeometricInverse (∑ e : E, edge e) N) =
361       q (prunedWordInverse weight edge L N) := by
362   simp only [finiteGeometricInverse, prunedWordInverse, map_sum, map_mul, map_pow, map_neg,
363     map_one]
364   apply Finset.sum_congr rfl
365   intro n _
366   rw [neg_pow]
367   congr 1
368   simpa only [map_pow, map_sum] using
369     (map_pow_eq_retainedFixedWordSum filtration q L certificate weight edge hedge n)
370 
371 /-- If the normalized transfer is nilpotent after mapping, the explicit pruned word sum is a
372 two-sided inverse.  The precision cutoff `L` and nilpotence/length cutoff `N` are independent. -/
373 theorem prunedWordInverse_spec_of_pow_eq_zero
374     {R : Type u} {S : Type v} [Ring R] [Ring S]
375     (filtration : MultiplicativeFiltration R)
376     (q : R →+* S) (L N : ℕ) (certificate : PrecisionCertificate filtration q L)
377     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
378     (hedge : ∀ e, filtration.Mem (weight e) (edge e))
379     (hNil : q ((∑ e : E, edge e) ^ N) = 0) :
380     TwoSidedInverse
381       (q (1 + ∑ e : E, edge e))
382       (q (prunedWordInverse weight edge L N)) := by
383   have hfull := finitePrecisionInverse q (∑ e : E, edge e) N hNil
384   rw [← map_finiteGeometricInverse_eq_prunedWordInverse
385     filtration q L N certificate weight edge hedge]
386   exact hfull
387 
388 /-- When each edge has positive weight, word length is bounded by cumulative weight. -/
389 theorem length_le_wordWeight {E : Type u} (weight : E → ℕ)
390     (hpositive : ∀ e, 1 ≤ weight e) (word : List E) :
391     word.length ≤ wordWeight weight word := by
392   induction word with
393   | nil => simp
394   | cons e word ih =>
395       rw [List.length_cons, wordWeight_cons]
396       calc
397         word.length + 1 = 1 + word.length := Nat.add_comm _ _
398         _ ≤ weight e + wordWeight weight word := Nat.add_le_add (hpositive e) ih
399 
400 /-- A uniform lower bound `m` on edge weights gives the sharper estimate
401 `m * word.length ≤ wordWeight weight word`. -/
402 theorem minWeight_mul_length_le_wordWeight {E : Type u} (weight : E → ℕ) (m : ℕ)
403     (hmin : ∀ e, m ≤ weight e) (word : List E) :
404     m * word.length ≤ wordWeight weight word := by
405   induction word with
406   | nil => simp
407   | cons e word ih =>
408       rw [List.length_cons, wordWeight_cons, Nat.mul_succ, Nat.add_comm (m * word.length) m]
409       exact Nat.add_le_add (hmin e) ih
410 
411 /-- Positive edge weights force the `L`th power of their sum to vanish in a precision-`L`
412 realization.  The proof uses the full noncommutative word expansion. -/
413 theorem map_sum_pow_eq_zero_at_cutoff {R : Type u} {S : Type v}
414     [Ring R] [Ring S] (filtration : MultiplicativeFiltration R)
415     (q : R →+* S) (L : ℕ) (certificate : PrecisionCertificate filtration q L)
416     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
417     (hpositive : ∀ e, 1 ≤ weight e)
418     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
419     q ((∑ e : E, edge e) ^ L) = 0 := by
420   rw [← sum_fixedWordProduct_eq_pow edge L, map_sum]
421   apply Finset.sum_eq_zero
422   intro word _
423   apply wordProduct_vanishes_at_precision
424     filtration q L certificate weight edge hedge (List.ofFn word)
425   simpa only [List.length_ofFn] using
426     length_le_wordWeight weight hpositive (List.ofFn word)
427 
428 /-- A minimum edge weight `m` permits any nilpotence cutoff `N` satisfying `L ≤ m * N`.
429 
430 For `m > 1`, this can be strictly smaller than the coarse length cutoff `N = L`. -/
431 theorem map_sum_pow_eq_zero_at_scaled_cutoff {R : Type u} {S : Type v}
432     [Ring R] [Ring S] (filtration : MultiplicativeFiltration R)
433     (q : R →+* S) (L m N : ℕ) (certificate : PrecisionCertificate filtration q L)
434     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
435     (hmin : ∀ e, m ≤ weight e) (hcutoff : L ≤ m * N)
436     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
437     q ((∑ e : E, edge e) ^ N) = 0 := by
438   rw [← sum_fixedWordProduct_eq_pow edge N, map_sum]
439   apply Finset.sum_eq_zero
440   intro word _
441   apply wordProduct_vanishes_at_precision
442     filtration q L certificate weight edge hedge (List.ofFn word)
443   calc
444     L ≤ m * N := hcutoff
445     _ = m * (List.ofFn word).length := by simp only [List.length_ofFn]
446     _ ≤ wordWeight weight (List.ofFn word) :=
447       minWeight_mul_length_le_wordWeight weight m hmin (List.ofFn word)
448 
449 /-- The executable ceiling cutoff used in the manuscript satisfies the
450 scaled cutoff inequality.  Positivity of `m` is essential: ceiling division
451 by zero is not a valid minimum-weight cutoff. -/
452 theorem le_mul_ceilDiv (L m : ℕ) (hm : 0 < m) :
453     L ≤ m * (L ⌈/⌉ m) := by
454   exact (ceilDiv_le_iff_le_mul hm).mp le_rfl
455 
456 /-- The explicit pruned word expression is a two-sided finite-precision inverse at any scaled
457 cutoff `N` satisfying `L ≤ m * N`. -/
458 theorem prunedWordInverse_spec_of_minWeight
459     {R : Type u} {S : Type v} [Ring R] [Ring S]
460     (filtration : MultiplicativeFiltration R)
461     (q : R →+* S) (L m N : ℕ) (certificate : PrecisionCertificate filtration q L)
462     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
463     (hmin : ∀ e, m ≤ weight e) (hcutoff : L ≤ m * N)
464     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
465     TwoSidedInverse
466       (q (1 + ∑ e : E, edge e))
467       (q (prunedWordInverse weight edge L N)) := by
468   apply prunedWordInverse_spec_of_pow_eq_zero
469     filtration q L N certificate weight edge hedge
470   exact map_sum_pow_eq_zero_at_scaled_cutoff
471     filtration q L m N certificate weight edge hmin hcutoff hedge
472 
473 /-- The common positive-weight specialization uses the coarse but assumption-free cutoff `N=L`. -/
474 theorem finitePrecisionPrunedInverse_of_weightedEdges
475     {R : Type u} {S : Type v} [Ring R] [Ring S]
476     (filtration : MultiplicativeFiltration R)
477     (q : R →+* S) (L : ℕ) (certificate : PrecisionCertificate filtration q L)
478     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
479     (hpositive : ∀ e, 1 ≤ weight e)
480     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
481     TwoSidedInverse
482       (q (1 + ∑ e : E, edge e))
483       (q (prunedWordInverse weight edge L L)) := by
484   exact prunedWordInverse_spec_of_minWeight
485     filtration q L 1 L certificate weight edge hpositive (by simp) hedge
486 
487 /-- Weighted finite-precision inversion: positive filtered edge weights provide the nilpotence
488 cutoff needed by the finite geometric inverse. -/
489 theorem finitePrecisionInverse_of_weightedEdges {R : Type u} {S : Type v}
490     [Ring R] [Ring S] (filtration : MultiplicativeFiltration R)
491     (q : R →+* S) (L : ℕ) (certificate : PrecisionCertificate filtration q L)
492     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
493     (hpositive : ∀ e, 1 ≤ weight e)
494     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
495     TwoSidedInverse
496       (q (1 + ∑ e : E, edge e))
497       (q (finiteGeometricInverse (∑ e : E, edge e) L)) := by
498   apply finitePrecisionInverse q (∑ e : E, edge e) L
499   exact map_sum_pow_eq_zero_at_cutoff
500     filtration q L certificate weight edge hpositive hedge
501 
502 /--
503 Full mapped diagonal-plus-transfer inversion from positive filtered edge data.
504 
505 The equality `Dinv * K = ∑ e, edge e` identifies the normalized transfer with
506 the supplied weighted edge expansion.  Its `L`th power vanishes after `q`, the
507 inverse certificate for `D` maps to the target ring, and the diagonal
508 factorization then gives the displayed two-sided inverse of `q (D + K)`.
509 -/
510 theorem finitePrecisionDiagonalTransferInverse_of_weightedEdges
511     {R : Type u} {S : Type v} [Ring R] [Ring S]
512     (filtration : MultiplicativeFiltration R)
513     (q : R →+* S) (L : ℕ) (certificate : PrecisionCertificate filtration q L)
514     (D Dinv K : R) (hD : TwoSidedInverse D Dinv)
515     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
516     (htransfer : Dinv * K = ∑ e : E, edge e)
517     (hpositive : ∀ e, 1 ≤ weight e)
518     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
519     TwoSidedInverse
520       (q (D + K))
521       (q (finiteGeometricInverse (Dinv * K) L * Dinv)) := by
522   have hprecision : q ((Dinv * K) ^ L) = 0 := by
523     rw [htransfer]
524     exact map_sum_pow_eq_zero_at_cutoff
525       filtration q L certificate weight edge hpositive hedge
526   have hnil : (q Dinv * q K) ^ L = 0 := by
527     simpa only [map_pow, map_mul] using hprecision
528   have hmappedD : TwoSidedInverse (q D) (q Dinv) := hD.map q
529   have hdiagonal :=
530     diagonalTransferInverse_spec (q D) (q Dinv) (q K) L hmappedD hnil
531   have hgeometric :
532       q (finiteGeometricInverse (Dinv * K) L) =
533         finiteGeometricInverse (q Dinv * q K) L := by
534     simp [finiteGeometricInverse]
535   simpa only [diagonalTransferInverse, map_add, map_mul, hgeometric] using hdiagonal
536 
537 /-- The explicit weight-pruned diagonal-plus-transfer inverse candidate. -/
538 def prunedDiagonalTransferInverse {E : Type u} {R : Type v} [Fintype E] [Ring R]
539     (weight : E → ℕ) (edge : E → R) (Dinv : R) (L N : ℕ) : R :=
540   prunedWordInverse weight edge L N * Dinv
541 
542 /-- Full mapped diagonal-plus-transfer inversion with an explicit pruned word inverse and the
543 scaled cutoff supplied by a minimum edge weight. -/
544 theorem finitePrecisionPrunedDiagonalTransferInverse_of_minWeight
545     {R : Type u} {S : Type v} [Ring R] [Ring S]
546     (filtration : MultiplicativeFiltration R)
547     (q : R →+* S) (L m N : ℕ) (certificate : PrecisionCertificate filtration q L)
548     (D Dinv K : R) (hD : TwoSidedInverse D Dinv)
549     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
550     (htransfer : Dinv * K = ∑ e : E, edge e)
551     (hmin : ∀ e, m ≤ weight e) (hcutoff : L ≤ m * N)
552     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
553     TwoSidedInverse
554       (q (D + K))
555       (q (prunedDiagonalTransferInverse weight edge Dinv L N)) := by
556   have hpruned := prunedWordInverse_spec_of_minWeight
557     filtration q L m N certificate weight edge hmin hcutoff hedge
558   have htransferMapped : q Dinv * q K = ∑ e : E, q (edge e) := by
559     simpa only [map_mul, map_sum] using congrArg q htransfer
560   have hnormalized :
561       TwoSidedInverse (1 + q Dinv * q K) (q (prunedWordInverse weight edge L N)) := by
562     simpa only [map_add, map_one, map_sum, htransferMapped] using hpruned
563   have hdiagonal := diagonal_inverse_of_perturbation_inverse
564     (q D) (q Dinv) (q K) (q (prunedWordInverse weight edge L N)) (hD.map q) hnormalized
565   simpa only [prunedDiagonalTransferInverse, map_add, map_mul] using hdiagonal
566 
567 /-- Positive edge weights give the explicit pruned diagonal inverse at the standard cutoff
568 `N = L`. -/
569 theorem finitePrecisionPrunedDiagonalTransferInverse_of_weightedEdges
570     {R : Type u} {S : Type v} [Ring R] [Ring S]
571     (filtration : MultiplicativeFiltration R)
572     (q : R →+* S) (L : ℕ) (certificate : PrecisionCertificate filtration q L)
573     (D Dinv K : R) (hD : TwoSidedInverse D Dinv)
574     {E : Type w} [Fintype E] (weight : E → ℕ) (edge : E → R)
575     (htransfer : Dinv * K = ∑ e : E, edge e)
576     (hpositive : ∀ e, 1 ≤ weight e)
577     (hedge : ∀ e, filtration.Mem (weight e) (edge e)) :
578     TwoSidedInverse
579       (q (D + K))
580       (q (prunedDiagonalTransferInverse weight edge Dinv L L)) := by
581   exact finitePrecisionPrunedDiagonalTransferInverse_of_minWeight
582     filtration q L 1 L certificate D Dinv K hD weight edge htransfer hpositive (by simp) hedge
583 
584 end Komorebi.PaperII.WeightedTransfer

Back to source controls