PolynomialDeformationControls.lean

1 module
2 public import PolynomialTowerControls
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.PolynomialDeformationControls
8 open MvPolynomial PolynomialDigitBridge
9 
10 def squareMinusOne : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => X 0 ^ 2 - C 1
11 
12 /-- At the root one the actual Jacobian of X²−1 is invertible modulo three. -/
13 theorem square_minus_one_jacobian_bijective :
14     Function.Bijective (digitJacobian 3 squareMinusOne (fun _ => 1)) := by
15   have hformula : ∀ t : Fin 1 → ZMod 3,
16       digitJacobian 3 squareMinusOne (fun _ => 1) t = fun i => 2 * t i := by
17     intro t
18     ext i
19     simp [digitJacobian, squareMinusOne, Fin.eq_zero i]
20   constructor
21   · intro u v h
22     funext i
23     have hi := congrFun h i
24     rw [hformula, hformula] at hi
25     exact mul_left_cancel₀ (by decide : (2 : ZMod 3) ≠ 0) hi
26   · intro y
27     refine ⟨fun i => 2 * y i, ?_⟩
28     rw [hformula]
29     funext i
30     calc
31       (2 : ZMod 3) * (2 * y i) = (2 * 2) * y i := (mul_assoc _ _ _).symm
32       _ = y i := by rw [show (2 : ZMod 3) * 2 = 1 by decide, one_mul]
33 
34 /-- Distinct exact roots persist outside the local residue ball, even when
35 the initial reduced Jacobian is invertible. The second root is not congruent to the first modulo three. -/
36 theorem square_minus_one_two_padic_roots :
37     ∃ a b : Fin 1 → ℤ_[3], a ≠ b ∧
38       (∀ i, eval₂ (Int.castRingHom ℤ_[3]) a (squareMinusOne i) = 0) ∧
39       (∀ i, eval₂ (Int.castRingHom ℤ_[3]) b (squareMinusOne i) = 0) ∧
40       ¬ (3 : ℤ_[3]) ∣ b 0 - a 0 := by
41   refine ⟨fun _ => 1, fun _ => -1, ?_, ?_, ?_, ?_⟩
42   · intro h
43     have := congrFun h 0
44     norm_num at this
45   · intro i
46     simp [squareMinusOne]
47   · intro i
48     simp [squareMinusOne]
49   · intro h
50     have heq : (-1 : ℤ_[3]) - 1 = ((-2 : ℤ) : ℤ_[3]) := by norm_num
51     have hd : (3 : ℤ_[3]) ^ 1 ∣ ((-2 : ℤ) : ℤ_[3]) := by
52       simpa only [pow_one, ← heq] using h
53     have hi := (PadicInt.pow_p_dvd_int_iff (p := 3) 1 (-2)).mp hd
54     norm_num at hi
55 
56 /-- Global uniqueness is false for a square polynomial with invertible initial Jacobian. -/
57 theorem square_minus_one_not_global_unique :
58     ¬ ∀ a b : Fin 1 → ℤ_[3],
59       (∀ i, eval₂ (Int.castRingHom ℤ_[3]) a (squareMinusOne i) = 0) →
60       (∀ i, eval₂ (Int.castRingHom ℤ_[3]) b (squareMinusOne i) = 0) → a = b := by
61   intro h
62   obtain ⟨a, b, hne, ha, hb, _⟩ := square_minus_one_two_padic_roots
63   exact hne (h a b ha hb)
64 
65 /-- The polynomial X−2 is exactly a perturbation of X by 2 times an integral polynomial. -/
66 theorem linear_shift_coefficient_perturbation (i : Fin 1) :
67     PolynomialTowerControls.linearMinusTwo i =
68       X 0 + C (2 : ℤ) * C (-1) := by
69   simp [PolynomialTowerControls.linearMinusTwo, sub_eq_add_neg]
70 
71 /-- An actual nonsingular dyadic perturbation has root displacement exactly two,
72 so coefficient precision two cannot be strengthened to displacement divisible by four. -/
73 theorem linear_shift_no_extra_padic_precision :
74     ¬ ∃ b : Fin 1 → ℤ_[2],
75       eval₂ (Int.castRingHom ℤ_[2]) b (PolynomialTowerControls.linearMinusTwo 0) = 0 ∧
76       (2 : ℤ_[2]) ^ 2 ∣ b 0 := by
77   rintro ⟨b, hb, hd⟩
78   have hroot : b 0 = 2 := by
79     simpa [PolynomialTowerControls.linearMinusTwo, sub_eq_zero] using hb
80   rw [hroot] at hd
81   have hi : (2 : ℤ) ^ 2 ∣ 2 := by
82     exact (PadicInt.pow_p_dvd_int_iff 2 2).mp hd
83   norm_num at hi
84 
85 end Komorebi.PolynomialDeformationControls

Back to source controls