ZeroEnumeration.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.WeightedZeroCounts
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Metric
10 
11 /-- A positive simple tail, proved below to exist, with all large complex zeros
12 accounted for by its finite root-of-unity orbits. -/
13 structure SignedZeroEnumeration (N : ℕ) where
14   root : ℕ → ℝ
15   positive : ∀ m, 0 < root m
16   zero : ∀ m, canonicalSignedDenominator N (root m : ℂ) = 0
17   simple : ∀ m, analyticOrderAt (canonicalSignedDenominator N) (root m : ℂ) = 1
18   injective : Function.Injective root
19   shift : ℕ
20   windows : ∀ m, (Real.pi / Real.sin (Real.pi / N)) * m ≤ root m ∧
21     root m ≤ (Real.pi / Real.sin (Real.pi / N)) * ((m : ℝ) + shift)
22   offset : ℕ
23   displacement : ∃ C : ℝ, 0 < C ∧ ∃ γ : ℝ, 0 < γ ∧ ∀ m,
24     |root m - signedZeroCenter N (m + offset)| ≤ C * Real.exp (-γ * signedZeroCenter N (m + offset))
25   radius : ℝ
26   radius_pos : 0 < radius
27   exhaustive : ∀ z : ℂ, radius ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
28     ∃ k : Fin N, ∃ m : ℕ, z = canonicalPrimitiveRoot N ^ k.val * (root m : ℂ)
29 
30 theorem signedZeroEnumeration_exists_ge_three {N : ℕ} (hN : 3 ≤ N) :
31     Nonempty (SignedZeroEnumeration N) := by
32   let : NeZero N := ⟨by omega⟩
33   have hn : 0 < N := by omega
34   have homega := canonicalPrimitiveRoot_isPrimitive hn
35   obtain ⟨C, hC, M, hM⟩ := signedPositiveZero_local_strings hN
36   obtain ⟨R, hR, hex⟩ := canonicalSignedDenominator_large_zero_orbits hN M
37   refine ⟨{ root := fun m => signedPositiveZero N (m + M)
38             positive := fun m => (hM (m + M) (by omega)).1.1
39             zero := fun m => (hM (m + M) (by omega)).1.2.1
40             simple := fun m => (hM (m + M) (by omega)).2.1
41             injective := ?_
42             shift := M + 1
43             windows := ?_
44             offset := M
45             displacement := ⟨C, hC, signedPolygonGap N, signedPolygonGap_pos hN,
46               fun m => (hM (m + M) (by omega)).2.2.1⟩
47             radius := R
48             radius_pos := hR
49             exhaustive := ?_ }⟩
50   · intro m n h
51     change signedPositiveZero N (m + M) = signedPositiveZero N (n + M) at h
52     have he : m + M = n + M := by
53       apply signedZeroCenter_disk_index_unique (by omega : 2 ≤ N) (hM (m + M) (by omega)).1.2.2
54       rw [h]
55       exact (hM (n + M) (by omega)).1.2.2
56     omega
57   · intro m
58     have hb := (hM (m + M) (by omega)).1.2.2
59     have he : |signedPositiveZero N (m + M) - signedZeroCenter N (m + M)| ≤
60         1 / ‖signedZeroFrequency N‖ := by
61       simpa only [mem_closedBall, dist_eq_norm, ← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs] using hb
62     have hr := signedZeroCenter_ge_radius (by omega : 2 ≤ N) 0
63     have hA : 0 < Real.pi / Real.sin (Real.pi / N) := div_pos Real.pi_pos (signed_sine_pos (by omega))
64     have hM0 : (0 : ℝ) ≤ M := Nat.cast_nonneg M
65     rw [abs_le] at he
66     simp only [signedZeroCenter, Nat.cast_zero, zero_add] at hr
67     simp only [signedZeroCenter, Nat.cast_add, Nat.cast_one] at he ⊢
68     constructor <;> nlinarith
69   · intro z hz hz0
70     obtain ⟨k, _, m, hm, hb, _, _, _⟩ := hex z hz hz0
71     have hu : (canonicalPrimitiveRoot N ^ k) ^ N = 1 := by
72       rw [← pow_mul, Nat.mul_comm, pow_mul, homega.pow_eq_one, one_pow]
73     have he := (hM m hm).2.2.2 (canonicalPrimitiveRoot N ^ k * z)
74       ⟨hb, by rw [canonicalSignedDenominator_rotation hn hu]; exact hz0⟩
75     have hui : ((canonicalPrimitiveRoot N ^ k)⁻¹) ^ N = 1 := by rw [inv_pow, hu, inv_one]
76     obtain ⟨j, hj, hjinv⟩ := homega.eq_pow_of_pow_eq_one hui
77     have hu0 : canonicalPrimitiveRoot N ^ k ≠ 0 := by intro h; simp [h, hn.ne'] at hu
78     refine ⟨⟨j, hj⟩, m - M, ?_⟩
79     rw [Nat.sub_add_cancel hm, ← he, hjinv, ← mul_assoc, inv_mul_cancel₀ hu0, one_mul]
80 
81 theorem signedZeroEnumeration_exists_two : Nonempty (SignedZeroEnumeration 2) := by
82   have homega := canonicalPrimitiveRoot_isPrimitive (by norm_num : 0 < 2)
83   have hrho := canonicalSignedRoot_pow (by norm_num : 0 < 2)
84   have hz : ∀ m : ℕ, canonicalSignedDenominator 2 ((Real.pi * ((m : ℝ) + 1 / 2) : ℝ) : ℂ) = 0 := by
85     intro m
86     apply (entireSigned_two_zero_iff_nat homega hrho).mpr
87     refine ⟨m, Or.inl ?_⟩
88     push_cast
89     ring
90   refine ⟨{ root := fun m => Real.pi * ((m : ℝ) + 1 / 2)
91             positive := fun m => by positivity
92             zero := hz
93             simple := fun m => entireSigned_two_zero_order_one homega hrho (hz m)
94             injective := ?_
95             shift := 1
96             windows := ?_
97             offset := 0
98             displacement := ⟨1, by norm_num, 1, by norm_num, fun m => by
99               simp only [Nat.add_zero, signedZeroCenter, Nat.cast_ofNat, Real.sin_pi_div_two,
100                 div_one, sub_self, abs_zero, neg_mul, one_mul]
101               exact (Real.exp_pos _).le⟩
102             radius := 1
103             radius_pos := by norm_num
104             exhaustive := ?_ }⟩
105   · intro m n h
106     have he := mul_left_cancel₀ Real.pi_ne_zero h
107     exact_mod_cast (add_right_cancel he)
108   · intro m
109     simp only [Nat.cast_ofNat, Real.sin_pi_div_two, div_one, Nat.cast_one]
110     constructor <;> nlinarith [Real.pi_pos]
111   · intro z _ hz0
112     obtain ⟨m, hm | hm⟩ := (entireSigned_two_zero_iff_nat homega hrho).mp hz0
113     · refine ⟨⟨0, by omega⟩, m, ?_⟩
114       simp only [pow_zero, one_mul]
115       rw [hm]; push_cast; ring
116     · refine ⟨⟨1, by omega⟩, m, ?_⟩
117       simp only [pow_one, homega.eq_neg_one_of_two_right]
118       rw [hm]; push_cast; ring
119 
120 /-- No enumeration or zero-counting certificate is assumed. -/
121 theorem signedZeroEnumeration_exists {N : ℕ} (hN : 2 ≤ N) :
122     Nonempty (SignedZeroEnumeration N) := by
123   rcases eq_or_lt_of_le hN with h | h
124   · subst N; exact signedZeroEnumeration_exists_two
125   · exact signedZeroEnumeration_exists_ge_three (by omega)
126 
127 def canonicalZeroEnumeration {N : ℕ} (hN : 2 ≤ N) : SignedZeroEnumeration N :=
128   Classical.choice (signedZeroEnumeration_exists hN)
129 
130 def SignedZeroEnumeration.orbit {N : ℕ} (e : SignedZeroEnumeration N) (p : Fin N × ℕ) : ℂ :=
131   canonicalPrimitiveRoot N ^ p.1.val * (e.root p.2 : ℂ)
132 
133 theorem SignedZeroEnumeration.orbit_norm {N : ℕ} (hN : 0 < N) (e : SignedZeroEnumeration N)
134     (p : Fin N × ℕ) : ‖e.orbit p‖ = e.root p.2 := by
135   rw [SignedZeroEnumeration.orbit, norm_mul, norm_pow,
136     (canonicalPrimitiveRoot_isPrimitive hN).norm'_eq_one hN.ne', one_pow, one_mul,
137     Complex.norm_real, Real.norm_eq_abs, abs_of_pos (e.positive _)]
138 
139 theorem SignedZeroEnumeration.orbit_injective {N : ℕ} (hN : 0 < N) (e : SignedZeroEnumeration N) :
140     Function.Injective e.orbit := by
141   intro p q hpq
142   have hm : p.2 = q.2 := e.injective (by
143     have hh := congrArg norm hpq
144     rwa [e.orbit_norm hN, e.orbit_norm hN] at hh)
145   have hp : p.1 = q.1 := by
146     apply Fin.ext
147     apply (canonicalPrimitiveRoot_isPrimitive hN).pow_inj p.1.isLt q.1.isLt
148     unfold SignedZeroEnumeration.orbit at hpq
149     rw [hm] at hpq
150     exact mul_right_cancel₀ (Complex.ofReal_ne_zero.mpr (ne_of_gt (e.positive _))) hpq
151   exact Prod.ext hp hm
152 
153 theorem SignedZeroEnumeration.orbit_zero_simple {N : ℕ} (hN : 0 < N)
154     (e : SignedZeroEnumeration N) (p : Fin N × ℕ) :
155     canonicalSignedDenominator N (e.orbit p) = 0 ∧
156       analyticOrderNatAt (canonicalSignedDenominator N) (e.orbit p) = 1 := by
157   have hu : (canonicalPrimitiveRoot N ^ p.1.val) ^ N = 1 := by
158     rw [← pow_mul, Nat.mul_comm, pow_mul, (canonicalPrimitiveRoot_isPrimitive hN).pow_eq_one, one_pow]
159   constructor
160   · rw [SignedZeroEnumeration.orbit, canonicalSignedDenominator_rotation hN hu]; exact e.zero _
161   · rw [analyticOrderNatAt, SignedZeroEnumeration.orbit,
162       ← canonicalSignedDenominator_order_rotation hN hu, e.simple]
163     rfl
164 
165 end
166 end Komorebi.PaperIV

Back to source controls