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

Back to source controls