PolynomialDigitBridge.lean

1 module
2 public import PolynomialObstruction
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialDigitBridge
9 open Komorebi.NativeAffine Komorebi.PolynomialObstruction
10 variable {d e : ℕ}
11 
12 /-- Canonical integer representatives of correction digits. -/
13 def integerLift (q : ℕ) (t : Fin d → ZMod q) : Fin d → ℤ :=
14   fun i => (t i).val
15 
16 /-- The actual Jacobian over the finite coefficient ring. -/
17 def digitJacobian (q : ℕ) (F : Fin e → MvPolynomial (Fin d) ℤ)
18     (x : Fin d → ℤ) : (Fin d → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q) where
19   toFun t i := ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod q) * t k
20   map_add' t u := by
21     ext i
22     simp [mul_add, Finset.sum_add_distrib]
23   map_smul' a t := by
24     ext i
25     simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
26     rw [Finset.mul_sum]
27     apply Finset.sum_congr rfl
28     intro k _
29     ring
30 
31 theorem reduction_integerLift (q : ℕ) (hq : 0 < q) (t : Fin d → ZMod q) :
32     reduction q d (integerLift q t) = t := by
33   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
34   ext i
35   change (((t i).val : ℤ) : ZMod q) = t i
36   rw [Int.cast_natCast, ZMod.natCast_zmod_val]
37 
38 /-- Reducing the original integer Jacobian gives exactly the finite-ring map. -/
39 theorem reduction_jacobian (q : ℕ) (F : Fin e → MvPolynomial (Fin d) ℤ)
40     (x t : Fin d → ℤ) :
41     digitJacobian q F x (reduction q d t) = reduction q e (jacobian F x t) := by
42   ext i
43   change (∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod q) * (t k : ZMod q)) =
44     ((∑ k, MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) * t k : ℤ) : ZMod q)
45   simp
46 
47 /-- A finite correction digit solves the linearized residual equation. -/
48 abbrev DigitSolutions (q : ℕ) (F : Fin e → MvPolynomial (Fin d) ℤ)
49     (x : Fin d → ℤ) (r : Fin e → ℤ) :=
50   {t : Fin d → ZMod q // reduction q e r + digitJacobian q F x t = 0}
51 
52 /-- Actual polynomial liftability for each finite correction digit. -/
53 theorem digit_solution_iff (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
54     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
55     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
56     (t : Fin d → ZMod q) :
57     (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • integerLift q t) i) ↔
58       reduction q e r + digitJacobian q F x t = 0 := by
59   rw [next_level_iff_digit q L hq hL F x r hr]
60   rw [map_add, ← reduction_jacobian, reduction_integerLift q hq t]
61 
62 /-- Every integer correction projects to a finite digit solution and conversely. -/
63 theorem digit_solutions_nonempty_iff (q : ℕ) (hq : 0 < q)
64     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) (r : Fin e → ℤ) :
65     Nonempty (DigitSolutions q F x r) ↔ obstruction q (jacobian F x) r = 0 := by
66   rw [obstruction_zero_iff_correction]
67   constructor
68   · rintro ⟨⟨t, ht⟩⟩
69     refine ⟨integerLift q t, ?_⟩
70     rw [map_add, ← reduction_jacobian, reduction_integerLift q hq t]
71     exact ht
72   · rintro ⟨t, ht⟩
73     refine ⟨⟨reduction q d t, ?_⟩⟩
74     rw [reduction_jacobian]
75     simpa only [map_add] using ht
76 
77 end Komorebi.PolynomialDigitBridge

Back to source controls