PolynomialParameterControls.lean

1 module
2 public import PolynomialParameterSystem
3 public import Mathlib.NumberTheory.Padics.RingHoms
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 namespace Komorebi.PolynomialParameterControls
9 open MvPolynomial PolynomialDigitBridge PolynomialPadicLift PolynomialParameterSystem
10 
11 /-- A smooth equation for which the specified first coordinate cannot be solved. -/
12 def squareMinusParameter : Fin 1 → MvPolynomial (Fin (1+1)) ℤ :=
13   fun _ => X 0 ^ 2 - X 1
14 
15 theorem full_jacobian_surjective :
16     Function.Surjective (digitJacobian 2 squareMinusParameter (fun _ => 0)) := by
17   intro t
18   refine ⟨![0, -t 0], ?_⟩
19   ext i
20   simp [digitJacobian, squareMinusParameter, Fin.eq_zero i, Fin.sum_univ_two]
21 
22 theorem solved_jacobian_zero :
23     solvedJacobian 2 squareMinusParameter (fun _ => 0) = 0 := by
24   ext u i
25   simp [solvedJacobian, squareMinusParameter, Fin.eq_zero i]
26 
27 theorem solved_jacobian_not_surjective :
28     ¬ Function.Surjective (solvedJacobian 2 squareMinusParameter (fun _ => 0)) := by
29   rw [solved_jacobian_zero]
30   intro h
31   obtain ⟨u, hu⟩ := h (fun _ => 1)
32   have hi := congrFun hu 0
33   norm_num at hi
34 
35 /-- The proposed parameter is in the base residue ball modulo two. -/
36 theorem parameter_two_near_origin : (2 : ℤ_[2]) ∣ (2 : ℤ_[2]) - 0 := by simp
37 
38 /-- Prescribing the second coordinate to two has no root, already modulo four. -/
39 theorem no_root_at_parameter_two :
40     ¬ ∃ a : Fin (1+1) → ℤ_[2],
41       padicEval 2 squareMinusParameter a = 0 ∧ a 1 = 2 := by
42   rintro ⟨a, ha, ht⟩
43   have hsq : a 0 ^ 2 = (2 : ℤ_[2]) := by
44     have hi := congrFun ha 0
45     simpa [padicEval, squareMinusParameter, ht, sub_eq_zero] using hi
46   have hmod := congrArg (PadicInt.toZModPow 2) hsq
47   have hnot : ∀ r : ZMod (2^2), r^2 ≠ 2 := by decide
48   have htwo : (2 : ℤ_[2]) = 1 + 1 := by norm_num
49   rw [map_pow, htwo, map_add, map_one] at hmod
50   exact hnot _ (hmod.trans (by decide : (1 : ZMod (2^2)) + 1 = 2))
51 
52 end Komorebi.PolynomialParameterControls

Back to source controls