PolynomialJointMotionContracts.lean

1 module
2 public import PolynomialJointDeformation
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 open scoped BigOperators
8 
9 namespace Komorebi.PolynomialJointMotionContracts
10 open MvPolynomial
11 variable {e k : ℕ}
12 
13 /-- The actual solved derivative certificate constructs a root of the original
14 perturbed equations with exactly the prescribed parameters. The parameter derivative
15 is explicit in the integral first-order error, and uniqueness is on the full ball. -/
16 theorem actual_joint_certificate (p s M : ℕ) [Fact p.Prime]
17     (hM : 2 * s < M) (F H : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
18     (a : Fin (e + k) → ℤ_[p]) (v : Fin k → ℤ_[p])
19     (A : Matrix (Fin e) (Fin e) ℤ_[p])
20     (hAJ : A * (Matrix.of fun i j => eval a (pderiv (Fin.castAdd k j) (F i))) =
21       (p : ℤ_[p]) ^ s • (1 : Matrix (Fin e) (Fin e) ℤ_[p]))
22     (hJA : (Matrix.of fun i j => eval a (pderiv (Fin.castAdd k j) (F i))) * A =
23       (p : ℤ_[p]) ^ s • (1 : Matrix (Fin e) (Fin e) ℤ_[p]))
24     (hFa : ∀ i, eval a (F i) = 0) :
25     ∃ b : Fin (e + k) → ℤ_[p],
26       (∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0) ∧
27       (∀ j, b (Fin.natAdd e j) = a (Fin.natAdd e j) + (p : ℤ_[p]) ^ M * v j) ∧
28       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) ∧
29       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
30       (∀ z : Fin (e + k) → ℤ_[p],
31         (∀ i, eval z (F i) + (p : ℤ_[p]) ^ M * eval z (H i) = 0) →
32         (∀ j, z (Fin.natAdd e j) = a (Fin.natAdd e j) + (p : ℤ_[p]) ^ M * v j) →
33         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) ∧
34       (∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣
35         b (Fin.castAdd k i) - a (Fin.castAdd k i) + (p : ℤ_[p]) ^ (M - s) *
36           A.mulVec ((fun j => eval a (H j)) +
37             (Matrix.of fun r j => eval a (pderiv (Fin.natAdd e j) (F r))).mulVec v) i) := by
38   obtain ⟨b, hb, ht, hdepth, hball, huniq, herror⟩ :=
39     PolynomialJointMotion.exists_joint_root_certificate p s M hM F H a v A hAJ hJA hFa
40   refine ⟨b, hb, fun j => congrFun ht j, hdepth, hball, ?_, herror⟩
41   intro z hz hzt hzb
42   exact huniq z hz (funext hzt) hzb
43 
44 /-- The final statement names only the original polynomial derivatives and the
45 original solved inverse bound. Parameters are substituted explicitly, and the
46 first-order formula contains both the coefficient and parameter forcing. -/
47 theorem actual_joint_rational_motion (p s M : ℕ) [Fact p.Prime]
48     (hM : 2 * s < M) (F H : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
49     (a : Fin (e + k) → ℤ_[p]) (hFa : ∀ i, eval a (F i) = 0)
50     (hJ : IsUnit ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix
51       (fun i j => eval a (pderiv (Fin.castAdd k j) (F i)))))
52     (hbound : ∃ A : Matrix (Fin e) (Fin e) ℤ_[p],
53       (algebraMap ℤ_[p] ℚ_[p]).mapMatrix A = (p : ℚ_[p]) ^ s •
54         ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix
55           (fun i j => eval a (pderiv (Fin.castAdd k j) (F i))))⁻¹)
56     (v : Fin k → ℤ_[p]) :
57     ∃ y : Fin e → ℤ_[p],
58       (∀ i, eval (Fin.append y (fun j => a (Fin.natAdd e j) + (p : ℤ_[p]) ^ M * v j))
59           (F i) + (p : ℤ_[p]) ^ M *
60         eval (Fin.append y (fun j => a (Fin.natAdd e j) + (p : ℤ_[p]) ^ M * v j)) (H i) = 0) ∧
61       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ y i - a (Fin.castAdd k i)) ∧
62       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ y i - a (Fin.castAdd k i)) ∧
63       (∀ z : Fin e → ℤ_[p],
64         (∀ i, eval (Fin.append z (fun j => a (Fin.natAdd e j) + (p : ℤ_[p]) ^ M * v j))
65             (F i) + (p : ℤ_[p]) ^ M *
66           eval (Fin.append z (fun j => a (Fin.natAdd e j) + (p : ℤ_[p]) ^ M * v j)) (H i) = 0) →
67         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a (Fin.castAdd k i)) → z = y) ∧
68       (∃ ε : Fin e → ℤ_[p], (∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣ ε i) ∧
69         ∀ i, (y i : ℚ_[p]) - (a (Fin.castAdd k i) : ℚ_[p]) =
70           -(p : ℚ_[p]) ^ M *
71             (((algebraMap ℤ_[p] ℚ_[p]).mapMatrix
72               (fun r j => eval a (pderiv (Fin.castAdd k j) (F r))))⁻¹).mulVec
73               (fun j => ((eval a (H j) +
74                 (Matrix.of fun r t => eval a (pderiv (Fin.natAdd e t) (F r))).mulVec v j : ℤ_[p]) : ℚ_[p])) i +
75             (ε i : ℚ_[p])) := by
76   have result := PolynomialJointDeformation.exists_joint_deformation
77     p s M hM F H a hFa hJ hbound v
78   unfold PolynomialWeightedInverse.rationalMatrix
79     PolynomialJointSystem.solvedJacobian PolynomialJointSystem.parameterJacobian
80     PolynomialParameterSystem.join PolynomialParameterSystem.solvedPart
81     PolynomialParameterSystem.freePart at result
82   exact result
83 
84 end Komorebi.PolynomialJointMotionContracts

Back to source controls