PolynomialObstructionContract.lean

1 module
2 public import PolynomialObstruction
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialObstructionContract
9 
10 /-- Actual integer representatives and polynomial evaluations, including the
11 finite quotient and its zero residual class, appear in the external contract. -/
12 theorem explicit_finite_polynomial_contract (d e q L : ℕ)
13     (hq : 0 < q) (hL : 1 ≤ L)
14     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
15     (hx : ∀ i, (q : ℤ)^L ∣ MvPolynomial.eval x (F i)) :
16     ∃ r : Fin e → ℤ,
17       (fun i => MvPolynomial.eval x (F i)) = (q : ℤ)^L • r ∧
18       Finite ((Fin e → ZMod q) ⧸
19         LinearMap.range (NativeAffine.digitMap q (PolynomialObstruction.jacobian F x))) ∧
20       ((∃ y : Fin d → ℤ,
21         (∀ i, (q : ℤ)^L ∣ y i - x i) ∧
22         (∀ i, (q : ℤ)^(L+1) ∣ MvPolynomial.eval y (F i))) ↔
23           (Submodule.Quotient.mk (fun i => (r i : ZMod q)) :
24             (Fin e → ZMod q) ⧸ LinearMap.range
25               (NativeAffine.digitMap q (PolynomialObstruction.jacobian F x))) = 0) :=
26   PolynomialObstruction.finite_polynomial_obstruction q L hq hL F x hx
27 
28 end Komorebi.PolynomialObstructionContract

Back to source controls