PolynomialControls.lean

1 module
2 
3 public import PolynomialObstruction
4 public import Mathlib.Tactic
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialControls
11 
12 open MvPolynomial PolynomialObstruction
13 
14 def squarePolynomial : MvPolynomial (Fin 1) ℤ := X 0 ^ 2
15 
16 /-- The first-order remainder can survive modulo the next base at depth zero. -/
17 theorem zero_depth_taylor_failure :
18     ¬ (2 : ℤ) ∣
19       eval (fun _ : Fin 1 => (1 : ℤ)) squarePolynomial -
20         eval (fun _ : Fin 1 => (0 : ℤ)) squarePolynomial -
21         PolynomialTaylor.directional squarePolynomial (fun _ => 0) (fun _ => 1) := by
22   norm_num [squarePolynomial, PolynomialTaylor.directional, pderiv_pow]
23 
24 def squareMinusTwo : Fin 1 → MvPolynomial (Fin 1) ℤ :=
25   fun _ => X 0 ^ 2 - C 2
26 
27 theorem even_square_cannot_be_two_mod_four (y : ℤ) (hy : (2 : ℤ) ∣ y) :
28     ¬ (4 : ℤ) ∣ y ^ 2 - 2 := by
29   obtain ⟨t, rfl⟩ := hy
30   intro h
31   have hs : (4 : ℤ) ∣ (2 * t) ^ 2 := ⟨t ^ 2, by ring⟩
32   have htwo : (4 : ℤ) ∣ 2 := by
33     simpa using dvd_sub hs h
34   norm_num at htwo
35 
36 /-- A singular lower root can have a nonzero one-step obstruction. -/
37 theorem singular_root_without_lift :
38     (∀ i, (2 : ℤ) ∣ evalSystem squareMinusTwo (fun _ => 0) i) ∧
39     jacobian squareMinusTwo (fun _ => 0) = 0 ∧
40     ¬ (∃ y : Fin 1 → ℤ,
41       (∀ i, (2 : ℤ) ∣ y i) ∧
42       (∀ i, (4 : ℤ) ∣ evalSystem squareMinusTwo y i)) := by
43   refine ⟨?_, ?_, ?_⟩
44   · intro i
45     simp only [evalSystem, squareMinusTwo, map_sub, map_pow, eval_X, eval_C]
46     norm_num
47   · apply LinearMap.ext
48     intro t
49     ext i
50     change (∑ k, eval (fun _ : Fin 1 => (0 : ℤ)) (pderiv k (squareMinusTwo i)) * t k) = 0
51     simp only [squareMinusTwo, map_sub, pderiv_pow, pderiv_C, map_mul, map_pow, eval_X]
52     simp
53   · rintro ⟨y, hy, hF⟩
54     have heven : (2 : ℤ) ∣ y 0 := by simpa using hy 0
55     have hfour : (4 : ℤ) ∣ y 0 ^ 2 - 2 := by
56       simpa [evalSystem, squareMinusTwo] using hF 0
57     exact even_square_cannot_be_two_mod_four (y 0) heven hfour
58 
59 def linearZero : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => X 0
60 def linearTwo : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => X 0 - C 2
61 
62 /-- Each equation lifts the same lower residue separately. -/
63 theorem separate_polynomial_lifts :
64     (∃ y : Fin 1 → ℤ,
65       (∀ i, (2 : ℤ) ∣ y i) ∧
66       (∀ i, (4 : ℤ) ∣ evalSystem linearZero y i)) ∧
67     (∃ y : Fin 1 → ℤ,
68       (∀ i, (2 : ℤ) ∣ y i) ∧
69       (∀ i, (4 : ℤ) ∣ evalSystem linearTwo y i)) := by
70   constructor
71   · refine ⟨fun _ => 0, ?_, ?_⟩ <;> intro i <;> norm_num [evalSystem, linearZero]
72   · refine ⟨fun _ => 2, ?_, ?_⟩ <;> intro i <;> norm_num [evalSystem, linearTwo]
73 
74 /-- Those separate lifts have no common next-level representative. -/
75 theorem no_common_polynomial_lift :
76     ¬ (∃ y : Fin 1 → ℤ,
77       (∀ i, (2 : ℤ) ∣ y i) ∧
78       (∀ i, (4 : ℤ) ∣ evalSystem linearZero y i) ∧
79       (∀ i, (4 : ℤ) ∣ evalSystem linearTwo y i)) := by
80   rintro ⟨y, _, hF, hG⟩
81   have hzero : (4 : ℤ) ∣ y 0 := by simpa [evalSystem, linearZero] using hF 0
82   have htwo : (4 : ℤ) ∣ y 0 - 2 := by simpa [evalSystem, linearTwo] using hG 0
83   have hbad : (4 : ℤ) ∣ 2 := by
84     simpa using dvd_sub hzero htwo
85   norm_num at hbad
86 
87 end Komorebi.PolynomialControls

Back to source controls