PolynomialRootStability.lean

1 module
2 public import PolynomialPadicUnique
3 public import PolynomialCoefficientPerturbation
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialRootStability
10 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
11 open Komorebi.PolynomialPadicLift Komorebi.PolynomialPadicUnique
12 open Komorebi.PolynomialCoefficientPerturbation Komorebi.PolynomialSurjectiveStep
13 variable {d e : ℕ}
14 
15 /-- Two integer representatives of the same p-adic residue are congruent as integers. -/
16 theorem integer_congruent_of_common_padic (p n : ℕ) [Fact (Nat.Prime p)]
17     (a : ℤ_[p]) (x y : ℤ)
18     (hx : (p : ℤ_[p])^n ∣ a - (x : ℤ_[p]))
19     (hy : (p : ℤ_[p])^n ∣ a - (y : ℤ_[p])) :
20     (p : ℤ)^n ∣ x - y := by
21   apply (int_pow_dvd_iff p n (x-y)).mpr
22   have h := dvd_sub hy hx
23   simpa only [sub_sub_sub_cancel_left, Int.cast_sub] using h
24 
25 /-- A smooth exact p-adic root has a nearby root after any sufficiently divisible
26 integer coefficient perturbation. The system may be rectangular. -/
27 theorem exists_nearby_perturbed_root (p M : ℕ) [Fact (Nat.Prime p)] (hM : 1 ≤ M)
28     (c : ℤ) (hc : (p : ℤ)^M ∣ c)
29     (F H : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
30     (hJ : Function.Surjective (digitJacobian p F x))
31     (a : Fin d → ℤ_[p]) (ha : ∀ i, padicEval p F a i = 0)
32     (hax : ∀ i, (p : ℤ_[p]) ∣ a i - (x i : ℤ_[p])) :
33     ∃ b : Fin d → ℤ_[p],
34       (∀ i, padicEval p (perturb c F H) b i = 0) ∧
35       (∀ i, (p : ℤ_[p])^M ∣ b i - a i) := by
36   let y := truncInt p M a
37   have hy : ∀ i, (p : ℤ)^M ∣ evalSystem F y i := truncInt_root p M F a ha
38   have hay : ∀ i, (p : ℤ_[p])^M ∣ a i - (y i : ℤ_[p]) :=
39     truncInt_precision p M a
40   have hyx : ∀ i, (p : ℤ) ∣ y i - x i := by
41     intro i
42     have hy1 : (p : ℤ_[p])^1 ∣ a i - (y i : ℤ_[p]) :=
43       (pow_dvd_pow (p : ℤ_[p]) hM).trans (hay i)
44     simpa only [pow_one] using integer_congruent_of_common_padic p 1 (a i) (y i) (x i)
45       hy1 (by simpa only [pow_one] using hax i)
46   have hJy : Function.Surjective (digitJacobian p F y) := by
47     rw [digitJacobian_eq p F x y hyx]
48     exact hJ
49   obtain ⟨b, hb, hby⟩ := exists_padic_root_perturb p M hM c hc F H y hy hJy
50   refine ⟨b, hb, ?_⟩
51   intro i
52   have h := dvd_sub (hby i) (hay i)
53   simpa only [sub_sub_sub_cancel_right] using h
54 
55 /-- In a smooth square residue ball, every selected root of F+cH agrees with
56 the original root to the full coefficient-perturbation precision. -/
57 theorem perturbed_roots_congruent (p L M : ℕ) [Fact (Nat.Prime p)]
58     (hL : 1 ≤ L) (hLM : L ≤ M) (c : ℤ) (hc : (p : ℤ)^M ∣ c)
59     (F H : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
60     (hJ : Function.Surjective (digitJacobian p F x))
61     (a b : Fin d → ℤ_[p])
62     (ha : ∀ i, padicEval p F a i = 0)
63     (hb : ∀ i, padicEval p (perturb c F H) b i = 0)
64     (hax : ∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p]))
65     (hbx : ∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) :
66     ∀ i, (p : ℤ_[p])^M ∣ b i - a i := by
67   have hM : 1 ≤ M := hL.trans hLM
68   have hax1 : ∀ i, (p : ℤ_[p]) ∣ a i - (x i : ℤ_[p]) := by
69     intro i
70     exact (dvd_pow_self (p : ℤ_[p]) (by omega : L ≠ 0)).trans (hax i)
71   obtain ⟨b', hb', hb'a⟩ := exists_nearby_perturbed_root p M hM c hc F H x hJ a ha hax1
72   have hb'x : ∀ i, (p : ℤ_[p])^L ∣ b' i - (x i : ℤ_[p]) := by
73     intro i
74     have h := dvd_add ((pow_dvd_pow (p : ℤ_[p]) hLM).trans (hb'a i)) (hax i)
75     simpa only [sub_add_sub_cancel] using h
76   have hp : (p : ℤ) ∣ c := (dvd_pow_self (p : ℤ) (by omega : M ≠ 0)).trans hc
77   have hJG : Function.Surjective (digitJacobian p (perturb c F H) x) := by
78     rw [digitJacobian_perturb_eq p c hp F H x]
79     exact hJ
80   have heq := padic_root_unique p L hL (perturb c F H) x hJG b b' hb hb' hbx hb'x
81   simpa only [heq] using hb'a
82 
83 /-- The perturbed square root exists uniquely in the original residue ball,
84 and retains the entire coefficient-perturbation precision around the original root. -/
85 theorem exists_unique_nearby_perturbed_root (p L M : ℕ) [Fact (Nat.Prime p)]
86     (hL : 1 ≤ L) (hLM : L ≤ M) (c : ℤ) (hc : (p : ℤ)^M ∣ c)
87     (F H : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
88     (hJ : Function.Surjective (digitJacobian p F x))
89     (a : Fin d → ℤ_[p]) (ha : ∀ i, padicEval p F a i = 0)
90     (hax : ∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) :
91     ∃! b : Fin d → ℤ_[p],
92       (∀ i, padicEval p (perturb c F H) b i = 0) ∧
93       (∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) ∧
94       (∀ i, (p : ℤ_[p])^M ∣ b i - a i) := by
95   have hax1 : ∀ i, (p : ℤ_[p]) ∣ a i - (x i : ℤ_[p]) := by
96     intro i
97     exact (dvd_pow_self (p : ℤ_[p]) (by omega : L ≠ 0)).trans (hax i)
98   obtain ⟨b, hb, hba⟩ := exists_nearby_perturbed_root p M (hL.trans hLM) c hc
99     F H x hJ a ha hax1
100   have hbx : ∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p]) := by
101     intro i
102     have h := dvd_add ((pow_dvd_pow (p : ℤ_[p]) hLM).trans (hba i)) (hax i)
103     simpa only [sub_add_sub_cancel] using h
104   refine ⟨b, ⟨hb, hbx, hba⟩, ?_⟩
105   intro b' hb'
106   have hp : (p : ℤ) ∣ c := (dvd_pow_self (p : ℤ) (by omega : M ≠ 0)).trans hc
107   have hJG : Function.Surjective (digitJacobian p (perturb c F H) x) := by
108     rw [digitJacobian_perturb_eq p c hp F H x]
109     exact hJ
110   exact padic_root_unique p L hL (perturb c F H) x hJG b' b hb'.1 hb hb'.2.1 hbx
111 
112 /-- Starting only with a lower square root, construct the original root and
113 the uniquely determined nearby perturbed root, including the full displacement bound. -/
114 theorem exists_root_and_unique_perturbation (p L M : ℕ) [Fact (Nat.Prime p)]
115     (hL : 1 ≤ L) (hLM : L ≤ M) (c : ℤ) (hc : (p : ℤ)^M ∣ c)
116     (F H : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
117     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
118     (hJ : Function.Surjective (digitJacobian p F x)) :
119     ∃ a : Fin d → ℤ_[p],
120       (∀ i, padicEval p F a i = 0) ∧
121       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) ∧
122       ∃! b : Fin d → ℤ_[p],
123         (∀ i, padicEval p (perturb c F H) b i = 0) ∧
124         (∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) ∧
125         (∀ i, (p : ℤ_[p])^M ∣ b i - a i) := by
126   obtain ⟨a, ha, hax⟩ := exists_padic_root p L hL F x hx hJ
127   exact ⟨a, ha, hax, exists_unique_nearby_perturbed_root p L M hL hLM c hc F H x hJ a ha hax⟩
128 
129 end Komorebi.PolynomialRootStability

Back to source controls