PolynomialPrescribedObstruction.lean

1 module
2 public import PolynomialPrescribedLifts
3 public import PolynomialPrescribedCounts
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 open scoped Classical
9 
10 namespace Komorebi.PolynomialPrescribedObstruction
11 open PolynomialObstruction PolynomialDigitBridge PolynomialPrescribedSystem
12 open PolynomialPrescribedLifts PolynomialParameterSystem ResidueLiftDigits
13 variable {m k e : ℕ}
14 
15 /-- The solved-block cokernel class decides actual next-level residue lifts with
16 the requested parameter digits, including positive composite moduli. -/
17 theorem prescribed_lift_iff_obstruction_zero (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
18     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
19     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ) ^ L • r)
20     (v : Fin k → ZMod q) :
21     Nonempty (PrescribedLifts q L F x v) ↔ PolynomialPrescribedSystem.obstruction q F x r v = 0 := by
22   have he := prescribedDigitEquivLifts q L hq hL F x r hr v
23   constructor
24   · rintro ⟨y⟩
25     exact (prescribed_digits_nonempty_iff q F x r v).mp ⟨he.symm y⟩
26   · intro h
27     obtain ⟨u⟩ := (prescribed_digits_nonempty_iff q F x r v).mpr h
28     exact ⟨he u⟩
29 
30 /-- Expanded actual residue-vector form: the lower residue, the polynomial root
31 condition, and the prescribed next parameter residues are all explicit. -/
32 theorem prescribed_residue_exists_iff (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
33     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
34     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ) ^ L • r)
35     (v : Fin k → ZMod q) :
36     (∃ y : Fin (m + k) → ZMod (q ^ (L + 1)),
37       (∀ i, (q : ℤ) ^ L ∣ ((y i).val : ℤ) - x i) ∧
38       (∀ i, (q : ℤ) ^ (L + 1) ∣ evalSystem F (integerLift (q ^ (L + 1)) y) i) ∧
39       (∀ j : Fin k, y (Fin.natAdd m j) =
40         ((x (Fin.natAdd m j) + (q : ℤ) ^ L * ((v j).val : ℤ) : ℤ) :
41           ZMod (q ^ (L + 1))))) ↔ PolynomialPrescribedSystem.obstruction q F x r v = 0 := by
42   rw [← prescribed_lift_iff_obstruction_zero q L hq hL F x r hr v]
43   constructor
44   · rintro ⟨y, hy, hF, hv⟩
45     exact ⟨⟨⟨⟨y, hy⟩, hF⟩, funext hv⟩⟩
46   · rintro ⟨y⟩
47     exact ⟨y.val.val.val, y.val.val.property, y.val.property, fun j => congrFun y.property j⟩
48 
49 /-- The solved-block cokernel is finite for every positive modulus. -/
50 theorem prescribed_obstruction_finite (q : ℕ) (hq : 0 < q)
51     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ) :
52     Finite (PrescribedObstruction q F x) := by
53   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
54   unfold PrescribedObstruction
55   infer_instance
56 
57 /-- The residual and a single finite obstruction object are obtained from the
58 actual lower root, uniformly for every choice of the parameter digit. -/
59 theorem finite_prescribed_obstruction (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
60     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
61     (hx : ∀ i, (q : ℤ) ^ L ∣ evalSystem F x i) :
62     ∃ r : Fin e → ℤ, evalSystem F x = (q : ℤ) ^ L • r ∧
63       Finite (PrescribedObstruction q F x) ∧
64       (∀ v : Fin k → ZMod q, Nonempty (PrescribedLifts q L F x v) ↔
65         PolynomialPrescribedSystem.obstruction q F x r v = 0) := by
66   obtain ⟨r, hr⟩ := residual_exists q L F x hx
67   exact ⟨r, hr, prescribed_obstruction_finite q hq F x,
68     fun v => prescribed_lift_iff_obstruction_zero q L hq hL F x r hr v⟩
69 
70 /-- From an actual lower root, every prescribed parameter fiber has the exact
71 prime-field count, and the solved-block obstruction has its exact cardinality. -/
72 theorem finite_prescribed_lift_count (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
73     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
74     (hx : ∀ i, (p : ℤ) ^ L ∣ evalSystem F x i) :
75     ∃ r : Fin e → ℤ, evalSystem F x = (p : ℤ) ^ L • r ∧
76       (∀ v : Fin k → ZMod p,
77         (Nonempty (PrescribedLifts p L F x v) ↔
78           PolynomialPrescribedSystem.obstruction p F x r v = 0) ∧
79         Nat.card (PrescribedLifts p L F x v) =
80           if PolynomialPrescribedSystem.obstruction p F x r v = 0 then
81             p ^ (m - FiniteFiberCounts.rank p (PolynomialPrescribedSystem.solvedJacobian p F x))
82           else 0) ∧
83       Nat.card (PrescribedObstruction p F x) =
84         p ^ (e - FiniteFiberCounts.rank p (PolynomialPrescribedSystem.solvedJacobian p F x)) := by
85   obtain ⟨r, hr⟩ := residual_exists p L F x hx
86   refine ⟨r, hr, ?_, PolynomialPrescribedCounts.obstruction_card p F x⟩
87   intro v
88   exact ⟨prescribed_lift_iff_obstruction_zero p L (Fact.out : Nat.Prime p).pos hL F x r hr v,
89     PolynomialPrescribedCounts.lift_card p L hL F x r hr v⟩
90 
91 end Komorebi.PolynomialPrescribedObstruction

Back to source controls