SignedSectorExhaustion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedSectorConfinement
6 
7 /-! # Exhaustion of the large zeros within the fundamental sector -/
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Metric
12 
13 theorem signedSectorWidth_pos {N : ℕ} (hN : 3 ≤ N) : 0 < signedSectorWidth N := by
14   apply div_pos (Real.log_pos _) (mul_pos (by norm_num) (signed_sine_pos (by omega)))
15   exact_mod_cast (show 1 < N - 1 by omega)
16 
17 /-- The canonical remainder is uniformly small on any fixed horizontal strip. -/
18 theorem signedRemainder_eventually_small_on_strip {N : ℕ} (hN : 3 ≤ N)
19     {Y ε : ℝ} (hY : 0 ≤ Y) (hε : 0 < ε) (q : ℕ) :
20     ∃ T : ℝ, 0 ≤ T ∧ ∀ z : ℂ, T ≤ z.re → |z.im| ≤ Y →
21       ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) q z‖ ≤ ε := by
22   obtain ⟨T, hT, hb⟩ := signedRemainder_eventually_small_on_disks hN hY hε q
23   refine ⟨T, hY.trans hT, ?_⟩
24   intro z hx hy
25   apply hb z.re hx z
26   rw [mem_closedBall, dist_eq_norm]
27   have he : z - (z.re : ℂ) = (z.im : ℂ) * Complex.I := by apply Complex.ext <;> simp
28   rw [he, norm_mul, Complex.norm_I, mul_one, Complex.norm_real, Real.norm_eq_abs]
29   exact hy
30 
31 /-- The integer cancellation centers in the perturbation theorem are real. -/
32 theorem signed_integer_center {N : ℕ} (hN : 2 ≤ N) (k : ℤ) :
33     oddExponentialCenter k / signedZeroFrequency N =
34       (((Real.pi / Real.sin (Real.pi / N)) * ((k : ℝ) + 1 / 2) : ℝ) : ℂ) := by
35   have hs : (Real.sin (Real.pi / N) : ℂ) ≠ 0 := by exact_mod_cast (signed_sine_pos hN).ne'
36   rw [signedZeroFrequency, canonicalSignedVertex_adjacent_difference (by omega)]
37   unfold oddExponentialCenter
38   push_cast
39   field_simp
40 
41 /-- Beyond an explicit existence threshold, every sector zero lies in one of
42 the already constructed natural-index disks, and is real and simple. -/
43 theorem canonicalSignedDenominator_sector_exhaustion {N : ℕ} (hN : 3 ≤ N) (m0 : ℕ) :
44     ∃ X : ℝ, 0 < X ∧ ∀ z : ℂ, signedFundamentalSector N z → X ≤ z.re →
45       canonicalSignedDenominator N z = 0 → ∃ m : ℕ, m0 ≤ m ∧
46         z ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
47         z.im = 0 ∧ 0 < z.re ∧ analyticOrderAt (canonicalSignedDenominator N) z = 1 ∧
48         ∀ w : ℂ, w ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
49           canonicalSignedDenominator N w = 0 → w = z := by
50   let a := signedZeroFrequency N
51   let r : ℝ := 1 / ‖a‖
52   let A : ℝ := Real.pi / Real.sin (Real.pi / N)
53   have ha : 0 < ‖a‖ := norm_pos_iff.mpr (signedZeroFrequency_ne_zero (by omega))
54   have hr : 0 < r := one_div_pos.mpr ha
55   have hA : 0 < A := div_pos Real.pi_pos (signed_sine_pos (by omega))
56   obtain ⟨T, hTr, hlocal⟩ := canonicalSignedDenominator_eventual_local_zero hN
57   obtain ⟨T0, hT0, hb0⟩ := signedRemainder_eventually_small_on_strip hN
58     (signedSectorWidth_pos hN).le (by norm_num : (0 : ℝ) < 1 / 2) 0
59   obtain ⟨T1, hT1, hb1⟩ := signedRemainder_eventually_small_on_strip hN
60     (signedSectorWidth_pos hN).le (div_pos ha (by norm_num : (0 : ℝ) < 4)) 1
61   let B := max T (A * ((m0 : ℝ) + 1 / 2))
62   let X := max (B + r) (max T0 T1) + 1
63   have hB : 0 < B := lt_of_lt_of_le (hr.trans_le hTr) (le_max_left _ _)
64   refine ⟨X, by dsimp [X]; have := le_max_left (B + r) (max T0 T1); linarith, ?_⟩
65   intro z hsector hx hz0
66   have hstrip := canonicalSignedDenominator_sector_zero_bound hN hsector hz0
67   have hxB : B + r < z.re := by
68     have := le_max_left (B + r) (max T0 T1)
69     dsimp [X] at hx
70     linarith
71   have hx0 : T0 ≤ z.re := by
72     have := le_max_right (B + r) (max T0 T1)
73     have := le_max_left T0 T1
74     dsimp [X] at hx
75     linarith
76   have hx1 : T1 ≤ z.re := by
77     have := le_max_right (B + r) (max T0 T1)
78     have := le_max_right T0 T1
79     dsimp [X] at hx
80     linarith
81   have h0 := hb0 z hx0 hstrip
82   have h1 := hb1 z hx1 hstrip
83   obtain ⟨k, hk, _⟩ := canonicalSignedDenominator_zero_lattice_distance hN hz0 h0
84   let t : ℝ := A * ((k : ℝ) + 1 / 2)
85   have hdist : ‖z - (t : ℂ)‖ ≤ r := by
86     rw [signed_integer_center (by omega)] at hk
87     apply hk.trans
88     change (3 / 2 : ℝ) * _ / ‖a‖ ≤ 1 / ‖a‖
89     apply div_le_div_of_nonneg_right _ ha.le
90     nlinarith
91   have ht : B < t := by
92     have hh := (Complex.abs_re_le_norm (z - (t : ℂ))).trans hdist
93     simp only [Complex.sub_re, Complex.ofReal_re] at hh
94     have := (abs_le.mp hh).2
95     linarith
96   have hk0 : 0 ≤ k := by
97     by_contra hh
98     have hk1 : (k : ℝ) ≤ -1 := by exact_mod_cast (show k ≤ -1 by omega)
99     have ht0 : 0 < t := hB.trans ht
100     dsimp [t] at ht0
101     nlinarith
102   let m : ℕ := k.toNat
103   have hkm : (m : ℝ) = k := by exact_mod_cast (Int.toNat_of_nonneg hk0)
104   have hcenter : signedZeroCenter N m = t := by
105     change A * ((m : ℝ) + 1 / 2) = A * ((k : ℝ) + 1 / 2)
106     rw [hkm]
107   have hm0 : m0 ≤ m := by
108     have hh := lt_of_le_of_lt (le_max_right T (A * ((m0 : ℝ) + 1 / 2))) ht
109     have hmm : (m0 : ℝ) < m := by dsimp [t] at hh; rw [← hkm] at hh; nlinarith
110     exact_mod_cast hmm.le
111   have hzball : z ∈ closedBall (signedZeroCenter N m : ℂ) r := by
112     simpa only [mem_closedBall, dist_eq_norm, hcenter] using hdist
113   obtain ⟨w, hw, hu⟩ := hlocal (signedZeroCenter N m)
114     (by rw [hcenter]; exact (le_max_left _ _).trans ht.le)
115     (signedZeroCenter_cancellation (by omega) m)
116   have hzw : z = w := hu z ⟨hzball, hz0⟩
117   have huz : ∀ v : ℂ, v ∈ closedBall (signedZeroCenter N m : ℂ) r ∧
118       canonicalSignedDenominator N v = 0 → v = z := by
119     intro v hv
120     exact (hu v hv).trans hzw.symm
121   refine ⟨m, hm0, hzball, canonicalSignedDenominator_unique_zero_real (by omega) hzball hz0 huz,
122     by linarith, canonicalSignedDenominator_local_zero_simple hN hz0 h0 h1, huz⟩
123 
124 end
125 end Komorebi.PaperIV

Back to source controls