PolynomialInverseCongruence.lean

1 module
2 public import PolynomialPadicUnique
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialInverseCongruence
9 open Komorebi.NativeAffine Komorebi.PolynomialObstruction
10 open Komorebi.PolynomialDigitBridge Komorebi.PolynomialPadicLift
11 open Komorebi.PolynomialPadicUnique Komorebi.PolynomialSurjectiveStep
12 variable {d e : ℕ}
13 
14 /-- The actual square Jacobian recovers one further input digit from an output digit.
15 The modulus may be any positive integer. -/
16 theorem integer_inverse_congruence_step (q n : ℕ) (hq : 0 < q) (hn : 1 ≤ n)
17     (F : Fin d → MvPolynomial (Fin d) ℤ) (a b : Fin d → ℤ)
18     (hJ : Function.Surjective (digitJacobian q F a))
19     (hab : ∀ i, (q : ℤ)^n ∣ b i - a i)
20     (hF : ∀ i, (q : ℤ)^(n+1) ∣ evalSystem F b i - evalSystem F a i) :
21     ∀ i, (q : ℤ)^(n+1) ∣ b i - a i := by
22   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
23   choose t ht using hab
24   have hb : b = fun i => a i + (q : ℤ)^n * t i := by
25     funext i
26     linarith [ht i]
27   have hdir : ∀ i, (q : ℤ) ∣ jacobian F a t i := by
28     intro i
29     have hrem := Komorebi.PolynomialTaylor.taylor_step_dvd (F i) a t q n hn
30     rw [← hb] at hrem
31     have hmul : (q : ℤ)^(n+1) ∣ (q : ℤ)^n * jacobian F a t i := by
32       convert dvd_sub (hF i) hrem using 1
33       · rfl
34       · dsimp [evalSystem, jacobian, Komorebi.PolynomialTaylor.directional]
35         ring
36     rwa [pow_succ, mul_dvd_mul_iff_left
37       (pow_ne_zero n (Int.natCast_ne_zero.mpr (Nat.ne_of_gt hq)))] at hmul
38   have hz : digitJacobian q F a (reduction q d t) = 0 := by
39     rw [reduction_jacobian, reduction_zero_iff]
40     exact hdir
41   have hinj : Function.Injective (digitJacobian q F a) :=
42     Finite.injective_iff_surjective.mpr hJ
43   have htzero : reduction q d t = 0 := hinj (hz.trans (map_zero _).symm)
44   have htdvd := (reduction_zero_iff q t).mp htzero
45   intro i
46   rw [ht i, pow_succ]
47   exact mul_dvd_mul_left ((q : ℤ)^n) (htdvd i)
48 
49 /-- A square smooth integer polynomial map reflects all congruence depths
50 inside a fixed residue class, also for positive composite moduli. -/
51 theorem integer_inverse_congruence (q N : ℕ) (hq : 0 < q)
52     (F : Fin d → MvPolynomial (Fin d) ℤ) (a b : Fin d → ℤ)
53     (hJ : Function.Surjective (digitJacobian q F a))
54     (hab : ∀ i, (q : ℤ) ∣ b i - a i)
55     (hF : ∀ i, (q : ℤ)^N ∣ evalSystem F b i - evalSystem F a i) :
56     ∀ i, (q : ℤ)^N ∣ b i - a i := by
57   induction N with
58   | zero => simp
59   | succ N ih =>
60     by_cases hN : N = 0
61     · simpa only [hN, zero_add, pow_one] using hab
62     · apply integer_inverse_congruence_step q N hq (by omega) F a b hJ
63       · apply ih
64         intro i
65         exact (pow_dvd_pow (q : ℤ) (Nat.le_succ N)).trans (hF i)
66       · exact hF
67 
68 /-- Actual p-adic polynomial evaluation preserves every coordinate congruence. -/
69 theorem padicEval_congruent (p N : ℕ) [Fact (Nat.Prime p)]
70     (F : Fin e → MvPolynomial (Fin d) ℤ) (a b : Fin d → ℤ_[p])
71     (hab : ∀ i, (p : ℤ_[p])^N ∣ a i - b i) :
72     ∀ i, (p : ℤ_[p])^N ∣ padicEval p F a i - padicEval p F b i := by
73   intro i
74   apply (toZModPow_eq_iff_dvd_sub p N _ _).mp
75   have ha := MvPolynomial.hom_eval₂ (F i) (Int.castRingHom ℤ_[p])
76     (PadicInt.toZModPow N) a
77   have hb := MvPolynomial.hom_eval₂ (F i) (Int.castRingHom ℤ_[p])
78     (PadicInt.toZModPow N) b
79   simp only [padicEval]
80   rw [ha, hb]
81   congr 1
82   funext k
83   exact (toZModPow_eq_iff_dvd_sub p N _ _).mpr (hab k)
84 
85 /-- A square polynomial map with surjective actual reduced Jacobian reflects
86 all p-adic congruence depths in the residue ball of the integer base point. -/
87 theorem padic_inverse_congruence (p N : ℕ) [Fact (Nat.Prime p)]
88     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
89     (hJ : Function.Surjective (digitJacobian p F x))
90     (a b : Fin d → ℤ_[p])
91     (hax : ∀ i, (p : ℤ_[p]) ∣ a i - (x i : ℤ_[p]))
92     (hbx : ∀ i, (p : ℤ_[p]) ∣ b i - (x i : ℤ_[p]))
93     (hF : ∀ i, (p : ℤ_[p])^N ∣ padicEval p F a i - padicEval p F b i) :
94     ∀ i, (p : ℤ_[p])^N ∣ a i - b i := by
95   let y := truncInt p (N+1) a
96   let z := truncInt p (N+1) b
97   have hay : ∀ i, (p : ℤ_[p])^N ∣ a i - (y i : ℤ_[p]) := by
98     intro i
99     exact (pow_dvd_pow (p : ℤ_[p]) (Nat.le_succ N)).trans
100       (truncInt_precision p (N+1) a i)
101   have hbz : ∀ i, (p : ℤ_[p])^N ∣ b i - (z i : ℤ_[p]) := by
102     intro i
103     exact (pow_dvd_pow (p : ℤ_[p]) (Nat.le_succ N)).trans
104       (truncInt_precision p (N+1) b i)
105   have hyx : ∀ i, (p : ℤ) ∣ y i - x i := by
106     intro i
107     have hy1 : (p : ℤ_[p]) ∣ a i - (y i : ℤ_[p]) :=
108       (dvd_pow_self (p : ℤ_[p]) (Nat.succ_ne_zero N)).trans
109         (truncInt_precision p (N+1) a i)
110     have hcast : (p : ℤ_[p])^1 ∣ ((y i - x i : ℤ) : ℤ_[p]) := by
111       simpa only [pow_one, Int.cast_sub, sub_sub_sub_cancel_left] using dvd_sub (hax i) hy1
112     simpa only [pow_one] using (int_pow_dvd_iff p 1 (y i-x i)).mpr hcast
113   have hzx : ∀ i, (p : ℤ) ∣ z i - x i := by
114     intro i
115     have hz1 : (p : ℤ_[p]) ∣ b i - (z i : ℤ_[p]) :=
116       (dvd_pow_self (p : ℤ_[p]) (Nat.succ_ne_zero N)).trans
117         (truncInt_precision p (N+1) b i)
118     have hcast : (p : ℤ_[p])^1 ∣ ((z i - x i : ℤ) : ℤ_[p]) := by
119       simpa only [pow_one, Int.cast_sub, sub_sub_sub_cancel_left] using dvd_sub (hbx i) hz1
120     simpa only [pow_one] using (int_pow_dvd_iff p 1 (z i-x i)).mpr hcast
121   have hJy : Function.Surjective (digitJacobian p F y) := by
122     rw [digitJacobian_eq p F x y hyx]
123     exact hJ
124   have hzy : ∀ i, (p : ℤ) ∣ z i - y i := by
125     intro i
126     simpa only [sub_sub_sub_cancel_right] using dvd_sub (hzx i) (hyx i)
127   have hFy := padicEval_congruent p N F a (fun i => (y i : ℤ_[p])) hay
128   have hFz := padicEval_congruent p N F b (fun i => (z i : ℤ_[p])) hbz
129   have hFzy : ∀ i, (p : ℤ)^N ∣ evalSystem F z i - evalSystem F y i := by
130     intro i
131     apply (int_pow_dvd_iff p N _).mpr
132     have h := dvd_sub (dvd_sub (hFy i) (hFz i)) (hF i)
133     rw [padicEval_intCast, padicEval_intCast] at h
134     convert h using 1
135     push_cast
136     ring
137   have hzyN := integer_inverse_congruence p N (Fact.out : Nat.Prime p).pos F y z hJy hzy hFzy
138   intro i
139   have hyz : (p : ℤ_[p])^N ∣ (y i : ℤ_[p]) - (z i : ℤ_[p]) := by
140     have h := (int_pow_dvd_iff p N _).mp (hzyN i)
141     simpa only [Int.cast_sub, neg_sub] using dvd_neg.mpr h
142   have h := dvd_add (dvd_sub (hay i) (hbz i)) hyz
143   convert h using 1
144   ring
145 
146 /-- On a smooth square residue ball the input and output have exactly the
147 same congruences at every precision. -/
148 theorem padic_congruence_iff (p N : ℕ) [Fact (Nat.Prime p)]
149     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
150     (hJ : Function.Surjective (digitJacobian p F x))
151     (a b : Fin d → ℤ_[p])
152     (hax : ∀ i, (p : ℤ_[p]) ∣ a i - (x i : ℤ_[p]))
153     (hbx : ∀ i, (p : ℤ_[p]) ∣ b i - (x i : ℤ_[p])) :
154     (∀ i, (p : ℤ_[p])^N ∣ padicEval p F a i - padicEval p F b i) ↔
155       (∀ i, (p : ℤ_[p])^N ∣ a i - b i) :=
156   ⟨padic_inverse_congruence p N F x hJ a b hax hbx, padicEval_congruent p N F a b⟩
157 
158 /-- The actual polynomial map is injective on its smooth square residue ball. -/
159 theorem padic_map_injective (p : ℕ) [Fact (Nat.Prime p)]
160     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
161     (hJ : Function.Surjective (digitJacobian p F x))
162     (a b : Fin d → ℤ_[p])
163     (hax : ∀ i, (p : ℤ_[p]) ∣ a i - (x i : ℤ_[p]))
164     (hbx : ∀ i, (p : ℤ_[p]) ∣ b i - (x i : ℤ_[p]))
165     (hF : padicEval p F a = padicEval p F b) : a = b := by
166   funext i
167   apply PadicInt.ext_of_toZModPow.mp
168   intro N
169   apply (toZModPow_eq_iff_dvd_sub p N _ _).mpr
170   exact padic_inverse_congruence p N F x hJ a b hax hbx (by simp only [hF, sub_self, dvd_zero, implies_true]) i
171 
172 #print axioms integer_inverse_congruence_step
173 #print axioms integer_inverse_congruence
174 #print axioms padicEval_congruent
175 #print axioms padic_inverse_congruence
176 #print axioms padic_congruence_iff
177 #print axioms padic_map_injective
178 
179 end Komorebi.PolynomialInverseCongruence

Back to source controls