PolynomialTowerContract.lean

1 module
2 public import PolynomialIntegerTower
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.PolynomialTowerContract
8 
9 /-- One initial surjectivity hypothesis produces one sequence at all depths;
10 no preselected per-level roots, surjectivity assumptions, or compatibility are inputs. -/
11 theorem explicit_polynomial_tower (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
12     {d e : ℕ} (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
13     (hx : ∀ i, (q : ℤ)^L ∣ MvPolynomial.eval x (F i))
14     (hJ : Function.Surjective (PolynomialDigitBridge.digitJacobian q F x)) :
15     ∃ z : ℕ → Fin d → ℤ,
16       z 0 = x ∧
17       (∀ n i, (q : ℤ)^(L+n) ∣ MvPolynomial.eval (z n) (F i)) ∧
18       (∀ n i, (q : ℤ)^(L+n) ∣ z (n+1) i - z n i) ∧
19       (∀ m n, m ≤ n → ∀ i, (q : ℤ)^(L+m) ∣ z n i - z m i) ∧
20       (∀ n, PolynomialDigitBridge.digitJacobian q F (z n) =
21         PolynomialDigitBridge.digitJacobian q F x) ∧
22       (∀ n, Function.Surjective (PolynomialDigitBridge.digitJacobian q F (z n))) := by
23   exact PolynomialIntegerTower.exists_compatible_tower_strong q L hq hL F x hx hJ
24 
25 /-- The actual Jacobian map is evaluated from formal polynomial derivatives. -/
26 theorem explicit_jacobian (q : ℕ) {d e : ℕ}
27     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
28     (t : Fin d → ZMod q) (i : Fin e) :
29     PolynomialDigitBridge.digitJacobian q F x t i =
30       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod q) * t k := rfl
31 
32 end Komorebi.PolynomialTowerContract

Back to source controls