PolynomialCountControls.lean

1 module
2 public import PolynomialLiftCounts
3 public import Mathlib.Tactic
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 namespace Komorebi.PolynomialCountControls
9 open MvPolynomial PolynomialDigitBridge NativeAffine PolynomialObstruction
10 
11 def linearSystem : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => X 0
12 def zeroSystem : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => 0
13 def squareSystem : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => X 0 ^ 2
14 def squareMinusTwo : Fin 1 → MvPolynomial (Fin 1) ℤ := fun _ => X 0 ^ 2 - C 2
15 
16 /-- A nonsingular linear equation has exactly one correction digit. -/
17 theorem linear_digit_count (q : ℕ) :
18     Nat.card (DigitSolutions q linearSystem (fun _ => 0) (fun _ => 0)) = 1 := by
19   apply Nat.card_eq_one_iff_exists.mpr
20   refine ⟨⟨0, by ext i; simp [reduction, digitJacobian, linearSystem]⟩, ?_⟩
21   intro t
22   apply Subtype.ext
23   funext i
24   have h := congrFun t.property 0
25   simpa [reduction, digitJacobian, linearSystem, Fin.eq_zero i] using h
26 
27 /-- A zero equation imposes no restriction on the single correction digit. -/
28 theorem zero_digit_count (q : ℕ) (hq : 0 < q) :
29     Nat.card (DigitSolutions q zeroSystem (fun _ => 0) (fun _ => 0)) = q := by
30   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
31   have h := Nat.card_congr (show DigitSolutions q zeroSystem (fun _ => 0) (fun _ => 0) ≃
32       (Fin 1 → ZMod q) from {
33     toFun := Subtype.val
34     invFun t := ⟨t, by ext i; simp [reduction, digitJacobian, zeroSystem]⟩
35     left_inv _ := rfl
36     right_inv _ := rfl })
37   simpa [Nat.card_fun, Nat.card_eq_fintype_card] using h
38 
39 /-- X²−2 at the even lower root has no correction digit modulo two. -/
40 theorem obstructed_square_digit_count :
41     Nat.card (DigitSolutions 2 squareMinusTwo (fun _ => 0) (fun _ => -1)) = 0 := by
42   apply Nat.card_eq_zero.mpr
43   left
44   refine ⟨fun t => ?_⟩
45   have h := congrFun t.property 0
46   change ((-1 : ℤ) : ZMod 2) +
47     (∑ k : Fin 1, (eval (fun _ : Fin 1 => (0 : ℤ))
48       (pderiv k (squareMinusTwo 0)) : ZMod 2) * t.val k) = 0 at h
49   simp only [squareMinusTwo, map_sub, pderiv_pow, pderiv_C] at h
50   norm_num at h
51 
52 /-- X² has the same zero Jacobian but both correction digits lift. -/
53 theorem singular_square_digit_count :
54     Nat.card (DigitSolutions 2 squareSystem (fun _ => 0) (fun _ => 0)) = 2 := by
55   have h := Nat.card_congr (show DigitSolutions 2 squareSystem (fun _ => 0) (fun _ => 0) ≃
56       (Fin 1 → ZMod 2) from {
57     toFun := Subtype.val
58     invFun t := ⟨t, by ext i; simp [reduction, digitJacobian, squareSystem]⟩
59     left_inv _ := rfl
60     right_inv _ := rfl })
61   simpa [Nat.card_fun, Nat.card_eq_fintype_card] using h
62 
63 /-- The linear count applies to actual next-level polynomial residue classes. -/
64 theorem linear_lift_count (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L) :
65     Nat.card (PolynomialLiftCounts.ActualLifts q L linearSystem (fun _ => 0)) = 1 := by
66   rw [← Nat.card_congr (PolynomialLiftCounts.digitEquivLifts q L hq hL
67     linearSystem (fun _ => 0) (fun _ => 0) (by ext i; simp [evalSystem, linearSystem]))]
68   exact linear_digit_count q
69 
70 /-- A zero equation leaves q actual next-level residue classes over the root. -/
71 theorem zero_lift_count (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L) :
72     Nat.card (PolynomialLiftCounts.ActualLifts q L zeroSystem (fun _ => 0)) = q := by
73   rw [← Nat.card_congr (PolynomialLiftCounts.digitEquivLifts q L hq hL
74     zeroSystem (fun _ => 0) (fun _ => 0) (by ext i; simp [evalSystem, zeroSystem]))]
75   exact zero_digit_count q hq
76 
77 /-- An even root of X²−2 modulo two has zero actual lifts modulo four. -/
78 theorem obstructed_square_lift_count :
79     Nat.card (PolynomialLiftCounts.ActualLifts 2 1 squareMinusTwo (fun _ => 0)) = 0 := by
80   rw [← Nat.card_congr (PolynomialLiftCounts.digitEquivLifts 2 1 (by decide) (by decide)
81     squareMinusTwo (fun _ => 0) (fun _ => -1)
82     (by
83       ext i
84       simp only [evalSystem, squareMinusTwo, map_sub, map_pow, eval_X, eval_C,
85         Pi.smul_apply, smul_eq_mul]
86       norm_num))]
87   exact obstructed_square_digit_count
88 
89 /-- A singular even root of X² modulo two has exactly two lifts modulo four. -/
90 theorem singular_square_lift_count :
91     Nat.card (PolynomialLiftCounts.ActualLifts 2 1 squareSystem (fun _ => 0)) = 2 := by
92   rw [← Nat.card_congr (PolynomialLiftCounts.digitEquivLifts 2 1 (by decide) (by decide)
93     squareSystem (fun _ => 0) (fun _ => 0)
94     (by ext i; norm_num [evalSystem, squareSystem]))]
95   exact singular_square_digit_count
96 
97 /-- There are four unrestricted roots of the zero equation modulo four.
98 The prescribed even lower residue retains only two of them. -/
99 theorem unrestricted_zero_root_count :
100     Nat.card {y : Fin 1 → ZMod 4 //
101       ∀ i, (4 : ℤ) ∣ eval (fun k => ((y k).val : ℤ)) (zeroSystem i)} = 4 := by
102   have h := Nat.card_congr (show {y : Fin 1 → ZMod 4 //
103       ∀ i, (4 : ℤ) ∣ eval (fun k => ((y k).val : ℤ)) (zeroSystem i)} ≃
104       (Fin 1 → ZMod 4) from {
105     toFun := Subtype.val
106     invFun t := ⟨t, by intro i; simp [zeroSystem]⟩
107     left_inv _ := rfl
108     right_inv _ := rfl })
109   simpa [Nat.card_fun, Nat.card_eq_fintype_card] using h
110 
111 end Komorebi.PolynomialCountControls

Back to source controls