LargeZeroCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroEnumeration
6 import KomorebiPaperIV.SignedDerivativeAsymptotics
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Metric Set
11 
12 /-- The derivative error is measured at the actual zero, with the same
13 exponential rate as in the manuscript, rather than only at its lattice center. -/
14 theorem signedPositiveZero_derivative_asymptotic {N : ℕ} (hN : 3 ≤ N) :
15     ∃ C : ℝ, 0 < C ∧ ∃ M : ℕ, ∀ m ≥ M,
16       |‖deriv (canonicalSignedDenominator N) (signedPositiveZero N m : ℂ)‖ /
17         ((2 * Real.sin (Real.pi / N) / N) *
18           Real.exp (Real.cos (Real.pi / N) * signedPositiveZero N m)) - 1| ≤
19         C * Real.exp (-signedPolygonGap N * signedPositiveZero N m) := by
20   obtain ⟨C0, _, M, hM⟩ := signedPositiveZero_local_strings hN
21   let B := (‖signedZeroFrequency N‖ + 2) / ‖signedZeroFrequency N‖
22   let S := signedRemainderScale N
23   let r := 1 / ‖signedZeroFrequency N‖
24   have hB : 0 < B := div_pos (by positivity) (norm_pos_iff.mpr (signedZeroFrequency_ne_zero (by omega)))
25   have hS : 0 < S := by
26     have h := signedRemainderEnvelope_pos hN 0
27     simpa only [signedRemainderEnvelope, mul_zero, Real.exp_zero, mul_one] using h
28   refine ⟨B * S * Real.exp (signedPolygonGap N * r), by positivity, M, ?_⟩
29   intro m hm
30   have hx := (hM m hm).1
31   have hbound := canonicalSignedDenominator_derivative_modulus_error hN
32     (signedZeroCenter_ge_radius (by omega) m) hx.2.2 hx.2.1
33   have hdelta : signedPositiveZero N m - signedZeroCenter N m ≤ r := by
34     have hb : |signedPositiveZero N m - signedZeroCenter N m| ≤ r := by
35       simpa only [mem_closedBall, dist_eq_norm, ← Complex.ofReal_sub, Complex.norm_real,
36         Real.norm_eq_abs] using hx.2.2
37     exact (le_abs_self _).trans hb
38   have hg : 0 < signedPolygonGap N := signedPolygonGap_pos hN
39   have he : Real.exp (-signedPolygonGap N * signedZeroCenter N m) ≤
40       Real.exp (signedPolygonGap N * r) *
41         Real.exp (-signedPolygonGap N * signedPositiveZero N m) := by
42     rw [← Real.exp_add]
43     apply Real.exp_le_exp.mpr
44     nlinarith
45   calc
46     _ ≤ B * (S * Real.exp (-signedPolygonGap N * signedZeroCenter N m)) := hbound
47     _ ≤ B * (S * (Real.exp (signedPolygonGap N * r) *
48         Real.exp (-signedPolygonGap N * signedPositiveZero N m))) := by gcongr
49     _ = _ := by ring
50 
51 /-- Unique root-of-unity orbit and lattice index for every sufficiently large
52 zero, with one fixed cutoff for the named sequence. -/
53 theorem signedPositiveZero_unique_global_strings {N : ℕ} (hN : 3 ≤ N) (K : ℕ) :
54     ∃ M : ℕ, K ≤ M ∧ ∃ R : ℝ, 0 < R ∧ ∀ z : ℂ, R ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
55       ∃! p : {p : Fin N × ℕ // M ≤ p.2},
56         z = canonicalPrimitiveRoot N ^ p.val.1.val * (signedPositiveZero N p.val.2 : ℂ) := by
57   let : NeZero N := ⟨by omega⟩
58   have hn : 0 < N := by omega
59   have homega := canonicalPrimitiveRoot_isPrimitive hn
60   obtain ⟨C, _, M0, hM0⟩ := signedPositiveZero_local_strings hN
61   let M := max M0 K
62   have hM (m : ℕ) (hm : M ≤ m) := hM0 m (le_trans (le_max_left M0 K) hm)
63   obtain ⟨R, hR, hex⟩ := canonicalSignedDenominator_large_zero_orbits hN M
64   have hinj : Set.InjOn (signedPositiveZero N) (Ici M) := by
65     intro m hm n hn he
66     apply signedZeroCenter_disk_index_unique (by omega) (hM m hm).1.2.2
67     rw [he]
68     exact (hM n hn).1.2.2
69   refine ⟨M, le_max_right M0 K, R, hR, ?_⟩
70   intro z hz hz0
71   obtain ⟨k, _, m, hm, hb, _, _, _⟩ := hex z hz hz0
72   have hu : (canonicalPrimitiveRoot N ^ k) ^ N = 1 := by
73     rw [← pow_mul, Nat.mul_comm, pow_mul, homega.pow_eq_one, one_pow]
74   have he := (hM m hm).2.2.2 (canonicalPrimitiveRoot N ^ k * z)
75     ⟨hb, by rw [canonicalSignedDenominator_rotation hn hu]; exact hz0⟩
76   have hui : ((canonicalPrimitiveRoot N ^ k)⁻¹) ^ N = 1 := by rw [inv_pow, hu, inv_one]
77   obtain ⟨j, hj, hjinv⟩ := homega.eq_pow_of_pow_eq_one hui
78   have hu0 : canonicalPrimitiveRoot N ^ k ≠ 0 := by intro h; simp [h, hn.ne'] at hu
79   have hzrep : z = canonicalPrimitiveRoot N ^ j * (signedPositiveZero N m : ℂ) := by
80     rw [← he, hjinv, ← mul_assoc, inv_mul_cancel₀ hu0, one_mul]
81   refine ⟨⟨(⟨j, hj⟩, m), hm⟩, hzrep, ?_⟩
82   intro p hp
83   have heq : canonicalPrimitiveRoot N ^ p.val.1.val * (signedPositiveZero N p.val.2 : ℂ) =
84       canonicalPrimitiveRoot N ^ j * (signedPositiveZero N m : ℂ) := hp.symm.trans hzrep
85   have hnorm := congrArg norm heq
86   simp only [norm_mul, norm_pow, homega.norm'_eq_one hn.ne', one_pow, one_mul,
87     Complex.norm_real, Real.norm_eq_abs, abs_of_pos (signedPositiveZero_pos (N := N) (by omega) _)] at hnorm
88   have hmidx : p.val.2 = m := hinj p.property hm hnorm
89   have hkidx : p.val.1.val = j := by
90     apply homega.pow_inj p.val.1.isLt hj
91     rw [hmidx] at heq
92     exact mul_right_cancel₀ (Complex.ofReal_ne_zero.mpr (ne_of_gt (signedPositiveZero_pos (by omega) m))) heq
93   apply Subtype.ext
94   exact Prod.ext (Fin.ext hkidx) hmidx
95 
96 /-- The exact derivative covariance at each named zero. -/
97 theorem signedPositiveZero_derivative_rotation {N : ℕ} (hN : 2 ≤ N) (k m : ℕ) :
98     deriv (canonicalSignedDenominator N)
99       (canonicalPrimitiveRoot N ^ k * (signedPositiveZero N m : ℂ)) =
100       (canonicalPrimitiveRoot N ^ k)⁻¹ *
101         deriv (canonicalSignedDenominator N) (signedPositiveZero N m : ℂ) := by
102   have hn : 0 < N := by omega
103   have hu : (canonicalPrimitiveRoot N ^ k) ^ N = 1 := by
104     rw [← pow_mul, Nat.mul_comm, pow_mul, (canonicalPrimitiveRoot_isPrimitive hn).pow_eq_one, one_pow]
105   have h := canonicalSignedDenominator_derivative_rotation hn hu (signedPositiveZero N m : ℂ)
106   have hu0 : canonicalPrimitiveRoot N ^ k ≠ 0 := by intro h; simp [h, hn.ne'] at hu
107   apply (mul_right_cancel₀ hu0)
108   rw [h]
109   field_simp
110 
111 /-- The complete large-zero statement: one tail cutoff, unique global orbit
112 indices, actual-zero displacement, derivative covariance, and the derivative
113 modulus estimate at the actual zero. All constants are derived. -/
114 theorem canonicalSignedDenominator_large_zero_strings {N : ℕ} (hN : 3 ≤ N) :
115     0 < signedPolygonGap N ∧ ∃ M : ℕ, ∃ C : ℝ, 0 < C ∧ ∃ B : ℝ, 0 < B ∧ ∃ R : ℝ, 0 < R ∧
116       (∀ m ≥ M, isLocalizedPositiveZero N m (signedPositiveZero N m) ∧
117         analyticOrderAt (canonicalSignedDenominator N) (signedPositiveZero N m : ℂ) = 1 ∧
118         |signedPositiveZero N m - signedZeroCenter N m| ≤
119           C * Real.exp (-signedPolygonGap N * signedZeroCenter N m) ∧
120         |‖deriv (canonicalSignedDenominator N) (signedPositiveZero N m : ℂ)‖ /
121           ((2 * Real.sin (Real.pi / N) / N) *
122             Real.exp (Real.cos (Real.pi / N) * signedPositiveZero N m)) - 1| ≤
123           B * Real.exp (-signedPolygonGap N * signedPositiveZero N m)) ∧
124       (∀ z : ℂ, R ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
125         ∃! p : {p : Fin N × ℕ // M ≤ p.2},
126           z = canonicalPrimitiveRoot N ^ p.val.1.val * (signedPositiveZero N p.val.2 : ℂ)) ∧
127       (∀ k m : ℕ, deriv (canonicalSignedDenominator N)
128         (canonicalPrimitiveRoot N ^ k * (signedPositiveZero N m : ℂ)) =
129         (canonicalPrimitiveRoot N ^ k)⁻¹ *
130           deriv (canonicalSignedDenominator N) (signedPositiveZero N m : ℂ)) := by
131   obtain ⟨C, hC, M0, hM0⟩ := signedPositiveZero_local_strings hN
132   obtain ⟨B, hB, M1, hM1⟩ := signedPositiveZero_derivative_asymptotic hN
133   obtain ⟨M, hM, R, hR, hex⟩ := signedPositiveZero_unique_global_strings hN (max M0 M1)
134   refine ⟨signedPolygonGap_pos hN, M, C, hC, B, hB, R, hR, ?_, hex,
135     signedPositiveZero_derivative_rotation (by omega)⟩
136   intro m hm
137   have hm0 := hM0 m (le_trans (le_max_left M0 M1) (le_trans hM hm))
138   have hm1 := hM1 m (le_trans (le_max_right M0 M1) (le_trans hM hm))
139   exact ⟨hm0.1, hm0.2.1, hm0.2.2.1, hm1⟩
140 
141 end
142 end Komorebi.PaperIV

Back to source controls