ZeroGeometry.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.EntireBridge
6 import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
7 import Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
8 import Mathlib.Analysis.Analytic.Order
9 
10 /-! # Exact zero geometry and quantitative two-exponential cancellation
11 
12 This module begins the formalization of Section 11. The cancellation estimate
13 uses the principal logarithm near one and gives universal explicit constants.
14 -/
15 
16 namespace Komorebi.PaperIV
17 noncomputable section
18 
19 /-- The exact order-two denominator, independently of the choices of roots. -/
20 theorem entireSigned_two_eq_cos {omega rho : ℂ}
21     (homega : IsPrimitiveRoot omega 2) (hrho : rho ^ 2 = -1) (z : ℂ) :
22     entireSigned 2 0 omega rho z = Complex.cos z := by
23   rw [entireSigned_independent_roots (by decide) (by decide) homega
24     (IsPrimitiveRoot.neg_one 0 (by decide)) hrho Complex.I_sq,
25     entireSigned_zero_eq_average]
26   simp [Finset.sum_range_succ, Complex.cos, mul_comm]
27   ring
28 
29 /-- Every complex zero in order two, with no omitted exceptional zeros. -/
30 theorem entireSigned_two_zero_iff {omega rho z : ℂ}
31     (homega : IsPrimitiveRoot omega 2) (hrho : rho ^ 2 = -1) :
32     entireSigned 2 0 omega rho z = 0 ↔
33       ∃ k : ℤ, z = (2 * k + 1) * (Real.pi : ℂ) / 2 := by
34   rw [entireSigned_two_eq_cos homega hrho, Complex.cos_eq_zero_iff]
35 
36 /-- At every order-two zero the derivative is nonzero, hence the zero is simple. -/
37 theorem entireSigned_two_zero_derivative_ne_zero {omega rho z : ℂ}
38     (homega : IsPrimitiveRoot omega 2) (hrho : rho ^ 2 = -1)
39     (hz : entireSigned 2 0 omega rho z = 0) :
40     deriv (entireSigned 2 0 omega rho) z ≠ 0 := by
41   have he : entireSigned 2 0 omega rho = Complex.cos :=
42     funext (entireSigned_two_eq_cos homega hrho)
43   rw [he, Complex.deriv_cos]
44   rw [he] at hz
45   have hs : Complex.sin z ≠ 0 := by
46     intro hs
47     have h := Complex.sin_sq_add_cos_sq z
48     simp [hs, hz] at h
49   exact neg_ne_zero.mpr hs
50 
51 /-- The positive/negative natural-number parametrization used in the paper. -/
52 theorem entireSigned_two_zero_iff_nat {omega rho z : ℂ}
53     (homega : IsPrimitiveRoot omega 2) (hrho : rho ^ 2 = -1) :
54     entireSigned 2 0 omega rho z = 0 ↔
55       ∃ m : ℕ, z = ((m : ℂ) + 1 / 2) * (Real.pi : ℂ) ∨
56         z = -(((m : ℂ) + 1 / 2) * (Real.pi : ℂ)) := by
57   rw [entireSigned_two_zero_iff homega hrho]
58   constructor
59   · rintro ⟨k, rfl⟩
60     cases k with
61     | ofNat m =>
62       refine ⟨m, Or.inl ?_⟩
63       change (2 * (m : ℂ) + 1) * (Real.pi : ℂ) / 2 = ((m : ℂ) + 1 / 2) * (Real.pi : ℂ)
64       ring
65     | negSucc m =>
66       refine ⟨m, Or.inr ?_⟩
67       push_cast
68       ring
69   · rintro ⟨m, rfl | rfl⟩
70     · refine ⟨(m : ℤ), ?_⟩
71       push_cast
72       ring
73     · refine ⟨-(m : ℤ) - 1, ?_⟩
74       push_cast
75       ring
76 
77 /-- All order-two zeros have analytic multiplicity exactly one. -/
78 theorem entireSigned_two_zero_order_one {omega rho z : ℂ}
79     (homega : IsPrimitiveRoot omega 2) (hrho : rho ^ 2 = -1)
80     (hz : entireSigned 2 0 omega rho z = 0) :
81     analyticOrderAt (entireSigned 2 0 omega rho) z = 1 :=
82   (analyticAt_entireSigned 2 0 omega rho z).analyticOrderAt_eq_one_of_zero_deriv_ne_zero
83     hz (entireSigned_two_zero_derivative_ne_zero homega hrho hz)
84 
85 /-- The order-two lattice spacing is exactly pi. -/
86 theorem orderTwo_zero_spacing :
87     Real.pi / Real.sin (Real.pi / 2) = Real.pi := by simp
88 
89 /-- The centers of cancellation of two exponentials. -/
90 def oddExponentialCenter (k : ℤ) : ℂ := (2 * k + 1) * (Real.pi : ℂ) * Complex.I
91 
92 /-- A quantitative logarithmic inverse near any cancellation center. -/
93 theorem near_cancellation_exists {w : ℂ} (hw : ‖1 + Complex.exp w‖ ≤ 1 / 2) :
94     ∃ k : ℤ, ‖w - oddExponentialCenter k‖ ≤ (3 / 2 : ℝ) * ‖1 + Complex.exp w‖ := by
95   let u : ℂ := -(1 + Complex.exp w)
96   have hu : ‖u‖ ≤ 1 / 2 := by simpa only [u, norm_neg] using hw
97   have hlog := Complex.norm_log_one_add_half_le_self hu
98   have he : Complex.exp w =
99       Complex.exp (Complex.log (-Complex.exp w) + (Real.pi : ℂ) * Complex.I) := by
100     rw [Complex.exp_add, Complex.exp_log (neg_ne_zero.mpr (Complex.exp_ne_zero w)),
101       Complex.exp_pi_mul_I]
102     ring
103   obtain ⟨k, hk⟩ := Complex.exp_eq_exp_iff_exists_int.mp he
104   refine ⟨k, ?_⟩
105   have hd : w - oddExponentialCenter k = Complex.log (-Complex.exp w) := by
106     unfold oddExponentialCenter
107     linear_combination hk
108   rw [hd]
109   have heq : (1 : ℂ) + u = -Complex.exp w := by dsimp [u]; ring
110   rw [heq] at hlog
111   simpa only [u, norm_neg] using hlog
112 
113 /-- Distinct cancellation centers are separated by at least one full period. -/
114 theorem oddExponentialCenter_separation {k l : ℤ} (hkl : k ≠ l) :
115     2 * Real.pi ≤ ‖oddExponentialCenter k - oddExponentialCenter l‖ := by
116   have he : oddExponentialCenter k - oddExponentialCenter l =
117       (((2 * Real.pi * ((k - l : ℤ) : ℝ)) : ℝ) : ℂ) * Complex.I := by
118     push_cast
119     unfold oddExponentialCenter
120     ring
121   rw [he, norm_mul, Complex.norm_I, mul_one, Complex.norm_real,
122     Real.norm_eq_abs, abs_mul, abs_of_pos (by positivity : 0 < 2 * Real.pi)]
123   have hi : (1 : ℝ) ≤ |((k - l : ℤ) : ℝ)| := by
124     exact_mod_cast (Int.one_le_abs (sub_ne_zero.mpr hkl))
125   nlinarith [Real.pi_pos]
126 
127 /-- Lemma 11.6 with explicit universal constants: epsilon = 1/2 and C = 3/2.
128 No strip restriction is required. -/
129 theorem near_cancellation_unique {w : ℂ} (hw : ‖1 + Complex.exp w‖ ≤ 1 / 2) :
130     ∃! k : ℤ, ‖w - oddExponentialCenter k‖ ≤ (3 / 2 : ℝ) * ‖1 + Complex.exp w‖ := by
131   obtain ⟨k, hk⟩ := near_cancellation_exists hw
132   refine ⟨k, hk, ?_⟩
133   intro l hl
134   by_contra hne
135   have hsep := oddExponentialCenter_separation hne
136   have htri : ‖oddExponentialCenter l - oddExponentialCenter k‖ ≤
137       ‖w - oddExponentialCenter l‖ + ‖w - oddExponentialCenter k‖ := by
138     calc
139       _ = ‖-(w - oddExponentialCenter l) + (w - oddExponentialCenter k)‖ := by
140         congr 1
141         ring
142       _ ≤ _ := by simpa only [norm_neg] using
143         norm_add_le (-(w - oddExponentialCenter l)) (w - oddExponentialCenter k)
144   nlinarith [Real.two_le_pi]
145 
146 end
147 end Komorebi.PaperIV

Back to source controls