PolynomialSurjectiveStep.lean

1 module
2 public import PolynomialDigitBridge
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialSurjectiveStep
9 open Komorebi.NativeAffine Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
10 variable {d e : ℕ}
11 
12 /-- The actual residue-ring Jacobian depends only on the point modulo q. -/
13 theorem digitJacobian_eq (q : ℕ) (F : Fin e → MvPolynomial (Fin d) ℤ)
14     (x y : Fin d → ℤ) (hxy : ∀ i, (q : ℤ) ∣ y i - x i) :
15     digitJacobian q F y = digitJacobian q F x := by
16   apply LinearMap.ext
17   intro t
18   ext i
19   change (∑ k, (MvPolynomial.eval y (MvPolynomial.pderiv k (F i)) : ZMod q) * t k) =
20     ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod q) * t k
21   apply Finset.sum_congr rfl
22   intro k _
23   have hd := Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd (F i) x y q hxy k
24   have hz := (ZMod.intCast_zmod_eq_zero_iff_dvd
25     (MvPolynomial.eval y (MvPolynomial.pderiv k (F i)) -
26       MvPolynomial.eval x (MvPolynomial.pderiv k (F i))) q).mpr hd
27   rw [Int.cast_sub, sub_eq_zero] at hz
28   rw [hz]
29 
30 /-- Every positive-depth digit correction preserves the actual finite Jacobian. -/
31 theorem digitJacobian_shift_eq (q L : ℕ) (hL : 1 ≤ L)
32     (F : Fin e → MvPolynomial (Fin d) ℤ) (x s : Fin d → ℤ) :
33     digitJacobian q F (x + (q : ℤ)^L • s) = digitJacobian q F x := by
34   apply digitJacobian_eq
35   intro i
36   change (q : ℤ) ∣ x i + (q : ℤ)^L * s i - x i
37   rw [add_sub_cancel_left]
38   exact dvd_mul_of_dvd_left (dvd_pow_self (q : ℤ) (by omega : L ≠ 0)) _
39 
40 /-- Surjectivity of the reduced Jacobian produces an actual next polynomial
41 solution and is preserved at that new solution. -/
42 theorem one_step_lift (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
43     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
44     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i)
45     (hJ : Function.Surjective (digitJacobian q F x)) :
46     ∃ y : Fin d → ℤ,
47       (∀ i, (q : ℤ)^L ∣ (y - x) i) ∧
48       (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F y i) ∧
49       Function.Surjective (digitJacobian q F y) := by
50   obtain ⟨r, hr⟩ := Komorebi.PolynomialObstruction.residual_exists q L F x hx
51   obtain ⟨t, ht⟩ := hJ (-(reduction q e r))
52   have hcorr : reduction q e r + digitJacobian q F x t = 0 := by
53     rw [ht, add_neg_cancel]
54   refine ⟨x + (q : ℤ)^L • integerLift q t, ?_, ?_, ?_⟩
55   · exact (same_residue_iff ((q : ℤ)^L) x _).mpr ⟨integerLift q t, rfl⟩
56   · exact (digit_solution_iff q L hq hL F x r hr t).mpr hcorr
57   · rw [digitJacobian_shift_eq q L hL F x]
58     exact hJ
59 
60 end Komorebi.PolynomialSurjectiveStep

Back to source controls