SignedSectorConfinement.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedZeroLocalization
6 
7 /-! # Exact confinement of zeros in the fundamental sector
8 
9 The two adjacent vertices are the largest two projections throughout the
10 fundamental sector. This gives a strip bound without an asymptotic hypothesis.
11 -/
12 
13 namespace Komorebi.PaperIV
14 noncomputable section
15 
16 /-- The closed fundamental sector, expressed without a choice of argument. -/
17 def signedFundamentalSector (N : ℕ) (z : ℂ) : Prop :=
18   0 ≤ z.re ∧ |z.im| * Real.cos (Real.pi / N) ≤ z.re * Real.sin (Real.pi / N)
19 
20 theorem signed_cosine_pos {N : ℕ} (hN : 3 ≤ N) : 0 < Real.cos (Real.pi / N) := by
21   have hn : (3 : ℝ) ≤ N := by exact_mod_cast hN
22   have hp : 0 < Real.pi / N := div_pos Real.pi_pos (by linarith)
23   have he : Real.pi / N * N = Real.pi := div_mul_cancel₀ _ (by linarith)
24   apply Real.cos_pos_of_mem_Ioo
25   constructor <;> nlinarith [Real.pi_pos]
26 
27 /-- Cosine on a closed arc avoiding zero is bounded by its endpoint value. -/
28 theorem cosine_arc_upper {a θ : ℝ} (ha : 0 ≤ a) (hlo : a ≤ θ)
29     (hhi : θ ≤ 2 * Real.pi - a) : Real.cos θ ≤ Real.cos a := by
30   by_cases hθ : θ ≤ Real.pi
31   · exact Real.cos_le_cos_of_nonneg_of_le_pi ha hθ hlo
32   · have hc := Real.cos_le_cos_of_nonneg_of_le_pi ha
33       (by linarith : 2 * Real.pi - θ ≤ Real.pi) (by linarith : a ≤ 2 * Real.pi - θ)
34     simpa only [Real.cos_two_pi_sub] using hc
35 
36 /-- A nonadjacent vertex cannot exceed the upper adjacent vertex on either
37 boundary of the upper half of the fundamental sector. -/
38 theorem canonicalSignedVertex_upper_boundary {N l : ℕ} (hN : 3 ≤ N)
39     (hl : l ∈ ((Finset.range N).erase 0).erase (N - 1)) :
40     (canonicalSignedVertex N l - canonicalSignedVertex N 0).re * Real.cos (Real.pi / N) -
41       (canonicalSignedVertex N l - canonicalSignedVertex N 0).im * Real.sin (Real.pi / N) ≤ 0 := by
42   have hi : 1 ≤ l ∧ l + 2 ≤ N := by
43     simp only [Finset.mem_erase, Finset.mem_range] at hl
44     omega
45   have hn : (3 : ℝ) ≤ N := by exact_mod_cast hN
46   have hl1 : (1 : ℝ) ≤ l := by exact_mod_cast hi.1
47   have hl2 : (l : ℝ) + 2 ≤ N := by exact_mod_cast hi.2
48   let a : ℝ := Real.pi / N
49   have hp : 0 < a := div_pos Real.pi_pos (by linarith)
50   have he : a * N = Real.pi := div_mul_cancel₀ _ (by linarith)
51   have hc := cosine_arc_upper (a := 2 * a) (θ := (2 * l + 1) * a + a)
52     (by positivity) (by nlinarith) (by nlinarith)
53   rw [Real.cos_add] at hc
54   have hdouble : Real.cos (2 * a) = Real.cos a * Real.cos a - Real.sin a * Real.sin a := by
55     rw [show 2 * a = a + a by ring, Real.cos_add]
56   rw [hdouble] at hc
57   simp only [Complex.sub_re, Complex.sub_im, canonicalSignedVertex_re,
58     canonicalSignedVertex_im, Nat.cast_zero, mul_zero, zero_add, one_mul]
59   change (Real.cos ((2 * l + 1) * a) - Real.cos a) * Real.cos a -
60     (Real.sin ((2 * l + 1) * a) - Real.sin a) * Real.sin a ≤ 0
61   nlinarith
62 
63 /-- Throughout the upper half sector every nonadjacent exponential is no
64 larger than the upper adjacent exponential. -/
65 theorem canonicalSignedVertex_upper_projection {N l : ℕ} (hN : 3 ≤ N)
66     (hl : l ∈ ((Finset.range N).erase 0).erase (N - 1))
67     {z : ℂ} (hz : signedFundamentalSector N z) (hy : 0 ≤ z.im) :
68     ((canonicalSignedVertex N l - canonicalSignedVertex N 0) * z).re ≤ 0 := by
69   let A := (canonicalSignedVertex N l - canonicalSignedVertex N 0).re
70   let B := (canonicalSignedVertex N l - canonicalSignedVertex N 0).im
71   let s := Real.sin (Real.pi / N)
72   let c := Real.cos (Real.pi / N)
73   have hs : 0 < s := signed_sine_pos (by omega)
74   have hA : A ≤ 0 := by
75     have hh := canonicalSignedVertex_re_gap hN hl
76     rw [Complex.sub_re, canonicalSignedVertex_last_re (by omega)] at hh
77     dsimp [A]
78     rw [canonicalSignedVertex_re N 0]
79     norm_num only [Nat.cast_zero, mul_zero, zero_add, one_mul]
80     linarith [signedPolygonGap_pos hN]
81   have hB : A * c - B * s ≤ 0 := canonicalSignedVertex_upper_boundary hN hl
82   have hw : 0 ≤ z.re * s - z.im * c := by
83     have hh := hz.2
84     rw [abs_of_nonneg hy] at hh
85     linarith
86   have h1 := mul_nonpos_of_nonpos_of_nonneg hA hw
87   have h2 := mul_nonpos_of_nonpos_of_nonneg hB hy
88   rw [Complex.mul_re]
89   change A * z.re - B * z.im ≤ 0
90   nlinarith
91 
92 /-- The lower adjacent vertex exceeds every other vertex by at least
93 `2 sin(pi/N) im(z)` on the upper half sector. -/
94 theorem canonicalSignedVertex_sector_gap {N l : ℕ} (hN : 3 ≤ N)
95     (hl : l ∈ (Finset.range N).erase (N - 1))
96     {z : ℂ} (hz : signedFundamentalSector N z) (hy : 0 ≤ z.im) :
97     ((canonicalSignedVertex N l - canonicalSignedVertex N (N - 1)) * z).re ≤
98       -(2 * Real.sin (Real.pi / N) * z.im) := by
99   have hd : ((canonicalSignedVertex N 0 - canonicalSignedVertex N (N - 1)) * z).re =
100       -(2 * Real.sin (Real.pi / N) * z.im) := by
101     have hzero : canonicalSignedVertex N 0 = canonicalSignedRoot N := by simp [canonicalSignedVertex]
102     rw [hzero, canonicalSignedVertex_adjacent_difference (by omega)]
103     simp only [Complex.mul_re, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im,
104       Complex.I_re, Complex.I_im, show (2 : ℂ).re = 2 from rfl,
105       show (2 : ℂ).im = 0 from rfl]
106     ring
107   by_cases hl0 : l = 0
108   · simpa only [hl0] using hd.le
109   · have hmem : l ∈ ((Finset.range N).erase 0).erase (N - 1) := by
110       simpa only [Finset.mem_erase] using ⟨(Finset.mem_erase.mp hl).1, hl0, (Finset.mem_erase.mp hl).2⟩
111     have hb := canonicalSignedVertex_upper_projection hN hmem hz hy
112     have he : ((canonicalSignedVertex N l - canonicalSignedVertex N (N - 1)) * z).re =
113         ((canonicalSignedVertex N l - canonicalSignedVertex N 0) * z).re +
114         ((canonicalSignedVertex N 0 - canonicalSignedVertex N (N - 1)) * z).re := by
115       rw [← Complex.add_re]; congr 1; ring
116     rw [he, hd]
117     linarith
118 
119 /-- Normalization by one exponential in a finite sum. -/
120 theorem finite_one_term_normalization {s : Finset ℕ} {a : ℕ → ℂ}
121     {k : ℕ} (hk : k ∈ s) (z : ℂ) :
122     Complex.exp (-(a k * z)) * (∑ l ∈ s, Complex.exp (a l * z)) =
123       1 + ∑ l ∈ s.erase k, Complex.exp ((a l - a k) * z) := by
124   rw [← Finset.sum_erase_add _ _ hk, mul_add, Finset.mul_sum]
125   have he (v : ℂ) : Complex.exp (-(a k * z)) * Complex.exp (v * z) =
126       Complex.exp ((v - a k) * z) := by rw [← Complex.exp_add]; congr 1; ring
127   simp only [he, sub_self, zero_mul, Complex.exp_zero]
128   ring
129 
130 /-- A zero must balance the modulus of the normalized dominant term. -/
131 theorem finite_exponential_zero_balance {s : Finset ℕ} {a : ℕ → ℂ}
132     {k : ℕ} (hk : k ∈ s) {z : ℂ} (hz : (∑ l ∈ s, Complex.exp (a l * z)) = 0)
133     {d : ℝ} (hgap : ∀ l ∈ s.erase k, ((a l - a k) * z).re ≤ -d) :
134     1 ≤ ((s.erase k).card : ℝ) * Real.exp (-d) := by
135   have he := finite_one_term_normalization (a := a) hk z
136   rw [hz, mul_zero] at he
137   have hs : (∑ l ∈ s.erase k, Complex.exp ((a l - a k) * z)) = -1 := by
138     linear_combination -he
139   calc
140     (1 : ℝ) = ‖∑ l ∈ s.erase k, Complex.exp ((a l - a k) * z)‖ := by rw [hs]; simp
141     _ ≤ ∑ l ∈ s.erase k, ‖Complex.exp ((a l - a k) * z)‖ := norm_sum_le _ _
142     _ ≤ ∑ _l ∈ s.erase k, Real.exp (-d) := Finset.sum_le_sum (fun l hl => by
143       rw [Complex.norm_exp]; exact Real.exp_le_exp.mpr (hgap l hl))
144     _ = _ := by simp
145 
146 /-- Explicit strip width for the signed denominator. -/
147 def signedSectorWidth (N : ℕ) : ℝ :=
148   Real.log ((N - 1 : ℕ) : ℝ) / (2 * Real.sin (Real.pi / N))
149 
150 theorem canonicalSignedDenominator_upper_sector_zero_bound {N : ℕ} (hN : 3 ≤ N)
151     {z : ℂ} (hz : signedFundamentalSector N z) (hy : 0 ≤ z.im)
152     (hz0 : canonicalSignedDenominator N z = 0) : z.im ≤ signedSectorWidth N := by
153   have hn : (N : ℂ) ≠ 0 := by exact_mod_cast (show N ≠ 0 by omega)
154   have hsum : (∑ l ∈ Finset.range N, Complex.exp (canonicalSignedVertex N l * z)) = 0 := by
155     unfold canonicalSignedDenominator at hz0
156     rw [entireSigned_zero_eq_average] at hz0
157     simpa only [canonicalSignedVertex, mul_eq_zero, inv_ne_zero hn, false_or] using hz0
158   have hb := finite_exponential_zero_balance
159     (k := N - 1) (Finset.mem_range.mpr (show N - 1 < N by omega)) hsum
160     (fun l hl => canonicalSignedVertex_sector_gap hN hl hz hy)
161   rw [Finset.card_erase_of_mem (Finset.mem_range.mpr (show N - 1 < N by omega)), Finset.card_range] at hb
162   have hC : (0 : ℝ) < ((N - 1 : ℕ) : ℝ) := by exact_mod_cast (show 0 < N - 1 by omega)
163   have he : Real.exp (2 * Real.sin (Real.pi / N) * z.im) ≤ ((N - 1 : ℕ) : ℝ) := by
164     have hm := mul_le_mul_of_nonneg_right hb (Real.exp_nonneg (2 * Real.sin (Real.pi / N) * z.im))
165     rw [mul_assoc (((N - 1 : ℕ) : ℝ)) (Real.exp _) (Real.exp _),
166       ← Real.exp_add, neg_add_cancel, Real.exp_zero, mul_one, one_mul] at hm
167     exact hm
168   apply (le_div_iff₀ (mul_pos (by norm_num) (signed_sine_pos (by omega)))).mpr
169   have hh := (Real.le_log_iff_exp_le hC).mpr he
170   nlinarith
171 
172 /-- Every zero in the closed fundamental sector lies in this fixed strip. -/
173 theorem canonicalSignedDenominator_sector_zero_bound {N : ℕ} (hN : 3 ≤ N)
174     {z : ℂ} (hz : signedFundamentalSector N z)
175     (hz0 : canonicalSignedDenominator N z = 0) : |z.im| ≤ signedSectorWidth N := by
176   by_cases hy : 0 ≤ z.im
177   · rw [abs_of_nonneg hy]
178     exact canonicalSignedDenominator_upper_sector_zero_bound hN hz hy hz0
179   · have hstar : signedFundamentalSector N (star z) := by
180       simpa [signedFundamentalSector] using hz
181     have hzero : canonicalSignedDenominator N (star z) = 0 := by
182       rw [canonicalSignedDenominator_conj (by omega), hz0, star_zero]
183     have hb := canonicalSignedDenominator_upper_sector_zero_bound hN hstar
184       (by change 0 ≤ -z.im; linarith) hzero
185     simpa [abs_of_neg (lt_of_not_ge hy)] using hb
186 
187 end
188 end Komorebi.PaperIV

Back to source controls