PolynomialSharedContract.lean

1 module
2 public import PolynomialShared
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialSharedContract
9 
10 /-- A common integer representative, both polynomial blocks, and the explicit
11 sum-of-kernels quotient are exposed without an assumed compatibility premise. -/
12 theorem explicit_shared_polynomial_contract (d e f q L : ℕ)
13     (hq : 0 < q) (hL : 1 ≤ L)
14     (F : Fin e → MvPolynomial (Fin d) ℤ)
15     (G : Fin f → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
16     (hxF : ∀ i, (q : ℤ)^L ∣ MvPolynomial.eval x (F i))
17     (hxG : ∀ i, (q : ℤ)^L ∣ MvPolynomial.eval x (G i)) :
18     Finite ((Fin d → ℤ) ⧸
19       (LinearMap.ker (NativeAffine.digitMap q (PolynomialObstruction.jacobian F x)) ⊔
20         LinearMap.ker (NativeAffine.digitMap q (PolynomialObstruction.jacobian G x)))) ∧
21       ((∃ y : Fin d → ℤ,
22         (∀ i, (q : ℤ)^L ∣ y i - x i) ∧
23         (∀ i, (q : ℤ)^(L+1) ∣ MvPolynomial.eval y (F i)) ∧
24         (∀ i, (q : ℤ)^(L+1) ∣ MvPolynomial.eval y (G i))) ↔
25         ∃ u v : Fin d → ℤ,
26           (∀ i, (q : ℤ)^(L+1) ∣
27             MvPolynomial.eval (fun k => x k + (q : ℤ)^L * u k) (F i)) ∧
28           (∀ i, (q : ℤ)^(L+1) ∣
29             MvPolynomial.eval (fun k => x k + (q : ℤ)^L * v k) (G i)) ∧
30           (Submodule.Quotient.mk u : (Fin d → ℤ) ⧸
31             (LinearMap.ker (NativeAffine.digitMap q (PolynomialObstruction.jacobian F x)) ⊔
32               LinearMap.ker (NativeAffine.digitMap q (PolynomialObstruction.jacobian G x)))) =
33             Submodule.Quotient.mk v) :=
34   PolynomialShared.finite_polynomial_pair_compatibility q L hq hL F G x hxF hxG
35 
36 end Komorebi.PolynomialSharedContract

Back to source controls