ResultantSeparation.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 import Mathlib.Algebra.Polynomial.Basic
11 import Mathlib.Algebra.Polynomial.Coeff
12 import Mathlib.Data.Finset.NatAntidiagonal
13 import Mathlib.Data.Fintype.Card
14 import Mathlib.Data.Matrix.Basic
15 import Mathlib.LinearAlgebra.Matrix.Adjugate
16 import Mathlib.RingTheory.PowerSeries.Basic
17 import Mathlib.RingTheory.PowerSeries.Inverse
18 import Mathlib.Analysis.Normed.Ring.Basic
19 import Mathlib.Tactic.NoncommRing
20 import Mathlib.Algebra.BigOperators.Intervals
21 import Mathlib.Algebra.Module.Submodule.LinearMap
22 import Mathlib.Algebra.Polynomial.Eval.Defs
23 import Mathlib.Analysis.Normed.Operator.Basic
24 import Mathlib.Tactic.Abel
25 import Mathlib.Util.AssertNoSorry
26 import Mathlib.Analysis.Complex.Exponential
27 import Mathlib.LinearAlgebra.Matrix.Notation
28 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
29 import Mathlib.Data.Nat.ChineseRemainder
30 import Mathlib.GroupTheory.SpecificGroups.Cyclic
31 import Mathlib.NumberTheory.Padics.PadicVal.Basic
32 import Mathlib.RingTheory.Polynomial.Resultant.Basic
33 import Mathlib.Tactic.NormNum
34 import Mathlib.Tactic.Ring
35 import Mathlib.Tactic.FinCases
36 import Mathlib.Tactic.FieldSimp
37 import Mathlib.Tactic.Push
38 import Mathlib.Tactic.ByContra
39 import Mathlib.Tactic.SplitIfs
40 import Mathlib.Tactic.FunProp
41 
42 /-!
43 # Paper II: evaluated Bezout separation and precision delay
44 
45 Author: Komorebi P.
46 
47 This file starts with evaluated endomorphism certificates.  It does not construct polynomial
48 resultants, and it does not promote nilpotence on a primary summand to exact kernel action.  The
49 identity and zero actions below follow only from the displayed Bezout and annihilation equations.
50 -/
51 
52 set_option autoImplicit false
53 
54 namespace Komorebi.PaperII.ResultantSeparation
55 
56 universe u v
57 
58 variable {K : Type u} {M : Type v}
59 variable [Field K] [AddCommGroup M] [Module K M]
60 
61 abbrev End := Module.End K M
62 
63 /-! ## Evaluated certificate and its numerator -/
64 
65 /-- The certificate obtained after evaluating a Bezout identity at an operator.
66 
67 All four supplied endomorphisms are required to commute, `UF + VG = rI` is recorded verbatim,
68 and `FG = 0` is a separate certificate.  In particular, no resultant construction or
69 nilpotence-to-kernel inference is hidden in this structure.
70 -/
71 structure EvaluatedBezoutCertificate (F G U V : End (K := K) (M := M)) (r : K) : Prop where
72   r_ne_zero : r ≠ 0
73   commute_FG : Commute F G
74   commute_FU : Commute F U
75   commute_FV : Commute F V
76   commute_GU : Commute G U
77   commute_GV : Commute G V
78   commute_UV : Commute U V
79   bezout : U * F + V * G = r • (1 : End (K := K) (M := M))
80   annihilate : F * G = 0
81 
82 /-- The integral numerator `VG` of the evaluated separator. -/
83 def separatorNumerator (V G : End (K := K) (M := M)) : End (K := K) (M := M) :=
84   V * G
85 
86 /-- The rational separator `r⁻¹ VG`. -/
87 def separator (r : K) (V G : End (K := K) (M := M)) : End (K := K) (M := M) :=
88   r⁻¹ • separatorNumerator V G
89 
90 variable {F G U V : End (K := K) (M := M)} {r : K}
91 
92 /-- Minimal form of the numerator identity: only the evaluated Bezout equality is needed. -/
93 theorem separatorNumerator_eq_scalar_sub_of_bezout
94     (bezout : U * F + V * G = r • (1 : End (K := K) (M := M))) :
95     separatorNumerator V G = r • (1 : End (K := K) (M := M)) - U * F := by
96   apply (eq_sub_iff_add_eq).2
97   simpa only [separatorNumerator, add_comm] using bezout
98 
99 /-- The numerator is also `rI - UF`, directly from the evaluated Bezout identity. -/
100 theorem separatorNumerator_eq_scalar_sub
101     (certificate : EvaluatedBezoutCertificate F G U V r) :
102     separatorNumerator V G = r • (1 : End (K := K) (M := M)) - U * F := by
103   exact separatorNumerator_eq_scalar_sub_of_bezout certificate.bezout
104 
105 /-- Minimal form of cross-term vanishing.  Among the six commutation fields in the bundled
106 certificate, only `FG = GF` and `GU = UG` enter this calculation. -/
107 theorem separatorNumerator_mul_complement_eq_zero_of_commute
108     (commute_FG : Commute F G) (commute_GU : Commute G U) (annihilate : F * G = 0) :
109     separatorNumerator V G * (U * F) = 0 := by
110   calc
111     separatorNumerator V G * (U * F) = V * (G * U) * F := by
112       simp only [separatorNumerator, mul_assoc]
113     _ = V * (U * G) * F := by rw [commute_GU.eq]
114     _ = (V * U) * (G * F) := by simp only [mul_assoc]
115     _ = (V * U) * (F * G) := by rw [← commute_FG.eq]
116     _ = 0 := by rw [annihilate, mul_zero]
117 
118 /-- The cross term which occurs in the numerator-square calculation vanishes. -/
119 theorem separatorNumerator_mul_complement_eq_zero
120     (certificate : EvaluatedBezoutCertificate F G U V r) :
121     separatorNumerator V G * (U * F) = 0 := by
122   exact separatorNumerator_mul_complement_eq_zero_of_commute
123     certificate.commute_FG certificate.commute_GU certificate.annihilate
124 
125 /-- Minimal denominator-free quasi-idempotence theorem.  It requires neither `r ≠ 0` nor the
126 four commutation relations unused by the numerator-square calculation. -/
127 theorem separatorNumerator_mul_self_of_bezout
128     (bezout : U * F + V * G = r • (1 : End (K := K) (M := M)))
129     (commute_FG : Commute F G) (commute_GU : Commute G U) (annihilate : F * G = 0) :
130     separatorNumerator V G * separatorNumerator V G = r • separatorNumerator V G := by
131   calc
132     separatorNumerator V G * separatorNumerator V G =
133         separatorNumerator V G *
134           (r • (1 : End (K := K) (M := M)) - U * F) := by
135             exact congrArg (separatorNumerator V G * ·)
136               (separatorNumerator_eq_scalar_sub_of_bezout bezout)
137     _ = separatorNumerator V G * (r • (1 : End (K := K) (M := M))) -
138           separatorNumerator V G * (U * F) := by rw [mul_sub]
139     _ = r • separatorNumerator V G := by
140       rw [separatorNumerator_mul_complement_eq_zero_of_commute
141         commute_FG commute_GU annihilate]
142       simp only [sub_zero, mul_smul_comm, mul_one]
143 
144 /-- The denominator-free numerator identity `N² = rN`. -/
145 theorem separatorNumerator_mul_self
146     (certificate : EvaluatedBezoutCertificate F G U V r) :
147     separatorNumerator V G * separatorNumerator V G = r • separatorNumerator V G := by
148   exact separatorNumerator_mul_self_of_bezout certificate.bezout certificate.commute_FG
149     certificate.commute_GU certificate.annihilate
150 
151 /-- Minimal idempotence theorem for the normalized separator. -/
152 theorem separator_idempotent_of_bezout
153     (r_ne_zero : r ≠ 0)
154     (bezout : U * F + V * G = r • (1 : End (K := K) (M := M)))
155     (commute_FG : Commute F G) (commute_GU : Commute G U) (annihilate : F * G = 0) :
156     separator r V G * separator r V G = separator r V G := by
157   rw [separator, smul_mul_smul,
158     separatorNumerator_mul_self_of_bezout bezout commute_FG commute_GU annihilate]
159   rw [smul_smul]
160   apply congrArg (fun a : K => a • separatorNumerator V G)
161   field_simp [r_ne_zero]
162 
163 /-- The evaluated separator is idempotent. -/
164 theorem separator_idempotent
165     (certificate : EvaluatedBezoutCertificate F G U V r) :
166     separator r V G * separator r V G = separator r V G := by
167   exact separator_idempotent_of_bezout certificate.r_ne_zero certificate.bezout
168     certificate.commute_FG certificate.commute_GU certificate.annihilate
169 
170 /-! ## Exact action on the two certified kernels -/
171 
172 /-- Minimal kernel-action theorem: evaluated Bezout alone makes the numerator act by `r` on
173 `ker F`. -/
174 theorem separatorNumerator_apply_of_mem_ker_F_of_bezout
175     (bezout : U * F + V * G = r • (1 : End (K := K) (M := M))) {x : M}
176     (hx : x ∈ LinearMap.ker F) :
177     separatorNumerator V G x = r • x := by
178   change F x = 0 at hx
179   have h := LinearMap.congr_fun bezout x
180   simpa [separatorNumerator, hx] using h
181 
182 /-- On the exact kernel of `F`, the numerator acts by the scalar `r`. -/
183 theorem separatorNumerator_apply_of_mem_ker_F
184     (certificate : EvaluatedBezoutCertificate F G U V r) {x : M}
185     (hx : x ∈ LinearMap.ker F) :
186     separatorNumerator V G x = r • x := by
187   exact separatorNumerator_apply_of_mem_ker_F_of_bezout certificate.bezout hx
188 
189 /-- Minimal normalized kernel-action theorem. -/
190 theorem separator_apply_of_mem_ker_F_of_bezout
191     (r_ne_zero : r ≠ 0)
192     (bezout : U * F + V * G = r • (1 : End (K := K) (M := M))) {x : M}
193     (hx : x ∈ LinearMap.ker F) :
194     separator r V G x = x := by
195   rw [separator, LinearMap.smul_apply,
196     separatorNumerator_apply_of_mem_ker_F_of_bezout bezout hx]
197   simp [smul_smul, r_ne_zero]
198 
199 /-- The separator is exactly the identity on `ker F`. -/
200 theorem separator_apply_of_mem_ker_F
201     (certificate : EvaluatedBezoutCertificate F G U V r) {x : M}
202     (hx : x ∈ LinearMap.ker F) :
203     separator r V G x = x := by
204   exact separator_apply_of_mem_ker_F_of_bezout certificate.r_ne_zero certificate.bezout hx
205 
206 /-- The numerator vanishes on `ker G`. -/
207 theorem separatorNumerator_apply_of_mem_ker_G
208     {x : M} (hx : x ∈ LinearMap.ker G) :
209     separatorNumerator V G x = 0 := by
210   change G x = 0 at hx
211   simp [separatorNumerator, hx]
212 
213 /-- The separator is exactly zero on `ker G`. -/
214 theorem separator_apply_of_mem_ker_G
215     {x : M} (hx : x ∈ LinearMap.ker G) :
216     separator r V G x = 0 := by
217   simp [separator, separatorNumerator_apply_of_mem_ker_G hx]
218 
219 /-! ## Lattice preservation and denominator certificates -/
220 
221 /-- An endomorphism preserves the chosen additive lattice. -/
222 def PreservesLattice (T : End (K := K) (M := M)) (lattice : AddSubgroup M) : Prop :=
223   ∀ x : M, x ∈ lattice → T x ∈ lattice
224 
225 /-- A scalar preserves the chosen additive lattice.  This is deliberately explicit: when `K` is
226 a fraction field, algebraic invertibility in `K` alone does not imply preservation of a chosen
227 valuation lattice. -/
228 def ScalarPreservesLattice (a : K) (lattice : AddSubgroup M) : Prop :=
229   ∀ x : M, x ∈ lattice → a • x ∈ lattice
230 
231 /-- A field unit acts as an automorphism of the chosen lattice: both it and its inverse preserve
232 the lattice.  This is the precise lattice condition needed for unit factors in a denominator. -/
233 def IsLatticeUnit (u : Kˣ) (lattice : AddSubgroup M) : Prop :=
234   ScalarPreservesLattice (u : K) lattice ∧ ScalarPreservesLattice (↑(u⁻¹) : K) lattice
235 
236 /-- Multiplicative closure of lattice preservation under composition. -/
237 theorem PreservesLattice.mul {S T : End (K := K) (M := M)} {lattice : AddSubgroup M}
238     (hS : PreservesLattice S lattice) (hT : PreservesLattice T lattice) :
239     PreservesLattice (S * T) lattice := by
240   intro x hx
241   exact hS (T x) (hT x hx)
242 
243 /-- Multiplying a lattice-preserving endomorphism by a lattice-preserving scalar preserves the
244 lattice. -/
245 theorem ScalarPreservesLattice.smul {a : K} {T : End (K := K) (M := M)}
246     {lattice : AddSubgroup M} (ha : ScalarPreservesLattice a lattice)
247     (hT : PreservesLattice T lattice) :
248     PreservesLattice (a • T) lattice := by
249   intro x hx
250   rw [LinearMap.smul_apply]
251   exact ha (T x) (hT x hx)
252 
253 /-- Lattice-preserving scalars are closed under multiplication. -/
254 theorem ScalarPreservesLattice.mul {a b : K} {lattice : AddSubgroup M}
255     (ha : ScalarPreservesLattice a lattice)
256     (hb : ScalarPreservesLattice b lattice) :
257     ScalarPreservesLattice (a * b) lattice := by
258   intro x hx
259   rw [mul_smul]
260   exact ha (b • x) (hb x hx)
261 
262 /-- Every power of a lattice-preserving scalar preserves the lattice. -/
263 theorem ScalarPreservesLattice.pow {a : K} {lattice : AddSubgroup M}
264     (ha : ScalarPreservesLattice a lattice) :
265     ∀ n : ℕ, ScalarPreservesLattice (a ^ n) lattice := by
266   intro n
267   induction n with
268   | zero =>
269       intro x hx
270       simpa using hx
271   | succ n ih =>
272       simpa [pow_succ] using ih.mul ha
273 
274 /-- Lattice units are closed under inversion. -/
275 theorem IsLatticeUnit.inv {u : Kˣ} {lattice : AddSubgroup M}
276     (hu : IsLatticeUnit u lattice) :
277     IsLatticeUnit u⁻¹ lattice := by
278   constructor
279   · exact hu.2
280   · simpa using hu.1
281 
282 /-- If `V` and `G` preserve the lattice, so does the numerator `VG`. -/
283 theorem separatorNumerator_preservesLattice {lattice : AddSubgroup M}
284     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
285     PreservesLattice (separatorNumerator V G) lattice := by
286   exact hV.mul hG
287 
288 /-- Clearing the displayed nonzero denominator recovers the numerator exactly. -/
289 theorem scalar_mul_separator_of_ne_zero (r_ne_zero : r ≠ 0) :
290     r • separator r V G = separatorNumerator V G := by
291   simp [separator, smul_smul, r_ne_zero]
292 
293 /-- Clearing the displayed nonzero denominator recovers the numerator exactly. -/
294 theorem scalar_mul_separator
295     (certificate : EvaluatedBezoutCertificate F G U V r) :
296     r • separator r V G = separatorNumerator V G := by
297   exact scalar_mul_separator_of_ne_zero certificate.r_ne_zero
298 
299 /-- Lattice form of denominator clearing: preservation of `V` and `G` certifies preservation of
300 `rE`. -/
301 theorem scalar_mul_separator_preservesLattice_of_ne_zero
302     (r_ne_zero : r ≠ 0) {lattice : AddSubgroup M}
303     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
304     PreservesLattice (r • separator r V G) lattice := by
305   rw [scalar_mul_separator_of_ne_zero r_ne_zero]
306   exact separatorNumerator_preservesLattice hV hG
307 
308 /-- Lattice form of denominator clearing, as a wrapper around the minimal nonvanishing theorem. -/
309 theorem scalar_mul_separator_preservesLattice
310     (certificate : EvaluatedBezoutCertificate F G U V r) {lattice : AddSubgroup M}
311     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
312     PreservesLattice (r • separator r V G) lattice := by
313   exact scalar_mul_separator_preservesLattice_of_ne_zero certificate.r_ne_zero hV hG
314 
315 /-- If `r = uπ^s`, then clearing only the uniformizer power leaves the inverse unit factor:
316 `π^s E = u⁻¹ N`.  No lattice hypothesis is needed for this algebraic identity. -/
317 theorem pow_smul_separator_eq_unit_inv_smul_separatorNumerator_of_ne_zero
318     (r_ne_zero : r ≠ 0) {pi : K} {s : ℕ} (u : Kˣ)
319     (hr : (u : K) * pi ^ s = r) :
320     (pi ^ s) • separator r V G = (↑(u⁻¹) : K) • separatorNumerator V G := by
321   have hpow : pi ^ s ≠ 0 := by
322     intro h
323     apply r_ne_zero
324     rw [← hr, h, mul_zero]
325   rw [separator, smul_smul]
326   apply congrArg (fun a : K ↦ a • separatorNumerator V G)
327   rw [← hr]
328   field_simp [hpow]
329   exact u.mul_inv.symm
330 
331 /-- Certificate wrapper for unit-aware algebraic denominator clearing. -/
332 theorem pow_smul_separator_eq_unit_inv_smul_separatorNumerator
333     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ} (u : Kˣ)
334     (hr : (u : K) * pi ^ s = r) :
335     (pi ^ s) • separator r V G = (↑(u⁻¹) : K) • separatorNumerator V G := by
336   exact pow_smul_separator_eq_unit_inv_smul_separatorNumerator_of_ne_zero
337     certificate.r_ne_zero u hr
338 
339 /-- A finite certificate that `s` powers of `pi` clear a projector on a lattice. -/
340 def IsSeparationWeight (pi : K) (E : End (K := K) (M := M))
341     (lattice : AddSubgroup M) (s : ℕ) : Prop :=
342   PreservesLattice ((pi ^ s) • E) lattice
343 
344 /-- Clearing exponents are upward closed whenever the uniformizer scalar preserves the lattice. -/
345 theorem IsSeparationWeight.mono {pi : K} {E : End (K := K) (M := M)}
346     {lattice : AddSubgroup M} {s t : ℕ}
347     (hs : IsSeparationWeight pi E lattice s) (hst : s ≤ t)
348     (hpi : ScalarPreservesLattice pi lattice) :
349     IsSeparationWeight pi E lattice t := by
350   rw [IsSeparationWeight] at hs ⊢
351   have hpow : pi ^ t = pi ^ (t - s) * pi ^ s := by
352     rw [← pow_add, Nat.sub_add_cancel hst]
353   rw [hpow, mul_smul]
354   exact (hpi.pow (t - s)).smul hs
355 
356 /-- Existence of a finite separation weight is kept as explicit data. -/
357 structure FiniteSeparationWeight (pi : K) (E : End (K := K) (M := M))
358     (lattice : AddSubgroup M) where
359   weight : ℕ
360   clears : IsSeparationWeight pi E lattice weight
361 
362 /-- Propositional form of finiteness, used to define the actual least separation weight. -/
363 def HasFiniteSeparationWeight (pi : K) (E : End (K := K) (M := M))
364     (lattice : AddSubgroup M) : Prop :=
365   ∃ s : ℕ, IsSeparationWeight pi E lattice s
366 
367 /-- A bundled finite certificate supplies the corresponding existence proof. -/
368 theorem FiniteSeparationWeight.exists {pi : K} {E : End (K := K) (M := M)}
369     {lattice : AddSubgroup M} (certificate : FiniteSeparationWeight pi E lattice) :
370     HasFiniteSeparationWeight pi E lattice :=
371   ⟨certificate.weight, certificate.clears⟩
372 
373 /-- The actual separation weight: the least natural exponent which clears the projector on the
374 lattice.  Its existence proof is explicit and `Nat.find` performs only the well-ordering step. -/
375 noncomputable def separationWeight {pi : K} {E : End (K := K) (M := M)}
376     {lattice : AddSubgroup M} (finite : HasFiniteSeparationWeight pi E lattice) : ℕ :=
377   by
378     classical
379     exact Nat.find finite
380 
381 /-- The least separation weight really clears the projector. -/
382 theorem separationWeight_clears {pi : K} {E : End (K := K) (M := M)}
383     {lattice : AddSubgroup M} (finite : HasFiniteSeparationWeight pi E lattice) :
384     IsSeparationWeight pi E lattice (separationWeight finite) := by
385   classical
386   exact Nat.find_spec finite
387 
388 /-- Minimality, equivalently the abstract upper-bound rule: every supplied clearing exponent bounds
389 the actual separation weight from above. -/
390 theorem separationWeight_le_of_clears {pi : K} {E : End (K := K) (M := M)}
391     {lattice : AddSubgroup M} (finite : HasFiniteSeparationWeight pi E lattice)
392     {s : ℕ} (hs : IsSeparationWeight pi E lattice s) :
393     separationWeight finite ≤ s := by
394   classical
395   exact Nat.find_min' finite hs
396 
397 /-- A certified weight is, tautologically, a finite separation-weight certificate. -/
398 def finiteSeparationWeightOfCertificate {pi : K} {E : End (K := K) (M := M)}
399     {lattice : AddSubgroup M} {s : ℕ} (h : IsSeparationWeight pi E lattice s) :
400     FiniteSeparationWeight pi E lattice :=
401   ⟨s, h⟩
402 
403 /-- If the evaluated denominator is exactly `pi^s`, preservation of `V` and `G` supplies the
404 corresponding finite separation-weight certificate. -/
405 theorem separator_isSeparationWeight_of_pow_eq
406     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ}
407     {lattice : AddSubgroup M} (hr : pi ^ s = r)
408     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
409     IsSeparationWeight pi (separator r V G) lattice s := by
410   rw [IsSeparationWeight, hr]
411   exact scalar_mul_separator_preservesLattice certificate hV hG
412 
413 /-- Minimal unit-aware denominator clearing.  If `r = uπ^s`, only the action of the inverse
414 unit is needed to transfer preservation of the integral numerator to `π^s E`. -/
415 theorem separator_isSeparationWeight_of_unit_mul_pow_eq_of_inv_preserves
416     (r_ne_zero : r ≠ 0) {pi : K} {s : ℕ} {u : Kˣ}
417     {lattice : AddSubgroup M} (hr : (u : K) * pi ^ s = r)
418     (huInv : ScalarPreservesLattice (↑(u⁻¹) : K) lattice)
419     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
420     IsSeparationWeight pi (separator r V G) lattice s := by
421   rw [IsSeparationWeight,
422     pow_smul_separator_eq_unit_inv_smul_separatorNumerator_of_ne_zero r_ne_zero u hr]
423   exact huInv.smul (separatorNumerator_preservesLattice hV hG)
424 
425 /-- Bundled valuation-unit wrapper for unit-aware denominator clearing.  Both unit directions
426 are convenient lattice data, although this implication uses only `u⁻¹`. -/
427 theorem separator_isSeparationWeight_of_unit_mul_pow_eq_of_ne_zero
428     (r_ne_zero : r ≠ 0) {pi : K} {s : ℕ} {u : Kˣ}
429     {lattice : AddSubgroup M} (hr : (u : K) * pi ^ s = r)
430     (hu : IsLatticeUnit u lattice)
431     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
432     IsSeparationWeight pi (separator r V G) lattice s := by
433   exact separator_isSeparationWeight_of_unit_mul_pow_eq_of_inv_preserves
434     r_ne_zero hr hu.2 hV hG
435 
436 /-- Certificate wrapper for unit-aware separation-weight clearing. -/
437 theorem separator_isSeparationWeight_of_unit_mul_pow_eq
438     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ} {u : Kˣ}
439     {lattice : AddSubgroup M} (hr : (u : K) * pi ^ s = r)
440     (hu : IsLatticeUnit u lattice)
441     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
442     IsSeparationWeight pi (separator r V G) lattice s := by
443   exact separator_isSeparationWeight_of_unit_mul_pow_eq_of_ne_zero
444     certificate.r_ne_zero hr hu hV hG
445 
446 /-- The same unit-aware theorem in the conventional valuation orientation `r = uπ^s`. -/
447 theorem separator_isSeparationWeight_of_eq_unit_mul_pow
448     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ} {u : Kˣ}
449     {lattice : AddSubgroup M} (hr : r = (u : K) * pi ^ s)
450     (hu : IsLatticeUnit u lattice)
451     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
452     IsSeparationWeight pi (separator r V G) lattice s :=
453   separator_isSeparationWeight_of_unit_mul_pow_eq certificate hr.symm hu hV hG
454 
455 /-- Unit-aware denominator data supplies finiteness directly, without a redundant external
456 existence hypothesis. -/
457 theorem separator_hasFiniteSeparationWeight_of_unit_mul_pow_eq
458     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ} {u : Kˣ}
459     {lattice : AddSubgroup M} (hr : (u : K) * pi ^ s = r)
460     (hu : IsLatticeUnit u lattice)
461     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
462     HasFiniteSeparationWeight pi (separator r V G) lattice :=
463   ⟨s, separator_isSeparationWeight_of_unit_mul_pow_eq certificate hr hu hV hG⟩
464 
465 /-- Conventional-orientation finiteness theorem for `r = uπ^s`. -/
466 theorem separator_hasFiniteSeparationWeight_of_eq_unit_mul_pow
467     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ} {u : Kˣ}
468     {lattice : AddSubgroup M} (hr : r = (u : K) * pi ^ s)
469     (hu : IsLatticeUnit u lattice)
470     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
471     HasFiniteSeparationWeight pi (separator r V G) lattice :=
472   ⟨s, separator_isSeparationWeight_of_eq_unit_mul_pow certificate hr hu hV hG⟩
473 
474 /-- The canonical least weight obtained from unit-aware denominator data is at most its displayed
475 exponent. -/
476 theorem separator_separationWeight_le_of_unit_mul_pow_eq
477     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ} {u : Kˣ}
478     {lattice : AddSubgroup M} (hr : (u : K) * pi ^ s = r)
479     (hu : IsLatticeUnit u lattice)
480     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
481     separationWeight
482         (separator_hasFiniteSeparationWeight_of_unit_mul_pow_eq certificate hr hu hV hG) ≤ s := by
483   apply separationWeight_le_of_clears
484   exact separator_isSeparationWeight_of_unit_mul_pow_eq certificate hr hu hV hG
485 
486 /-- The canonical least separation weight associated to `r = uπ^s` is at most `s`. -/
487 theorem separator_separationWeight_le_of_eq_unit_mul_pow
488     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ} {u : Kˣ}
489     {lattice : AddSubgroup M} (hr : r = (u : K) * pi ^ s)
490     (hu : IsLatticeUnit u lattice)
491     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
492     separationWeight
493         (separator_hasFiniteSeparationWeight_of_eq_unit_mul_pow certificate hr hu hV hG) ≤ s := by
494   apply separationWeight_le_of_clears
495   exact separator_isSeparationWeight_of_eq_unit_mul_pow certificate hr hu hV hG
496 
497 /-- Consequently, any displayed denominator `pi^s = r` gives the manuscript's upper bound on the
498 actual minimal separation weight. -/
499 theorem separator_separationWeight_le_of_pow_eq
500     (certificate : EvaluatedBezoutCertificate F G U V r) {pi : K} {s : ℕ}
501     {lattice : AddSubgroup M}
502     (finite : HasFiniteSeparationWeight pi (separator r V G) lattice)
503     (hr : pi ^ s = r)
504     (hV : PreservesLattice V lattice) (hG : PreservesLattice G lattice) :
505     separationWeight finite ≤ s := by
506   apply separationWeight_le_of_clears finite
507   exact separator_isSeparationWeight_of_pow_eq certificate hr hV hG
508 
509 /-! ## Precision delay -/
510 
511 /-- Congruence modulo the scalar lattice `pi^n lattice`, expressed with an explicit witness. -/
512 def CongruentModLattice (pi : K) (lattice : AddSubgroup M) (n : ℕ) (x y : M) : Prop :=
513   ∃ z : M, z ∈ lattice ∧ x - y = (pi ^ n) • z
514 
515 /-- An `s`-digit denominator certificate turns `m+s` input digits into `m` output digits. -/
516 theorem projector_precision_delay {pi : K} {E : End (K := K) (M := M)}
517     {lattice : AddSubgroup M} {s m : ℕ}
518     (hweight : IsSeparationWeight pi E lattice s) {x y : M}
519     (hxy : CongruentModLattice pi lattice (m + s) x y) :
520     CongruentModLattice pi lattice m (E x) (E y) := by
521   rcases hxy with ⟨z, hz, hxy⟩
522   refine ⟨((pi ^ s) • E) z, hweight z hz, ?_⟩
523   rw [← map_sub, hxy, map_smul]
524   simp only [LinearMap.smul_apply, pow_add, smul_smul]
525 
526 end Komorebi.PaperII.ResultantSeparation

Back to source controls