PolynomialLiftCountContract.lean

1 module
2 public import PolynomialLiftCounts
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 open scoped Classical
8 namespace Komorebi.PolynomialLiftCountContract
9 
10 /-- Full polynomial count contract: the lower solution is explicit, the counted
11 objects are actual next-level residue classes, and the rank is the Jacobian's. -/
12 theorem explicit_actual_polynomial_count (p L : ℕ) [Fact (Nat.Prime p)]
13     (hL : 1 ≤ L) {d e : ℕ} (F : Fin e → MvPolynomial (Fin d) ℤ)
14     (x : Fin d → ℤ)
15     (hx : ∀ i, (p : ℤ)^L ∣ MvPolynomial.eval x (F i)) :
16     ∃ r : Fin e → ℤ,
17       (∀ i, MvPolynomial.eval x (F i) = (p : ℤ)^L * r i) ∧
18       Nat.card {y : {y : Fin d → ZMod (p^(L+1)) //
19         ∀ k, (p : ℤ)^L ∣ ((y k).val : ℤ) - x k} //
20         ∀ i, (p : ℤ)^(L+1) ∣
21           MvPolynomial.eval (fun k => ((y.val k).val : ℤ)) (F i)} =
22         (if NativeAffine.obstruction p (PolynomialObstruction.jacobian F x) r = 0 then
23           p ^ (d - Module.finrank (ZMod p)
24             (PolynomialDigitBridge.digitJacobian p F x).range) else 0) ∧
25       Nat.card (NativeAffine.Obstruction p (PolynomialObstruction.jacobian F x)) =
26         p ^ (e - Module.finrank (ZMod p)
27           (PolynomialDigitBridge.digitJacobian p F x).range) := by
28   obtain ⟨r, hr, hc, ho⟩ :=
29     PolynomialLiftCounts.finite_polynomial_lift_count p L hL F x hx
30   exact ⟨r, fun i => congrFun hr i, hc, ho⟩
31 
32 /-- The map whose range defines the rank is the evaluated formal Jacobian. -/
33 theorem explicit_jacobian_formula (p : ℕ) {d e : ℕ}
34     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
35     (t : Fin d → ZMod p) (i : Fin e) :
36     PolynomialDigitBridge.digitJacobian p F x t i =
37       ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) * t k := rfl
38 
39 end Komorebi.PolynomialLiftCountContract

Back to source controls