PolynomialPrescribedPadicTower.lean

1 module
2 public import PolynomialPrescribedIntegerTower
3 public import PolynomialPrescribedTowerLimit
4 public import PolynomialPrescribedTowerUnique
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 open Filter Topology
11 
12 namespace Komorebi.PolynomialPrescribedPadicTower
13 
14 open Komorebi.PolynomialObstruction Komorebi.PolynomialPadicLift
15 open Komorebi.PolynomialPrescribedSystem Komorebi.PolynomialPrescribedLifts
16 open Komorebi.PolynomialParameterSystem (freePart)
17 
18 variable {m k e : ℕ}
19 
20 /-- Every supplied compatible parameter path admits an actual polynomial tower
21 and exact p-adic endpoint. The tower is constructed from initial solved-block
22 surjectivity; it is not an input. Every parameter digit remains admissible. -/
23 theorem exists_root_with_prescribed_path (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
24     (F : Fin e → MvPolynomial (Fin (m+k)) ℤ) (x : Fin (m+k) → ℤ)
25     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
26     (hJ : Function.Surjective (solvedJacobian p F x))
27     (t : ℕ → Fin k → ℤ) (ht0 : t 0 = freePart x)
28     (ht : ∀ n j, (p : ℤ)^(L+n) ∣ t (n+1) j - t n j)
29     (τ : Fin k → ℤ_[p])
30     (htlim : Tendsto (fun n i => (t n i : ℤ_[p])) atTop (𝓝 τ)) :
31     ∃ (z : ℕ → Fin (m+k) → ℤ) (b : Fin (m+k) → ℤ_[p]),
32       z 0 = x ∧
33       (∀ n, freePart (z n) = t n) ∧
34       (∀ n i, (p : ℤ)^(L+n) ∣ evalSystem F (z n) i) ∧
35       (∀ n i, (p : ℤ)^(L+n) ∣ (z (n+1) - z n) i) ∧
36       (∀ n, solvedJacobian p F (z n) = solvedJacobian p F x) ∧
37       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 b) ∧
38       (∀ i, padicEval p F b i = 0) ∧ freePart b = τ ∧
39       (∀ n i, (p : ℤ_[p])^(L+n) ∣ b i - (z n i : ℤ_[p])) ∧
40       (∀ n v, Nat.card (PrescribedLifts p (L+n) F (z n) v) = p^(m-e)) := by
41   obtain ⟨z, hz0, hfree, hroot, hstep, hfixed⟩ :=
42     PolynomialPrescribedIntegerTower.exists_prescribed_tower p L
43       (Fact.out : Nat.Prime p).pos hL F x hx hJ t ht0 ht
44   obtain ⟨b, hlim, hprecision, hb, hbτ⟩ :=
45     PolynomialPrescribedTowerLimit.prescribed_tower_limit p L F z t τ
46       hroot hstep hfree htlim
47   refine ⟨z, b, hz0, hfree, hroot, hstep, hfixed, hlim, hb, hbτ, hprecision, ?_⟩
48   intro n v
49   apply PolynomialPrescribedStep.prescribed_lift_card p (L+n) (by omega) F (z n)
50     (hroot n)
51   rw [hfixed n]
52   exact hJ
53 
54 /-- Any p-adic parameter in the initial residue ball has an exact root reached
55 by a compatible integer polynomial tower. No parameter path or solution tower
56 is assumed: both are constructed, with all precisions and per-digit counts. -/
57 theorem exists_prescribed_padic_root_with_tower (p L : ℕ) [Fact (Nat.Prime p)]
58     (hL : 1 ≤ L) (F : Fin e → MvPolynomial (Fin (m+k)) ℤ)
59     (x : Fin (m+k) → ℤ) (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
60     (hJ : Function.Surjective (solvedJacobian p F x))
61     (τ : Fin k → ℤ_[p])
62     (hτ : ∀ j, (p : ℤ_[p])^L ∣ τ j - ((freePart x j : ℤ) : ℤ_[p])) :
63     ∃ (z : ℕ → Fin (m+k) → ℤ) (b : Fin (m+k) → ℤ_[p]),
64       z 0 = x ∧
65       (∀ n i, (p : ℤ)^(L+n) ∣ evalSystem F (z n) i) ∧
66       (∀ n i, (p : ℤ)^(L+n) ∣ (z (n+1) - z n) i) ∧
67       (∀ n, solvedJacobian p F (z n) = solvedJacobian p F x) ∧
68       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 b) ∧
69       (∀ i, padicEval p F b i = 0) ∧ freePart b = τ ∧
70       (∀ n i, (p : ℤ_[p])^(L+n) ∣ b i - (z n i : ℤ_[p])) ∧
71       (∀ n v, Nat.card (PrescribedLifts p (L+n) F (z n) v) = p^(m-e)) := by
72   obtain ⟨t, ht0, ht, _, htlim⟩ :=
73     PolynomialParameterPath.exists_parameter_path p L (freePart x) τ hτ
74   obtain ⟨z, b, hz0, _, hroot, hstep, hfixed, hlim, hb, hbτ, hprecision, hcard⟩ :=
75     exists_root_with_prescribed_path p L hL F x hx hJ t ht0 ht τ htlim
76   exact ⟨z, b, hz0, hroot, hstep, hfixed, hlim, hb, hbτ, hprecision, hcard⟩
77 
78 /-- Root existence with prescribed arbitrary p-adic parameters, retaining the
79 initial residue class, follows from the actual tower construction. -/
80 theorem exists_prescribed_padic_root (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
81     (F : Fin e → MvPolynomial (Fin (m+k)) ℤ) (x : Fin (m+k) → ℤ)
82     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
83     (hJ : Function.Surjective (solvedJacobian p F x))
84     (τ : Fin k → ℤ_[p])
85     (hτ : ∀ j, (p : ℤ_[p])^L ∣ τ j - ((freePart x j : ℤ) : ℤ_[p])) :
86     ∃ b : Fin (m+k) → ℤ_[p],
87       (∀ i, padicEval p F b i = 0) ∧ freePart b = τ ∧
88       (∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) := by
89   obtain ⟨z, b, hz0, _, _, _, _, hb, hbτ, hprecision, _⟩ :=
90     exists_prescribed_padic_root_with_tower p L hL F x hx hJ τ hτ
91   refine ⟨b, hb, hbτ, ?_⟩
92   simpa only [Nat.add_zero, hz0] using hprecision 0
93 
94 /-- In the square solved case, every prescribed p-adic parameter has exactly
95 one root in the original ball, independent of all lifting choices. -/
96 theorem exists_unique_prescribed_padic_root (p L : ℕ) [Fact (Nat.Prime p)]
97     (hL : 1 ≤ L) (F : Fin e → MvPolynomial (Fin (e+k)) ℤ)
98     (x : Fin (e+k) → ℤ) (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
99     (hJ : Function.Surjective (solvedJacobian p F x))
100     (τ : Fin k → ℤ_[p])
101     (hτ : ∀ j, (p : ℤ_[p])^L ∣ τ j - ((freePart x j : ℤ) : ℤ_[p])) :
102     ∃! b : Fin (e+k) → ℤ_[p],
103       (∀ i, padicEval p F b i = 0) ∧ freePart b = τ ∧
104       (∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) := by
105   obtain ⟨b, hb, hbτ, hbx⟩ := exists_prescribed_padic_root p L hL F x hx hJ τ hτ
106   refine ⟨b, ⟨hb, hbτ, hbx⟩, ?_⟩
107   intro c hc
108   exact PolynomialPrescribedTowerUnique.prescribed_root_unique p L hL F x hx hJ
109     c b hc.1 hb hc.2.2 hbx (hc.2.1.trans hbτ.symm)
110 
111 end Komorebi.PolynomialPrescribedPadicTower

Back to source controls