PolynomialJointMotion.lean

1 module
2 public import PolynomialJointSystem
3 public import PolynomialBlockInverse
4 public import PolynomialRootMotion
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialJointMotion
11 open MvPolynomial Matrix
12 open Komorebi.PolynomialParameterSystem (join solvedPart freePart join_solved)
13 open Komorebi.PolynomialWeightedInverse Komorebi.PolynomialMotionNormalization
14 open Komorebi.PolynomialJointSystem Komorebi.PolynomialBlockInverse
15 
16 variable {e k : ℕ}
17 
18 /-- The original solved inverse certificate constructs the joint perturbed root.
19 The exact parameter displacement is built into actual augmented polynomial equations.
20 The integral first-order estimate retains the original denominator exponent. -/
21 theorem exists_joint_root_certificate (p s M : ℕ) [Fact p.Prime]
22     (hM : 2 * s < M) (F H : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
23     (a : Fin (e + k) → ℤ_[p]) (v : Fin k → ℤ_[p])
24     (A : Matrix (Fin e) (Fin e) ℤ_[p])
25     (hAJ : A * solvedJacobian F a =
26       (p : ℤ_[p]) ^ s • (1 : Matrix (Fin e) (Fin e) ℤ_[p]))
27     (hJA : solvedJacobian F a * A =
28       (p : ℤ_[p]) ^ s • (1 : Matrix (Fin e) (Fin e) ℤ_[p]))
29     (hFa : ∀ i, eval a (F i) = 0) :
30     ∃ b : Fin (e + k) → ℤ_[p],
31       (∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0) ∧
32       freePart b = freePart a + (p : ℤ_[p]) ^ M • v ∧
33       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) ∧
34       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
35       (∀ z : Fin (e + k) → ℤ_[p],
36         (∀ i, eval z (F i) + (p : ℤ_[p]) ^ M * eval z (H i) = 0) →
37         freePart z = freePart a + (p : ℤ_[p]) ^ M • v →
38         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) ∧
39       (∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣
40         solvedPart b i - solvedPart a i + (p : ℤ_[p]) ^ (M - s) *
41           A.mulVec ((fun j => eval a (H j)) + (parameterJacobian F a).mulVec v) i) := by
42   let B := blockCertificate A (parameterJacobian F a) ((p : ℤ_[p]) ^ s)
43   have hJac : jacobian (augmented F (freePart a)) a =
44       upperBlock (solvedJacobian F a) (parameterJacobian F a) 1 :=
45     jacobian_augmented F (freePart a) a
46   obtain ⟨hBA, hAB⟩ := blockCertificate_two_sided A (solvedJacobian F a)
47     (parameterJacobian F a) ((p : ℤ_[p]) ^ s) hAJ hJA
48   rw [← hJac] at hBA hAB
49   have hBase := augmented_root F a hFa
50   obtain ⟨b, hb, hdepth, hball, huniq⟩ :=
51     PolynomialRootMotion.exists_perturbed_root_certificate p s M hM
52       (augmented F (freePart a)) (augmentedPerturbation H v) a B hBA hAB hBase
53   have hbParts := (perturb_augmented_root_iff p M F H (freePart a) v b).mp hb
54   have hbSum : ∀ i, eval b (augmented F (freePart a) i) +
55       (p : ℤ_[p]) ^ M * eval b (augmentedPerturbation H v i) = 0 := by
56     intro i
57     simpa only [eval_perturbSystem] using hb i
58   have herror := PolynomialMotionEstimate.first_order_error_dvd p s M
59     (augmented F (freePart a)) (augmentedPerturbation H v) a b B
60     hM hBA hBase hbSum hdepth
61   refine ⟨b, hbParts.1, hbParts.2, hdepth, hball, ?_, ?_⟩
62   · intro z hz ht hzb
63     exact huniq z ((perturb_augmented_root_iff p M F H (freePart a) v z).mpr
64       ⟨hz, ht⟩) hzb
65   · intro i
66     have hi := herror (Fin.castAdd k i)
67     change (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣
68       b (Fin.castAdd k i) - a (Fin.castAdd k i) + (p : ℤ_[p]) ^ (M - s) *
69         (blockCertificate A (parameterJacobian F a) ((p : ℤ_[p]) ^ s)).mulVec
70           (fun j => eval a (augmentedPerturbation H v j)) (Fin.castAdd k i) at hi
71     rw [eval_augmentedPerturbation, blockCertificate_mulVec_join_neg, join_solved] at hi
72     exact hi
73 
74 /-- Simultaneous coefficient and prescribed parameter motion under the original
75 actual solved Jacobian's rational inverse bound. The perturbed Jacobian is not a hypothesis. -/
76 theorem exists_joint_root_motion (p s M : ℕ) [Fact p.Prime]
77     (hM : 2 * s < M) (F H : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
78     (a : Fin (e + k) → ℤ_[p]) (v : Fin k → ℤ_[p])
79     (hFa : ∀ i, eval a (F i) = 0)
80     (hJ : IsUnit (rationalMatrix p (solvedJacobian F a)))
81     (hbound : ∃ A : Matrix (Fin e) (Fin e) ℤ_[p],
82       rationalMatrix p A = (p : ℚ_[p]) ^ s • (rationalMatrix p (solvedJacobian F a))⁻¹) :
83     ∃ b : Fin (e + k) → ℤ_[p],
84       (∀ i, eval b (F i) + (p : ℤ_[p]) ^ M * eval b (H i) = 0) ∧
85       freePart b = freePart a + (p : ℤ_[p]) ^ M • v ∧
86       (∀ i, (p : ℤ_[p]) ^ (M - s) ∣ b i - a i) ∧
87       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
88       (∀ z : Fin (e + k) → ℤ_[p],
89         (∀ i, eval z (F i) + (p : ℤ_[p]) ^ M * eval z (H i) = 0) →
90         freePart z = freePart a + (p : ℤ_[p]) ^ M • v →
91         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) ∧
92       (∃ ε : Fin e → ℤ_[p], (∀ i, (p : ℤ_[p]) ^ (2 * M - 3 * s) ∣ ε i) ∧
93         ∀ i, ((solvedPart b i : ℤ_[p]) : ℚ_[p]) - ((solvedPart a i : ℤ_[p]) : ℚ_[p]) =
94           -(p : ℚ_[p]) ^ M * ((rationalMatrix p (solvedJacobian F a))⁻¹).mulVec
95             (fun j => ((eval a (H j) + (parameterJacobian F a).mulVec v j : ℤ_[p]) : ℚ_[p])) i +
96           (ε i : ℚ_[p])) := by
97   obtain ⟨A, hA⟩ := hbound
98   obtain ⟨hAJ, hJA⟩ := certificate_of_integral_inverse p s (solvedJacobian F a) A hJ hA
99   obtain ⟨b, hb, ht, hdepth, hball, huniq, herror⟩ :=
100     exists_joint_root_certificate p s M hM F H a v A hAJ hJA hFa
101   obtain ⟨ε, hε, hformula⟩ := PolynomialMotionRational.exists_rational_error
102     p s M (2 * M - 3 * s) (by omega) (solvedJacobian F a) A hA
103     (solvedPart a) (solvedPart b)
104     ((fun j => eval a (H j)) + (parameterJacobian F a).mulVec v) herror
105   exact ⟨b, hb, ht, hdepth, hball, huniq, ε, hε, hformula⟩
106 
107 end Komorebi.PolynomialJointMotion

Back to source controls