PolynomialPadicUniqueContract.lean

1 module
2 public import PolynomialPadicUnique
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.PolynomialPadicUniqueContract
8 
9 /-- Uniqueness concerns arbitrary actual roots in the ball, without a selected
10 integer lifting sequence or a hypothesis identifying either root with its limit. -/
11 theorem explicit_arbitrary_root_uniqueness (p L : ℕ) [Fact (Nat.Prime p)]
12     (hL : 1 ≤ L) {d : ℕ} (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
13     (hJ : Function.Surjective (fun t : Fin d → ZMod p => fun i : Fin d =>
14       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k))
15     (a b : Fin d → ℤ_[p])
16     (ha : ∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0)
17     (hb : ∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) b (F i) = 0)
18     (hax : ∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p]))
19     (hbx : ∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) : a = b := by
20   exact PolynomialPadicUnique.padic_root_unique p L hL F x hJ a b ha hb hax hbx
21 
22 /-- Starting from the original polynomial lower-root congruence and the actual
23 reduced square Jacobian, both existence and uniqueness are conclusions. -/
24 theorem explicit_unique_padic_root (p L : ℕ) [Fact (Nat.Prime p)]
25     (hL : 1 ≤ L) {d : ℕ} (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
26     (hx : ∀ i, (p : ℤ)^L ∣ MvPolynomial.eval x (F i))
27     (hJ : Function.Surjective (fun t : Fin d → ZMod p => fun i : Fin d =>
28       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k)) :
29     ∃! a : Fin d → ℤ_[p],
30       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0) ∧
31       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) := by
32   exact PolynomialPadicUnique.exists_unique_padic_root p L hL F x hx hJ
33 
34 end Komorebi.PolynomialPadicUniqueContract

Back to source controls