PolynomialTowerControls.lean

1 module
2 public import PolynomialIntegerTower
3 public import PadicTowerLimit
4 public import Mathlib.Tactic
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 namespace Komorebi.PolynomialTowerControls
10 open MvPolynomial PolynomialObstruction PolynomialDigitBridge
11 
12 def squareMinusFive : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => X 0 ^ 2 - C 5
13 
14 /-- The singular lower root one already lifts from modulus two to modulus four. -/
15 theorem square_minus_five_lower_steps :
16     (2 : ℤ) ∣ eval (fun _ : Fin 1 => 1) (squareMinusFive 0) ∧
17     (4 : ℤ) ∣ eval (fun _ : Fin 1 => 1) (squareMinusFive 0) := by
18   norm_num [squareMinusFive]
19 
20 /-- The very next level is impossible, even without a prescribed lower residue. -/
21 theorem square_minus_five_no_mod_eight (x : ℤ) : ¬ (8 : ℤ) ∣ x ^ 2 - 5 := by
22   intro h
23   have hz : ((x : ZMod 8) ^ 2 - 5) = 0 := by
24     simpa using (ZMod.intCast_zmod_eq_zero_iff_dvd (x ^ 2 - 5) 8).mpr h
25   have hn : ∀ t : ZMod 8, t ^ 2 - 5 ≠ 0 := by decide
26   exact hn (x : ZMod 8) hz
27 
28 /-- One successful singular lift does not furnish roots through all levels. -/
29 theorem square_minus_five_no_tower :
30     ¬ ∃ z : ℕ → Fin 1 → ℤ,
31       ∀ n i, (2 : ℤ) ^ (1+n) ∣ eval (z n) (squareMinusFive i) := by
32   rintro ⟨z, hz⟩
33   have h := hz 2 0
34   norm_num [squareMinusFive] at h
35   exact square_minus_five_no_mod_eight (z 2 0) h
36 
37 def projectionSystem : Fin 1 → MvPolynomial (Fin 2) ℤ := fun _ => X 0
38 
39 /-- A rectangular Jacobian can be surjective while leaving a free coordinate. -/
40 theorem projection_jacobian_surjective (q : ℕ) (x : Fin 2 → ℤ) :
41     Function.Surjective (digitJacobian q projectionSystem x) := by
42   intro y
43   refine ⟨fun _ => y 0, ?_⟩
44   ext i
45   simp [digitJacobian, projectionSystem, Fin.sum_univ_two, Fin.eq_zero i]
46 
47 /-- Surjectivity does not imply uniqueness: both roots have the same residue modulo two. -/
48 theorem projection_two_padic_roots :
49     ∃ a b : Fin 2 → ℤ_[2], a ≠ b ∧
50       (∀ i, eval₂ (Int.castRingHom ℤ_[2]) a (projectionSystem i) = 0) ∧
51       (∀ i, eval₂ (Int.castRingHom ℤ_[2]) b (projectionSystem i) = 0) ∧
52       (∀ i, (2 : ℤ_[2]) ∣ b i - a i) := by
53   let a : Fin 2 → ℤ_[2] := fun _ => 0
54   let b : Fin 2 → ℤ_[2] := ![0, 2]
55   refine ⟨a, b, ?_, ?_, ?_, ?_⟩
56   · intro h
57     have h1 := congrFun h 1
58     norm_num [a, b] at h1
59   · intro i
60     simp [a, projectionSystem]
61   · intro i
62     simp [b, projectionSystem]
63   · intro i
64     fin_cases i <;> simp [a, b]
65 
66 def linearMinusTwo : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => X 0 - C 2
67 
68 /-- A nonsingular lower root can require changing the very next binary digit. -/
69 theorem linear_shift_nonsingular_lower_root :
70     (2 : ℤ) ∣ eval (fun _ : Fin 1 => 0) (linearMinusTwo 0) ∧
71     Function.Surjective (digitJacobian 2 linearMinusTwo (fun _ => 0)) ∧
72     eval (fun _ : Fin 1 => 2) (linearMinusTwo 0) = 0 := by
73   refine ⟨?_, ?_, ?_⟩
74   · change (2 : ℤ) ∣ eval (fun _ : Fin 1 => 0) (X 0 - C 2)
75     simp only [map_sub, eval_X, eval_C]
76     norm_num
77   · intro y
78     refine ⟨y, ?_⟩
79     ext i
80     change (∑ k : Fin 1, (eval (fun _ : Fin 1 => (0 : ℤ))
81       (pderiv k (X 0 - C 2)) : ZMod 2) * y k) = y i
82     simp only [map_sub, pderiv_C, sub_zero,
83       Fin.sum_univ_one, pderiv_X_self, map_one, Int.cast_one, one_mul, Fin.eq_zero i]
84   · change eval (fun _ : Fin 1 => (2 : ℤ)) (X 0 - C 2) = 0
85     simp only [map_sub, eval_X, eval_C, sub_self]
86 
87 /-- The resulting exact integer root need not retain one extra digit of the initial point. -/
88 theorem linear_shift_no_extra_precision :
89     ¬ ∃ y : Fin 1 → ℤ,
90       eval y (linearMinusTwo 0) = 0 ∧ (4 : ℤ) ∣ y 0 := by
91   rintro ⟨y, hy, hd⟩
92   have h2 : y 0 = 2 := by
93     change eval y (X 0 - C 2) = 0 at hy
94     simpa only [map_sub, eval_X, eval_C, sub_eq_zero] using hy
95   rw [h2] at hd
96   norm_num at hd
97 
98 end Komorebi.PolynomialTowerControls

Back to source controls