SignedZeroSequence.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ReducedZeros
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Metric
10 
11 /-- A positive real zero in the fixed disk around the `m`th cancellation center. -/
12 def isLocalizedPositiveZero (N m : ℕ) (t : ℝ) : Prop :=
13   0 < t ∧ canonicalSignedDenominator N (t : ℂ) = 0 ∧
14     (t : ℂ) ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖)
15 
16 /-- An actual root is chosen when one exists; the default is used only before the proven tail. -/
17 def signedPositiveZero (N m : ℕ) : ℝ := by
18   classical
19   exact if h : ∃ t, isLocalizedPositiveZero N m t then h.choose else signedZeroCenter N m
20 
21 theorem signedPositiveZero_spec {N m : ℕ} (h : ∃ t, isLocalizedPositiveZero N m t) :
22     isLocalizedPositiveZero N m (signedPositiveZero N m) := by
23   unfold signedPositiveZero
24   rw [dite_eq_left h]
25   exact h.choose_spec
26 
27 theorem signedPositiveZero_eq_of_unique {N m : ℕ} {z : ℂ}
28     (hb : z ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖))
29     (hz : canonicalSignedDenominator N z = 0) (hi : z.im = 0) (hp : 0 < z.re)
30     (hu : ∀ w : ℂ, w ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
31       canonicalSignedDenominator N w = 0 → w = z) : (signedPositiveZero N m : ℂ) = z := by
32   have he : (z.re : ℂ) = z := by apply Complex.ext <;> simp [hi]
33   have hh : isLocalizedPositiveZero N m z.re := ⟨hp, he.symm ▸ hz, he.symm ▸ hb⟩
34   have hs := signedPositiveZero_spec ⟨z.re, hh⟩
35   exact hu _ ⟨hs.2.2, hs.2.1⟩
36 
37 /-- A fixed real sequence, rather than separate existential witnesses, realizes the local strings. -/
38 theorem signedPositiveZero_local_strings {N : ℕ} (hN : 3 ≤ N) :
39     ∃ C : ℝ, 0 < C ∧ ∃ m0 : ℕ, ∀ m ≥ m0,
40       isLocalizedPositiveZero N m (signedPositiveZero N m) ∧
41       analyticOrderAt (canonicalSignedDenominator N) (signedPositiveZero N m : ℂ) = 1 ∧
42       |signedPositiveZero N m - signedZeroCenter N m| ≤
43         C * Real.exp (-signedPolygonGap N * signedZeroCenter N m) ∧
44       ∀ w : ℂ, w ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
45         canonicalSignedDenominator N w = 0 → w = (signedPositiveZero N m : ℂ) := by
46   obtain ⟨C, hC, m0, hm0⟩ := canonicalSignedDenominator_local_strings hN
47   refine ⟨C, hC, m0, ?_⟩
48   intro m hm
49   obtain ⟨z, hb, hz, hi, hp, ho, he, hu⟩ := hm0 m hm
50   have hroot := signedPositiveZero_eq_of_unique hb hz hi hp hu
51   have hr : signedPositiveZero N m = z.re := by simpa using congrArg Complex.re hroot
52   refine ⟨⟨by rw [hr]; exact hp, by rw [hroot]; exact hz, by rw [hroot]; exact hb⟩,
53     by rw [hroot]; exact ho, ?_, ?_⟩
54   · rw [← hroot, ← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs] at he
55     exact he
56   · intro w hw; rw [hroot]; exact hu w hw
57 
58 /-- The real sequence exhausts all large zeros after root-of-unity rotation. -/
59 theorem signedPositiveZero_global_strings {N : ℕ} (hN : 3 ≤ N) :
60     ∃ m0 : ℕ, ∃ R : ℝ, 0 < R ∧ ∀ z : ℂ, R ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
61       ∃ k < N, ∃ m ≥ m0, canonicalPrimitiveRoot N ^ k * z = (signedPositiveZero N m : ℂ) := by
62   obtain ⟨C, _, m0, hm0⟩ := signedPositiveZero_local_strings hN
63   obtain ⟨R, hR, hex⟩ := canonicalSignedDenominator_large_zero_orbits hN m0
64   refine ⟨m0, R, hR, ?_⟩
65   intro z hz hz0
66   obtain ⟨k, hk, m, hm, hb, _, _, _⟩ := hex z hz hz0
67   have hu : (canonicalPrimitiveRoot N ^ k) ^ N = 1 := by
68     rw [← pow_mul, Nat.mul_comm, pow_mul, (canonicalPrimitiveRoot_isPrimitive (by omega)).pow_eq_one, one_pow]
69   refine ⟨k, hk, m, hm, (hm0 m hm).2.2.2 _ ⟨hb, ?_⟩⟩
70   rw [canonicalSignedDenominator_rotation (by omega) hu]; exact hz0
71 
72 theorem signedZeroCenter_ge_radius {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
73     1 / ‖signedZeroFrequency N‖ ≤ signedZeroCenter N m := by
74   rw [signedZeroFrequency_norm hN, signedZeroCenter]
75   have hs := signed_sine_pos hN
76   have hm : (0 : ℝ) ≤ m := Nat.cast_nonneg m
77   apply (div_le_iff₀ (mul_pos (by norm_num) hs)).mpr
78   have he : Real.pi / Real.sin (Real.pi / N) * ((m : ℝ) + 1 / 2) *
79       (2 * Real.sin (Real.pi / N)) = Real.pi * (2 * m + 1) := by field_simp
80   rw [he]
81   nlinarith [Real.two_le_pi]
82 
83 theorem signedPositiveZero_pos {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
84     0 < signedPositiveZero N m := by
85   classical
86   by_cases h : ∃ t, isLocalizedPositiveZero N m t
87   · exact (signedPositiveZero_spec h).1
88   · rw [signedPositiveZero, dite_eq_right h]
89     exact lt_of_lt_of_le (one_div_pos.mpr (norm_pos_iff.mpr (signedZeroFrequency_ne_zero hN)))
90       (signedZeroCenter_ge_radius hN m)
91 
92 /-- Distinct lattice disks give distinct real zeros. -/
93 theorem signedPositiveZero_injective_on_tail {N : ℕ} (hN : 3 ≤ N) :
94     ∃ m0 : ℕ, Set.InjOn (signedPositiveZero N) (Set.Ici m0) := by
95   obtain ⟨C, _, m0, hm0⟩ := signedPositiveZero_local_strings hN
96   refine ⟨m0, ?_⟩
97   intro m hm n hn he
98   apply signedZeroCenter_disk_index_unique (by omega : 2 ≤ N) (hm0 m hm).1.2.2
99   rw [he]
100   exact (hm0 n hn).1.2.2
101 
102 /-- The reduced zero sequence is the actual `N`th power of the positive denominator zero. -/
103 def reducedPositiveZero (N m : ℕ) : ℝ := signedPositiveZero N m ^ N
104 
105 /-- Every sufficiently large reduced zero is an entry of the fixed power sequence. -/
106 theorem reducedPositiveZero_global_strings {N : ℕ} (hN : 3 ≤ N) :
107     ∃ m0 : ℕ, ∃ R : ℝ, 0 < R ∧ ∀ w : ℂ, R ≤ ‖w‖ → entireReducedDenominator N w = 0 →
108       ∃ m ≥ m0, w = (reducedPositiveZero N m : ℂ) := by
109   obtain ⟨m0, R, hR, hex⟩ := signedPositiveZero_global_strings hN
110   refine ⟨m0, R ^ N, pow_pos hR N, ?_⟩
111   intro w hw hw0
112   obtain ⟨z, hz⟩ := exists_complex_nth_root (by omega : 0 < N) w
113   have hr : R ≤ ‖z‖ := by
114     by_contra h
115     have hp := pow_lt_pow_left₀ (lt_of_not_ge h) (norm_nonneg z) (by omega : N ≠ 0)
116     have hn : ‖z‖ ^ N = ‖w‖ := by rw [← norm_pow, hz]
117     linarith
118   have hd : canonicalSignedDenominator N z = 0 := by
119     rw [canonicalSignedDenominator_eq_reduced_power (by omega), hz]; exact hw0
120   obtain ⟨k, _, m, hm, he⟩ := hex z hr hd
121   have hu : (canonicalPrimitiveRoot N ^ k) ^ N = 1 := by
122     rw [← pow_mul, Nat.mul_comm, pow_mul, (canonicalPrimitiveRoot_isPrimitive (by omega)).pow_eq_one, one_pow]
123   refine ⟨m, hm, ?_⟩
124   have hh := congrArg (fun x : ℂ => x ^ N) he
125   simpa only [mul_pow, hu, one_mul, hz, reducedPositiveZero, Complex.ofReal_pow] using hh
126 
127 theorem reducedPositiveZero_injective_on_tail {N : ℕ} (hN : 3 ≤ N) :
128     ∃ m0 : ℕ, Set.InjOn (reducedPositiveZero N) (Set.Ici m0) := by
129   obtain ⟨m0, hm0⟩ := signedPositiveZero_injective_on_tail hN
130   refine ⟨m0, ?_⟩
131   intro m hm n hn he
132   apply hm0 hm hn
133   exact (pow_left_strictMonoOn₀ (by omega : N ≠ 0)).injOn
134     (le_of_lt (signedPositiveZero_pos (by omega) m))
135     (le_of_lt (signedPositiveZero_pos (by omega) n)) he
136 
137 /-- Quantitative reduced-zero displacement, including the polynomial loss in the power map. -/
138 theorem reducedPositiveZero_local_strings {N : ℕ} (hN : 3 ≤ N) :
139     ∃ C : ℝ, 0 < C ∧ ∃ m0 : ℕ, ∀ m ≥ m0,
140       0 < reducedPositiveZero N m ∧
141       entireReducedDenominator N (reducedPositiveZero N m : ℂ) = 0 ∧
142       analyticOrderAt (entireReducedDenominator N) (reducedPositiveZero N m : ℂ) = 1 ∧
143       |reducedPositiveZero N m - signedZeroCenter N m ^ N| ≤
144         C * signedZeroCenter N m ^ (N - 1) * Real.exp (-signedPolygonGap N * signedZeroCenter N m) := by
145   obtain ⟨C, hC, m0, hm0⟩ := signedPositiveZero_local_strings hN
146   refine ⟨C * N * 2 ^ (N - 1), by positivity, m0, ?_⟩
147   intro m hm
148   obtain ⟨hs, ho, he, _⟩ := hm0 m hm
149   have ht : 0 < signedZeroCenter N m := by
150     exact lt_of_lt_of_le (one_div_pos.mpr (norm_pos_iff.mpr (signedZeroFrequency_ne_zero (by omega))))
151       (signedZeroCenter_ge_radius (by omega) m)
152   have hb : |signedPositiveZero N m - signedZeroCenter N m| ≤ 1 / ‖signedZeroFrequency N‖ := by
153     simpa only [mem_closedBall, dist_eq_norm, ← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs] using hs.2.2
154   have hu : signedPositiveZero N m ≤ 2 * signedZeroCenter N m := by
155     have hh := (le_abs_self (signedPositiveZero N m - signedZeroCenter N m)).trans hb
156     have hr := signedZeroCenter_ge_radius (by omega : 2 ≤ N) m
157     linarith
158   refine ⟨pow_pos hs.1 N, ?_, ?_, ?_⟩
159   · rw [reducedPositiveZero, Complex.ofReal_pow, ← canonicalSignedDenominator_eq_reduced_power (by omega)]
160     exact hs.2.1
161   · rw [reducedPositiveZero, Complex.ofReal_pow,
162       ← canonicalSignedDenominator_order_eq_reduced (by omega) (Complex.ofReal_ne_zero.mpr (ne_of_gt hs.1))]
163     exact ho
164   · calc
165       _ ≤ |signedPositiveZero N m - signedZeroCenter N m| * N *
166           max |signedPositiveZero N m| |signedZeroCenter N m| ^ (N - 1) := abs_pow_sub_pow_le _ _ _
167       _ ≤ (C * Real.exp (-signedPolygonGap N * signedZeroCenter N m)) * N *
168           (2 * signedZeroCenter N m) ^ (N - 1) := by
169         gcongr
170         rw [abs_of_pos hs.1, abs_of_pos ht]
171         exact max_le hu (by linarith)
172       _ = _ := by rw [mul_pow]; ring
173 
174 end
175 end Komorebi.PaperIV

Back to source controls