PolynomialMotionControls.lean

1 module
2 public import PolynomialWeightedControls
3 public import PolynomialRootMotion
4 public import Mathlib.Tactic
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialMotionControls
11 open MvPolynomial Komorebi.PolynomialPadicUnique
12 
13 /-- A unit-Jacobian example attaining the first-order error bound. -/
14 def sharpQuadratic : MvPolynomial (Fin 1) ℤ_[2] := X 0 + X 0 ^ 2
15 
16 /-- The unperturbed system has an exact root and unit derivative at zero. -/
17 theorem sharpQuadratic_base :
18     eval (0 : Fin 1 → ℤ_[2]) sharpQuadratic = 0 ∧
19     eval (0 : Fin 1 → ℤ_[2]) (pderiv 0 sharpQuadratic) = 1 := by
20   norm_num [sharpQuadratic]
21 
22 /-- Exhaustive finite verification of the residue class of every even root. -/
23 theorem sharp_mod_eight (x : ZMod 8) (hx : x + x ^ 2 + 2 = 0)
24     (heven : ∃ y : ZMod 8, x = 2 * y) : x + 2 = 4 := by
25   have h : ∀ z : ZMod 8, z + z ^ 2 + 2 = 0 →
26       (∃ y : ZMod 8, z = 2 * y) → z + 2 = 4 := by decide
27   exact h x hx heven
28 
29 /-- The first-order error is exactly depth two for any selected even root of
30 X + X² + 2. Existence is supplied by the main perturbation theorem. -/
31 theorem sharp_error_of_even_root (b : ℤ_[2]) (hb : (2 : ℤ_[2]) ∣ b)
32     (hroot : b + b ^ 2 + 2 = 0) :
33     (2 : ℤ_[2]) ^ 2 ∣ b + 2 ∧ ¬ (2 : ℤ_[2]) ^ 3 ∣ b + 2 := by
34   rcases hb with ⟨c, hc⟩
35   have herror : b + 2 = (2 : ℤ_[2]) ^ 2 * (-c ^ 2) := by
36     rw [hc] at hroot ⊢
37     linear_combination hroot
38   constructor
39   · exact ⟨-c ^ 2, herror⟩
40   · intro hdeep
41     have hzero : PadicInt.toZModPow 3 (b + 2) = 0 := by
42       have h := (toZModPow_eq_iff_dvd_sub 2 3 (b + 2) 0).mpr
43         (by simpa using hdeep)
44       simpa only [map_zero] using h
45     have hroot8 := congrArg (PadicInt.toZModPow 3) hroot
46     have hc8 := congrArg (PadicInt.toZModPow 3) hc
47     simp only [map_add, map_pow, map_ofNat, map_zero] at hroot8
48     simp only [map_mul, map_ofNat] at hc8
49     have hfour := sharp_mod_eight (PadicInt.toZModPow 3 b) hroot8
50       ⟨PadicInt.toZModPow 3 c, hc8⟩
51     simp only [map_add, map_ofNat] at hzero
52     rw [hfour] at hzero
53     exact (by decide : (4 : ZMod 8) ≠ 0) hzero
54 
55 /-- The sharpness example has an actual p-adic root, constructed by the same
56 main theorem being tested, and its first-order error has no extra digit. -/
57 theorem exists_sharp_motion_root :
58     ∃ b : ℤ_[2], b + b ^ 2 + 2 = 0 ∧ (2 : ℤ_[2]) ∣ b ∧
59       (2 : ℤ_[2]) ^ 2 ∣ b + 2 ∧ ¬ (2 : ℤ_[2]) ^ 3 ∣ b + 2 := by
60   have hJ : PolynomialWeightedInverse.jacobian
61       (fun _ : Fin 1 => sharpQuadratic) (0 : Fin 1 → ℤ_[2]) =
62       (1 : Matrix (Fin 1) (Fin 1) ℤ_[2]) := by
63     ext i j
64     fin_cases i
65     fin_cases j
66     norm_num [PolynomialWeightedInverse.jacobian, sharpQuadratic]
67   obtain ⟨b, hb, _, hball, _⟩ :=
68     PolynomialRootMotion.exists_perturbed_root_certificate 2 0 1 (by decide)
69       (fun _ : Fin 1 => sharpQuadratic) (fun _ => C 1) (0 : Fin 1 → ℤ_[2])
70       (1 : Matrix (Fin 1) (Fin 1) ℤ_[2])
71       (by simp [hJ]) (by simp [hJ]) (fun _ => sharpQuadratic_base.1)
72   have hroot : b 0 + b 0 ^ 2 + 2 = 0 := by
73     simpa [PolynomialMotionNormalization.perturbSystem, sharpQuadratic] using hb 0
74   have htwo : (2 : ℤ_[2]) ∣ b 0 := by simpa using hball 0
75   exact ⟨b 0, hroot, htwo, sharp_error_of_even_root (b 0) htwo hroot⟩
76 
77 /-- The universal claim of one additional error digit is false for actual roots. -/
78 theorem no_uniform_extra_error_digit :
79     ¬ ∀ b : ℤ_[2], b + b ^ 2 + 2 = 0 → (2 : ℤ_[2]) ∣ b →
80       (2 : ℤ_[2]) ^ 3 ∣ b + 2 := by
81   intro h
82   obtain ⟨b, hroot, heven, _, hnot⟩ := exists_sharp_motion_root
83   exact hnot (h b hroot heven)
84 
85 end Komorebi.PolynomialMotionControls

Back to source controls