PolynomialParameterTowerContracts.lean

1 module
2 public import PolynomialPrescribedIntegerTower
3 public import PolynomialParameterPath
4 public import PolynomialPrescribedTowerUnique
5 public import PolynomialPrescribedContract
6 public import PolynomialPrescribedPadicTower
7 
8 @[expose] public section
9 noncomputable section
10 set_option autoImplicit false
11 open scoped BigOperators
12 open Filter Topology
13 
14 namespace Komorebi.PolynomialParameterTowerContracts
15 open MvPolynomial
16 variable {m k e : ℕ}
17 
18 /-- The expanded contract quantifies over every compatible exact integer parameter path.
19 Surjectivity is imposed only at the initial point, on the actual solved derivative columns. -/
20 theorem actual_integer_path_tower (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
21     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
22     (hx : ∀ i, (q : ℤ)^L ∣ eval x (F i))
23     (hJ : ∀ r : Fin e → ZMod q, ∃ u : Fin m → ZMod q,
24       ∀ i, ∑ j, (eval x (pderiv (Fin.castAdd k j) (F i)) : ZMod q) * u j = r i)
25     (t : ℕ → Fin k → ℤ) (ht0 : ∀ j, t 0 j = x (Fin.natAdd m j))
26     (ht : ∀ n j, (q : ℤ)^(L+n) ∣ t (n+1) j - t n j) :
27     ∃ z : ℕ → Fin (m + k) → ℤ,
28       z 0 = x ∧
29       (∀ n j, z n (Fin.natAdd m j) = t n j) ∧
30       (∀ n i, (q : ℤ)^(L+n) ∣ eval (z n) (F i)) ∧
31       (∀ n i, (q : ℤ)^(L+n) ∣ z (n+1) i - z n i) ∧
32       (∀ n, PolynomialPrescribedContract.actualSolvedMap q F (z n) =
33         PolynomialPrescribedContract.actualSolvedMap q F x) := by
34   have hs : Function.Surjective (PolynomialPrescribedSystem.solvedJacobian q F x) := by
35     intro r
36     obtain ⟨u, hu⟩ := hJ r
37     exact ⟨u, funext hu⟩
38   obtain ⟨z, hz0, hfree, hroot, hstep, hfixed⟩ :=
39     PolynomialPrescribedIntegerTower.exists_prescribed_tower q L hq hL F x hx hs t
40       (funext ht0) ht
41   exact ⟨z, hz0, fun n j => congrFun (hfree n) j, hroot, hstep, hfixed⟩
42 
43 /-- No approximation path is assumed: every p-adic target in the initial ball
44 has a compatible integer path with exact initial value and all requested precisions. -/
45 theorem arbitrary_padic_parameter_path (p L : ℕ) [Fact (Nat.Prime p)]
46     (x : Fin k → ℤ) (τ : Fin k → ℤ_[p])
47     (hτ : ∀ j, (p : ℤ_[p])^L ∣ τ j - (x j : ℤ_[p])) :
48     ∃ t : ℕ → Fin k → ℤ,
49       t 0 = x ∧
50       (∀ n j, (p : ℤ)^(L+n) ∣ t (n+1) j - t n j) ∧
51       (∀ n j, (p : ℤ_[p])^(L+n) ∣ τ j - (t n j : ℤ_[p])) ∧
52       Tendsto (fun n j => (t n j : ℤ_[p])) atTop (𝓝 τ) := by
53   exact PolynomialParameterPath.exists_parameter_path p L x τ hτ
54 
55 /-- With e solved variables for e equations, equal prescribed parameters force
56 uniqueness throughout the initial ball. All polynomial evaluations are explicit. -/
57 theorem actual_square_parameter_uniqueness (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
58     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ) (x : Fin (e + k) → ℤ)
59     (hx : ∀ i, (p : ℤ)^L ∣ eval x (F i))
60     (hJ : ∀ r : Fin e → ZMod p, ∃ u : Fin e → ZMod p,
61       ∀ i, ∑ j, (eval x (pderiv (Fin.castAdd k j) (F i)) : ZMod p) * u j = r i)
62     (b c : Fin (e + k) → ℤ_[p])
63     (hb : ∀ i, eval₂ (Int.castRingHom ℤ_[p]) b (F i) = 0)
64     (hc : ∀ i, eval₂ (Int.castRingHom ℤ_[p]) c (F i) = 0)
65     (hbx : ∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p]))
66     (hcx : ∀ i, (p : ℤ_[p])^L ∣ c i - (x i : ℤ_[p]))
67     (ht : ∀ j, b (Fin.natAdd e j) = c (Fin.natAdd e j)) : b = c := by
68   have hs : Function.Surjective (PolynomialPrescribedSystem.solvedJacobian p F x) := by
69     intro r
70     obtain ⟨u, hu⟩ := hJ r
71     exact ⟨u, funext hu⟩
72   exact PolynomialPrescribedTowerUnique.prescribed_root_unique p L hL F x hx hs
73     b c hb hc hbx hcx (funext ht)
74 
75 /-- The final target is an actual polynomial root for every arbitrary p-adic
76 parameter in the initial ball, reached by a constructed compatible integer tower.
77 The branching count uses explicitly constrained residue vectors at every level. -/
78 theorem arbitrary_padic_target_tower (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
79     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
80     (hx : ∀ i, (p : ℤ)^L ∣ eval x (F i))
81     (hJ : ∀ r : Fin e → ZMod p, ∃ u : Fin m → ZMod p,
82       ∀ i, ∑ j, (eval x (pderiv (Fin.castAdd k j) (F i)) : ZMod p) * u j = r i)
83     (τ : Fin k → ℤ_[p])
84     (hτ : ∀ j, (p : ℤ_[p])^L ∣ τ j - (x (Fin.natAdd m j) : ℤ_[p])) :
85     ∃ (z : ℕ → Fin (m + k) → ℤ) (b : Fin (m + k) → ℤ_[p]),
86       z 0 = x ∧
87       (∀ n i, (p : ℤ)^(L+n) ∣ eval (z n) (F i)) ∧
88       (∀ n i, (p : ℤ)^(L+n) ∣ z (n+1) i - z n i) ∧
89       (∀ n, PolynomialPrescribedContract.actualSolvedMap p F (z n) =
90         PolynomialPrescribedContract.actualSolvedMap p F x) ∧
91       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 b) ∧
92       (∀ i, eval₂ (Int.castRingHom ℤ_[p]) b (F i) = 0) ∧
93       (∀ j, b (Fin.natAdd m j) = τ j) ∧
94       (∀ n i, (p : ℤ_[p])^(L+n) ∣ b i - (z n i : ℤ_[p])) ∧
95       (∀ n (v : Fin k → ZMod p),
96         Nat.card (PolynomialPrescribedContract.ActualResidues p (L+n) F (z n) v) =
97           p^(m-e)) := by
98   have hs : Function.Surjective (PolynomialPrescribedSystem.solvedJacobian p F x) := by
99     intro r
100     obtain ⟨u, hu⟩ := hJ r
101     exact ⟨u, funext hu⟩
102   obtain ⟨z, b, hz0, hroot, hstep, hfixed, hlim, hb, hfree, hprecision, hcard⟩ :=
103     PolynomialPrescribedPadicTower.exists_prescribed_padic_root_with_tower p L hL
104       F x hx hs τ hτ
105   refine ⟨z, b, hz0, hroot, hstep, hfixed, hlim, hb,
106     fun j => congrFun hfree j, hprecision, ?_⟩
107   intro n v
108   rw [Nat.card_congr (PolynomialPrescribedContract.actualResidueEquiv p (L+n) F (z n) v)]
109   exact hcard n v
110 
111 /-- The supplied-path version retains each prescribed integer parameter exactly;
112 it does not merely reach some root with the same p-adic parameter limit. -/
113 theorem supplied_path_actual_endpoint (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
114     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
115     (hx : ∀ i, (p : ℤ)^L ∣ eval x (F i))
116     (hJ : ∀ r : Fin e → ZMod p, ∃ u : Fin m → ZMod p,
117       ∀ i, ∑ j, (eval x (pderiv (Fin.castAdd k j) (F i)) : ZMod p) * u j = r i)
118     (t : ℕ → Fin k → ℤ) (ht0 : ∀ j, t 0 j = x (Fin.natAdd m j))
119     (ht : ∀ n j, (p : ℤ)^(L+n) ∣ t (n+1) j - t n j)
120     (τ : Fin k → ℤ_[p])
121     (htlim : Tendsto (fun n j => (t n j : ℤ_[p])) atTop (𝓝 τ)) :
122     ∃ (z : ℕ → Fin (m + k) → ℤ) (b : Fin (m + k) → ℤ_[p]),
123       z 0 = x ∧
124       (∀ n j, z n (Fin.natAdd m j) = t n j) ∧
125       (∀ n i, (p : ℤ)^(L+n) ∣ eval (z n) (F i)) ∧
126       (∀ n i, (p : ℤ)^(L+n) ∣ z (n+1) i - z n i) ∧
127       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 b) ∧
128       (∀ i, eval₂ (Int.castRingHom ℤ_[p]) b (F i) = 0) ∧
129       (∀ j, b (Fin.natAdd m j) = τ j) ∧
130       (∀ n i, (p : ℤ_[p])^(L+n) ∣ b i - (z n i : ℤ_[p])) := by
131   have hs : Function.Surjective (PolynomialPrescribedSystem.solvedJacobian p F x) := by
132     intro r
133     obtain ⟨u, hu⟩ := hJ r
134     exact ⟨u, funext hu⟩
135   obtain ⟨z, b, hz0, hfree, hroot, hstep, _, hlim, hb, hbτ, hprecision, _⟩ :=
136     PolynomialPrescribedPadicTower.exists_root_with_prescribed_path p L hL F x hx hs
137       t (funext ht0) ht τ htlim
138   exact ⟨z, b, hz0, fun n j => congrFun (hfree n) j, hroot, hstep, hlim,
139     hb, fun j => congrFun hbτ j, hprecision⟩
140 
141 end Komorebi.PolynomialParameterTowerContracts

Back to source controls