PolynomialPrescribedContract.lean

1 module
2 public import PolynomialPrescribedObstruction
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 open scoped BigOperators Classical
8 
9 namespace Komorebi.PolynomialPrescribedContract
10 open MvPolynomial
11 variable {m k e : ℕ}
12 
13 /-- The contract writes the solved-coordinate derivative columns explicitly. -/
14 def actualSolvedMap (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
15     (x : Fin (m + k) → ℤ) : (Fin m → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q) where
16   toFun u i := ∑ j, (eval x (pderiv (Fin.castAdd k j) (F i)) : ZMod q) * u j
17   map_add' u v := by ext i; simp [mul_add, Finset.sum_add_distrib]
18   map_smul' a u := by
19     ext i
20     simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
21     rw [Finset.mul_sum]
22     apply Finset.sum_congr rfl
23     intro j _
24     ring
25 
26 /-- Actual next-level residue vectors, with all three restrictions written out. -/
27 abbrev ActualResidues (q L : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
28     (x : Fin (m + k) → ℤ) (v : Fin k → ZMod q) :=
29   {y : Fin (m + k) → ZMod (q ^ (L + 1)) //
30     (∀ i, (q : ℤ) ^ L ∣ ((y i).val : ℤ) - x i) ∧
31     (∀ i, (q : ℤ) ^ (L + 1) ∣ eval (fun j => ((y j).val : ℤ)) (F i)) ∧
32     (∀ j : Fin k, y (Fin.natAdd m j) =
33       ((x (Fin.natAdd m j) + (q : ℤ) ^ L * ((v j).val : ℤ) : ℤ) :
34         ZMod (q ^ (L + 1))))}
35 
36 /-- Flattening the formal lift subtype preserves precisely the residue vectors. -/
37 def actualResidueEquiv (q L : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
38     (x : Fin (m + k) → ℤ) (v : Fin k → ZMod q) :
39     ActualResidues q L F x v ≃ PolynomialPrescribedLifts.PrescribedLifts q L F x v where
40   toFun y := ⟨⟨⟨y.val, y.property.1⟩, y.property.2.1⟩, funext y.property.2.2⟩
41   invFun y := ⟨y.val.val.val, y.val.val.property, y.val.property,
42     fun j => congrFun y.property j⟩
43   left_inv _ := rfl
44   right_inv _ := rfl
45 
46 /-- The lower root alone supplies one residual for every parameter choice.
47 Both the solved quotient and parameter derivative contributions are explicit. -/
48 theorem actual_lower_root_obstruction (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
49     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
50     (hx : ∀ i, (q : ℤ) ^ L ∣ eval x (F i)) :
51     ∃ r : Fin e → ℤ, (∀ i, eval x (F i) = (q : ℤ) ^ L * r i) ∧
52       Finite ((Fin e → ZMod q) ⧸ (actualSolvedMap q F x).range) ∧
53       (∀ v : Fin k → ZMod q,
54         (∃ y : Fin (m + k) → ZMod (q ^ (L + 1)),
55           (∀ i, (q : ℤ) ^ L ∣ ((y i).val : ℤ) - x i) ∧
56           (∀ i, (q : ℤ) ^ (L + 1) ∣ eval (fun j => ((y j).val : ℤ)) (F i)) ∧
57           (∀ j : Fin k, y (Fin.natAdd m j) =
58             ((x (Fin.natAdd m j) + (q : ℤ) ^ L * ((v j).val : ℤ) : ℤ) :
59               ZMod (q ^ (L + 1))))) ↔
60         (Submodule.Quotient.mk (fun i => (r i : ZMod q) +
61           ∑ j : Fin k, (eval x (pderiv (Fin.natAdd m j) (F i)) : ZMod q) * v j) :
62           (Fin e → ZMod q) ⧸ (actualSolvedMap q F x).range) = 0) := by
63   obtain ⟨r, hr, hf, _⟩ :=
64     PolynomialPrescribedObstruction.finite_prescribed_obstruction q L hq hL F x hx
65   refine ⟨r, fun i => congrFun hr i, hf, ?_⟩
66   intro v
67   exact PolynomialPrescribedObstruction.prescribed_residue_exists_iff q L hq hL F x r hr v
68 
69 /-- Prime-field counts apply to the actual constrained residue vectors, using
70 rank of the solved derivative block and the same derived residual for every v. -/
71 theorem actual_lower_root_prime_count (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
72     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
73     (hx : ∀ i, (p : ℤ) ^ L ∣ eval x (F i)) :
74     ∃ r : Fin e → ℤ, (∀ i, eval x (F i) = (p : ℤ) ^ L * r i) ∧
75       (∀ v : Fin k → ZMod p,
76         Nat.card (ActualResidues p L F x v) =
77           if (Submodule.Quotient.mk (fun i => (r i : ZMod p) +
78             ∑ j : Fin k, (eval x (pderiv (Fin.natAdd m j) (F i)) : ZMod p) * v j) :
79             (Fin e → ZMod p) ⧸ (actualSolvedMap p F x).range) = 0 then
80               p ^ (m - Module.finrank (ZMod p) (actualSolvedMap p F x).range) else 0) ∧
81       Nat.card ((Fin e → ZMod p) ⧸ (actualSolvedMap p F x).range) =
82         p ^ (e - Module.finrank (ZMod p) (actualSolvedMap p F x).range) := by
83   obtain ⟨r, hr, hv, hc⟩ :=
84     PolynomialPrescribedObstruction.finite_prescribed_lift_count p L hL F x hx
85   refine ⟨r, fun i => congrFun hr i, ?_, hc⟩
86   intro v
87   rw [Nat.card_congr (actualResidueEquiv p L F x v)]
88   exact (hv v).2
89 
90 end Komorebi.PolynomialPrescribedContract

Back to source controls