SignedGlobalExhaustion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedSectorExhaustion
6 
7 /-! # Rotation and global exhaustion of the large denominator zeros -/
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Metric
12 
13 /-- The actual entire denominator is invariant under every Nth root of unity. -/
14 theorem canonicalSignedDenominator_rotation {N : ℕ} (hN : 0 < N)
15     {u : ℂ} (hu : u ^ N = 1) (z : ℂ) :
16     canonicalSignedDenominator N (u * z) = canonicalSignedDenominator N z := by
17   have hleft := hasSum_entireSigned hN hN (canonicalPrimitiveRoot_isPrimitive hN)
18     (canonicalSignedRoot_pow hN) (u * z)
19   have hright := hasSum_entireSigned hN hN (canonicalPrimitiveRoot_isPrimitive hN)
20     (canonicalSignedRoot_pow hN) z
21   unfold canonicalSignedDenominator
22   apply hleft.unique
23   convert hright using 1
24   funext n
25   by_cases hn : n % N = 0
26   · have hp : u ^ n = 1 := by rw [pow_eq_pow_mod n hu, hn, pow_zero]
27     simp only [mul_pow, hp, one_mul]
28   · simp [coeff_signedSection, signedSectionCoeff, hn]
29 
30 /-- Polar angles between the two tie-sector boundaries satisfy the Cartesian
31 sector inequalities, with a uniform positive lower bound for the real part. -/
32 theorem signedFundamentalSector_polar {N : ℕ} (hN : 3 ≤ N)
33     {r θ : ℝ} (hr : 0 ≤ r) (hθ : |θ| ≤ Real.pi / N) :
34     signedFundamentalSector N ((r : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)) ∧
35       r * Real.cos (Real.pi / N) ≤
36         ((r : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)).re := by
37   let a := Real.pi / N
38   have hn : (3 : ℝ) ≤ N := by exact_mod_cast hN
39   have ha : 0 < a := div_pos Real.pi_pos (by linarith)
40   have he : a * N = Real.pi := div_mul_cancel₀ _ (by linarith)
41   have hap : a ≤ Real.pi := by nlinarith [Real.pi_pos]
42   have hc : Real.cos a ≤ Real.cos θ := by
43     have hh := Real.cos_le_cos_of_nonneg_of_le_pi (abs_nonneg θ) hap hθ
44     simpa only [Real.cos_abs] using hh
45   have hre : ((r : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)).re = r * Real.cos θ := by
46     rw [Complex.re_ofReal_mul, Complex.exp_ofReal_mul_I_re]
47   have him : ((r : ℂ) * Complex.exp ((θ : ℂ) * Complex.I)).im = r * Real.sin θ := by
48     rw [Complex.im_ofReal_mul, Complex.exp_ofReal_mul_I_im]
49   have hcos : 0 < Real.cos θ := lt_of_lt_of_le (signed_cosine_pos hN) hc
50   have hs : |Real.sin θ| * Real.cos a ≤ Real.cos θ * Real.sin a := by
51     have ht : |θ| ≤ Real.pi := hθ.trans hap
52     have hsin : |Real.sin θ| = Real.sin |θ| := by
53       by_cases hh : 0 ≤ θ
54       · rw [abs_of_nonneg hh, abs_of_nonneg (Real.sin_nonneg_of_mem_Icc ⟨hh, (abs_le.mp ht).2⟩)]
55       · rw [abs_of_neg (lt_of_not_ge hh), Real.sin_neg]
56         have hnθ : Real.sin θ ≤ 0 := by
57           have hh' := Real.sin_nonneg_of_mem_Icc ⟨(by linarith : 0 ≤ -θ), (by linarith [(abs_le.mp ht).1] : -θ ≤ Real.pi)⟩
58           rw [Real.sin_neg] at hh'
59           linarith
60         rw [abs_of_nonpos hnθ]
61     have hdiff := Real.sin_nonneg_of_mem_Icc (show a - |θ| ∈ Set.Icc 0 Real.pi by
62       constructor <;> linarith [abs_nonneg θ])
63     rw [Real.sin_sub, Real.cos_abs, ← hsin] at hdiff
64     nlinarith
65   refine ⟨⟨by rw [hre]; positivity, ?_⟩, ?_⟩
66   · rw [him, hre, abs_mul, abs_of_nonneg hr]
67     nlinarith [mul_le_mul_of_nonneg_left hs hr]
68   · rw [hre]
69     exact mul_le_mul_of_nonneg_left hc hr
70 
71 /-- Every complex number can be rotated into the fundamental sector by an
72 actual Nth root of unity. The rotated real part controls its original norm. -/
73 theorem exists_signed_sector_rotation {N : ℕ} (hN : 3 ≤ N) (z : ℂ) :
74     ∃ u : ℂ, u ^ N = 1 ∧ ‖u‖ = 1 ∧ signedFundamentalSector N (u * z) ∧
75       ‖z‖ * Real.cos (Real.pi / N) ≤ (u * z).re := by
76   let a : ℝ := Real.pi / N
77   have hn : (0 : ℝ) < N := by exact_mod_cast (show 0 < N by omega)
78   have ha : 0 < a := div_pos Real.pi_pos hn
79   obtain ⟨k, hk, _⟩ := existsUnique_add_zsmul_mem_Ioc (show 0 < 2 * a by positivity) z.arg (-a)
80   rw [zsmul_eq_mul] at hk
81   let θ := z.arg + (k : ℝ) * (2 * a)
82   have hθ : |θ| ≤ a := by
83     rcases hk with ⟨hlo, hhi⟩
84     apply abs_le.mpr
85     constructor <;> dsimp [θ] <;> linarith
86   let u := Complex.exp ((((k : ℝ) * (2 * a) : ℝ) : ℂ) * Complex.I)
87   have hu : u ^ N = 1 := by
88     dsimp [u]
89     rw [← Complex.exp_nat_mul]
90     have harg : (N : ℂ) * (((((k : ℝ) * (2 * a) : ℝ) : ℂ)) * Complex.I) =
91         (k : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) := by
92       dsimp [a]
93       push_cast
94       field_simp [show (N : ℂ) ≠ 0 by exact_mod_cast hn.ne']
95     rw [harg, Complex.exp_int_mul_two_pi_mul_I]
96   have hnorm : ‖u‖ = 1 := by dsimp [u]; exact Complex.norm_exp_ofReal_mul_I _
97   have hz : u * z = (‖z‖ : ℂ) * Complex.exp ((θ : ℂ) * Complex.I) := by
98     conv_lhs => rw [← Complex.norm_mul_exp_arg_mul_I z]
99     dsimp [u, θ]
100     rw [mul_left_comm, ← Complex.exp_add]
101     congr 2
102     push_cast
103     ring
104   have hsector := signedFundamentalSector_polar hN (norm_nonneg z) hθ
105   rw [← hz] at hsector
106   exact ⟨u, hu, hnorm, hsector.1, hsector.2⟩
107 
108 /-- Every sufficiently large zero is a rotation of one of the real simple
109 zeros constructed near the natural-index cancellation centers. -/
110 theorem canonicalSignedDenominator_global_exhaustion {N : ℕ} (hN : 3 ≤ N) (m0 : ℕ) :
111     ∃ R : ℝ, 0 < R ∧ ∀ z : ℂ, R ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
112       ∃ u : ℂ, ∃ m : ℕ, u ^ N = 1 ∧ ‖u‖ = 1 ∧ m0 ≤ m ∧
113         canonicalSignedDenominator N (u * z) = 0 ∧
114         u * z ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
115         (u * z).im = 0 ∧ 0 < (u * z).re ∧
116         analyticOrderAt (canonicalSignedDenominator N) (u * z) = 1 ∧
117         ∀ w : ℂ, w ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
118           canonicalSignedDenominator N w = 0 → w = u * z := by
119   obtain ⟨X, hX, hex⟩ := canonicalSignedDenominator_sector_exhaustion hN m0
120   have hc := signed_cosine_pos hN
121   refine ⟨X / Real.cos (Real.pi / N), div_pos hX hc, ?_⟩
122   intro z hz hz0
123   obtain ⟨u, hu, hunorm, hsector, hreal⟩ := exists_signed_sector_rotation hN z
124   have hx : X ≤ (u * z).re := ((div_le_iff₀ hc).mp hz).trans hreal
125   have hu0 : canonicalSignedDenominator N (u * z) = 0 := by
126     rw [canonicalSignedDenominator_rotation (by omega) hu, hz0]
127   obtain ⟨m, hm, hball, him, hpos, hs, huniq⟩ := hex (u * z) hsector hx hu0
128   exact ⟨u, m, hu, hunorm, hm, hu0, hball, him, hpos, hs, huniq⟩
129 
130 end
131 end Komorebi.PaperIV

Back to source controls