PolynomialJointMotionControls.lean

1 module
2 public import PolynomialMotionControls
3 public import PolynomialParameterSystem
4 public import PolynomialJointSystem
5 public import Mathlib.Tactic
6 
7 @[expose] public section
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.PolynomialJointMotionControls
12 open MvPolynomial PolynomialParameterSystem
13 
14 @[simp] theorem join_one_zero {R : Type*} (y t : Fin 1 → R) :
15     join y t (0 : Fin (1 + 1)) = y 0 := rfl
16 
17 @[simp] theorem join_one_one {R : Type*} (y t : Fin 1 → R) :
18     join y t (1 : Fin (1 + 1)) = t 0 := rfl
19 
20 /-- Both the solved coordinate and the prescribed parameter enter this equation. -/
21 def linearSystem : Fin 1 → MvPolynomial (Fin (1 + 1)) ℤ_[2] :=
22   fun _ => X (Fin.castAdd 1 0) + X (Fin.natAdd 1 0)
23 
24 /-- A nonzero coefficient perturbation, independent of the parameter shift. -/
25 def linearPerturbation : Fin 1 → MvPolynomial (Fin (1 + 1)) ℤ_[2] :=
26   fun _ => C 1
27 
28 /-- The exact base root and both derivative contributions are nontrivial as intended. -/
29 theorem linear_base_data :
30     eval (0 : Fin (1 + 1) → ℤ_[2]) (linearSystem 0) = 0 ∧
31     eval (0 : Fin (1 + 1) → ℤ_[2])
32       (pderiv (Fin.castAdd 1 0) (linearSystem 0)) = 1 ∧
33     eval (0 : Fin (1 + 1) → ℤ_[2])
34       (pderiv (Fin.natAdd 1 0) (linearSystem 0)) = 1 ∧
35     eval (0 : Fin (1 + 1) → ℤ_[2]) (linearPerturbation 0) = 1 := by
36   norm_num [linearSystem, linearPerturbation, pderiv_X, Pi.single_apply, Fin.ext_iff]
37 
38 /-- For p=2, M=1, v=1, the prescribed parameter is 2 and the solved root is -4. -/
39 theorem linear_joint_root :
40     eval (join (fun _ : Fin 1 => (-4 : ℤ_[2])) (fun _ : Fin 1 => (2 : ℤ_[2])))
41       (linearSystem 0 + C ((2 : ℤ_[2]) ^ 1) * linearPerturbation 0) = 0 ∧
42     freePart (join (fun _ : Fin 1 => (-4 : ℤ_[2])) (fun _ : Fin 1 => (2 : ℤ_[2]))) =
43       (fun _ : Fin 1 => (2 : ℤ_[2])) := by
44   constructor
45   · norm_num [linearSystem, linearPerturbation]
46   · exact freePart_join _ _
47 
48 /-- Every root with the prescribed parameter equals the displayed root. -/
49 theorem linear_joint_unique (y : Fin 1 → ℤ_[2])
50     (hy : ∀ i, eval (join y (fun _ : Fin 1 => (2 : ℤ_[2])))
51       (linearSystem i + C ((2 : ℤ_[2]) ^ 1) * linearPerturbation i) = 0) :
52     y = (fun _ : Fin 1 => (-4 : ℤ_[2])) := by
53   ext i
54   fin_cases i
55   have h := hy 0
56   simp [linearSystem, linearPerturbation] at h
57   change y 0 = -4
58   linear_combination h
59 
60 /-- The response contains both H(a)=1 and K v=1, with the same negative sign. -/
61 theorem linear_joint_forcing_and_error :
62     eval (0 : Fin (1 + 1) → ℤ_[2]) (linearPerturbation 0) +
63       eval (0 : Fin (1 + 1) → ℤ_[2])
64         (pderiv (Fin.natAdd 1 0) (linearSystem 0)) * 1 = 2 ∧
65     (-4 : ℤ_[2]) = -(2 : ℤ_[2]) ^ 1 * (1 + 1) + 0 ∧
66     (2 : ℤ_[2]) ^ 2 ∣ (0 : ℤ_[2]) := by
67   norm_num [linearSystem, linearPerturbation, pderiv_X, Pi.single_apply, Fin.ext_iff]
68 
69 /-- The actual solved and parameter Jacobian matrices both equal the identity. -/
70 theorem linear_actual_jacobians :
71     PolynomialJointSystem.solvedJacobian linearSystem (0 : Fin (1 + 1) → ℤ_[2]) =
72       (1 : Matrix (Fin 1) (Fin 1) ℤ_[2]) ∧
73     PolynomialJointSystem.parameterJacobian linearSystem (0 : Fin (1 + 1) → ℤ_[2]) =
74       (1 : Matrix (Fin 1) (Fin 1) ℤ_[2]) := by
75   constructor <;> ext i j <;> fin_cases i <;> fin_cases j <;>
76     norm_num [PolynomialJointSystem.solvedJacobian, PolynomialJointSystem.parameterJacobian,
77       linearSystem, pderiv_X, Pi.single_apply, Matrix.one_apply, Fin.ext_iff]
78 
79 /-- At M=2 the actual augmented system has solved root -8 and prescribed parameter 4.
80 This precision distinguishes an incorrect response formula from its allowed error. -/
81 theorem linear_augmented_root_depth_two :
82     ∀ i, eval (join (fun _ : Fin 1 => (-8 : ℤ_[2])) (fun _ : Fin 1 => (4 : ℤ_[2])))
83       (PolynomialMotionNormalization.perturbSystem 2 2
84         (PolynomialJointSystem.augmented linearSystem (0 : Fin 1 → ℤ_[2]))
85         (PolynomialJointSystem.augmentedPerturbation linearPerturbation
86           (fun _ : Fin 1 => (1 : ℤ_[2]))) i) = 0 := by
87   apply (PolynomialJointSystem.perturb_augmented_root_iff 2 2 linearSystem linearPerturbation
88     (0 : Fin 1 → ℤ_[2]) (fun _ : Fin 1 => (1 : ℤ_[2])) _).mpr
89   constructor
90   · intro i
91     norm_num [linearSystem, linearPerturbation]
92   · rw [freePart_join]
93     ext i
94     norm_num
95 
96 /-- Omitting K v fails even modulo the permitted first-order error ideal. -/
97 theorem omitted_parameter_term_fails :
98     ¬ (2 : ℤ_[2]) ^ 4 ∣ (-8 : ℤ_[2]) - (-(2 : ℤ_[2]) ^ 2 * 1) := by
99   intro h
100   have hz : (2 : ℤ) ^ 4 ∣ (-4 : ℤ) :=
101     (PolynomialPadicUnique.int_pow_dvd_iff 2 4 (-4)).mpr (by convert h using 1 <;> norm_num)
102   norm_num at hz
103 
104 /-- Reversing the sign of K v also fails at the actual theorem's error precision. -/
105 theorem reversed_parameter_sign_fails :
106     ¬ (2 : ℤ_[2]) ^ 4 ∣ (-8 : ℤ_[2]) - (-(2 : ℤ_[2]) ^ 2 * (1 - 1)) := by
107   intro h
108   have hz : (2 : ℤ) ^ 4 ∣ (-8 : ℤ) :=
109     (PolynomialPadicUnique.int_pow_dvd_iff 2 4 (-8)).mpr (by convert h using 1 <;> norm_num)
110   norm_num at hz
111 
112 /-- The parameter-only nonlinear example is an actual two-variable polynomial. -/
113 def quadraticParameterSystem : Fin 1 → MvPolynomial (Fin (1 + 1)) ℤ_[2] :=
114   fun _ => X (Fin.castAdd 1 0) + X (Fin.castAdd 1 0) ^ 2 + X (Fin.natAdd 1 0)
115 
116 /-- Its unperturbed root has solved Jacobian 1 and parameter Jacobian 1. -/
117 theorem quadratic_parameter_base_data :
118     eval (0 : Fin (1 + 1) → ℤ_[2]) (quadraticParameterSystem 0) = 0 ∧
119     eval (0 : Fin (1 + 1) → ℤ_[2])
120       (pderiv (Fin.castAdd 1 0) (quadraticParameterSystem 0)) = 1 ∧
121     eval (0 : Fin (1 + 1) → ℤ_[2])
122       (pderiv (Fin.natAdd 1 0) (quadraticParameterSystem 0)) = 1 := by
123   norm_num [quadraticParameterSystem, pderiv_X, Pi.single_apply, Fin.ext_iff]
124 
125 /-- With H=0 and parameter shift 2, the first-order error has exactly depth two.
126 The root exists by the previously checked scalar root-motion theorem. -/
127 theorem exists_sharp_parameter_only_root :
128     ∃ y : Fin 1 → ℤ_[2],
129       (∀ i, eval (join y (fun _ : Fin 1 => (2 : ℤ_[2])))
130         (quadraticParameterSystem i) = 0) ∧
131       (2 : ℤ_[2]) ∣ y 0 ∧
132       (2 : ℤ_[2]) ^ 2 ∣ y 0 + 2 ∧
133       ¬ (2 : ℤ_[2]) ^ 3 ∣ y 0 + 2 := by
134   obtain ⟨b, hroot, heven, hdepth, hsharp⟩ := PolynomialMotionControls.exists_sharp_motion_root
135   refine ⟨fun _ => b, ?_, heven, hdepth, hsharp⟩
136   intro i
137   simpa [quadraticParameterSystem] using hroot
138 
139 /-- An extra error digit cannot hold uniformly even for parameter-only motion. -/
140 theorem no_uniform_extra_parameter_error_digit :
141     ¬ ∀ y : Fin 1 → ℤ_[2],
142       (∀ i, eval (join y (fun _ : Fin 1 => (2 : ℤ_[2])))
143         (quadraticParameterSystem i) = 0) →
144       (2 : ℤ_[2]) ∣ y 0 → (2 : ℤ_[2]) ^ 3 ∣ y 0 + 2 := by
145   intro h
146   obtain ⟨y, hy, heven, _, hsharp⟩ := exists_sharp_parameter_only_root
147   exact hsharp (h y hy heven)
148 
149 end Komorebi.PolynomialJointMotionControls

Back to source controls