SignedZeroOrbits.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedGlobalExhaustion
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Metric
10 
11 theorem signedZeroFrequency_norm {N : ℕ} (hN : 2 ≤ N) :
12     ‖signedZeroFrequency N‖ = 2 * Real.sin (Real.pi / N) := by
13   rw [signedZeroFrequency, canonicalSignedVertex_adjacent_difference (by omega), norm_mul,
14     norm_mul, Complex.norm_I, mul_one, Complex.norm_real, Real.norm_eq_abs,
15     abs_of_pos (signed_sine_pos hN)]
16   norm_num
17 
18 /-- Rotation preserves the actual analytic multiplicity. -/
19 theorem canonicalSignedDenominator_order_rotation {N : ℕ} (hN : 0 < N)
20     {u : ℂ} (hu : u ^ N = 1) (z : ℂ) :
21     analyticOrderAt (canonicalSignedDenominator N) z =
22       analyticOrderAt (canonicalSignedDenominator N) (u * z) := by
23   have hu0 : u ≠ 0 := by intro h; simp [h, Nat.ne_of_gt hN] at hu
24   have hg : AnalyticAt ℂ (fun w : ℂ => u * w) z := by fun_prop
25   have hd : deriv (fun w : ℂ => u * w) z = u := by
26     simpa only [id_eq, mul_one] using ((hasDerivAt_id z).const_mul u).deriv
27   have he : canonicalSignedDenominator N ∘ (fun w : ℂ => u * w) = canonicalSignedDenominator N :=
28     funext (canonicalSignedDenominator_rotation hN hu)
29   have hh := analyticOrderAt_comp_of_deriv_ne_zero (f := canonicalSignedDenominator N) hg
30     (by rw [hd]; exact hu0)
31   rwa [he] at hh
32 
33 /-- The derivative transforms by the inverse rotation. -/
34 theorem canonicalSignedDenominator_derivative_rotation {N : ℕ} (hN : 0 < N)
35     {u : ℂ} (hu : u ^ N = 1) (z : ℂ) :
36     deriv (canonicalSignedDenominator N) (u * z) * u = deriv (canonicalSignedDenominator N) z := by
37   have hd := (analyticAt_entireSigned N 0 (canonicalPrimitiveRoot N) (canonicalSignedRoot N)
38     (u * z)).differentiableAt.hasDerivAt
39   have hg := (hasDerivAt_id z).const_mul u
40   have hc := hd.comp z hg
41   have he : (fun w : ℂ => canonicalSignedDenominator N (u * w)) = canonicalSignedDenominator N :=
42     funext (canonicalSignedDenominator_rotation hN hu)
43   change HasDerivAt (fun w : ℂ => canonicalSignedDenominator N (u * w))
44     (deriv (canonicalSignedDenominator N) (u * z) * (u * 1)) z at hc
45   rw [he, mul_one] at hc
46   exact hc.deriv.symm
47 
48 /-- A nonzero complex number has at most one unit-modulus rotation to the
49 positive real axis. -/
50 theorem positive_real_rotation_unique {z u v : ℂ} (hz : z ≠ 0)
51     (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
52     (hui : (u * z).im = 0) (hvi : (v * z).im = 0)
53     (hur : 0 < (u * z).re) (hvr : 0 < (v * z).re) : u = v := by
54   have hreal (w : ℂ) (hi : w.im = 0) : w = (w.re : ℂ) := by
55     apply Complex.ext <;> simp [hi]
56   have hnorm (w : ℂ) (hi : w.im = 0) (hr : 0 < w.re) : ‖w‖ = w.re := by
57     conv_lhs => rw [hreal w hi]
58     rw [Complex.norm_real, Real.norm_eq_abs, abs_of_pos hr]
59   have he : u * z = v * z := by
60     apply Complex.ext
61     · rw [← hnorm (u * z) hui hur, ← hnorm (v * z) hvi hvr, norm_mul, norm_mul, hu, hv]
62     · rw [hui, hvi]
63   exact mul_right_cancel₀ hz he
64 
65 /-- The fixed-radius disks around distinct natural lattice centers are disjoint. -/
66 theorem signedZeroCenter_disk_index_unique {N m n : ℕ} (hN : 2 ≤ N) {z : ℂ}
67     (hm : z ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖))
68     (hn : z ∈ closedBall (signedZeroCenter N n : ℂ) (1 / ‖signedZeroFrequency N‖)) : m = n := by
69   have hs := signed_sine_pos hN
70   have hdist : ‖(signedZeroCenter N m : ℂ) - (signedZeroCenter N n : ℂ)‖ ≤
71       2 / ‖signedZeroFrequency N‖ := by
72     have h := dist_triangle (signedZeroCenter N m : ℂ) z (signedZeroCenter N n : ℂ)
73     have hm' := mem_closedBall.mp hm
74     have hn' := mem_closedBall.mp hn
75     rw [dist_comm z (signedZeroCenter N m : ℂ)] at hm'
76     rw [dist_eq_norm] at h
77     calc
78       _ ≤ _ := h
79       _ ≤ 1 / ‖signedZeroFrequency N‖ + 1 / ‖signedZeroFrequency N‖ := add_le_add hm' hn'
80       _ = _ := by ring
81   rw [← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs, signedZeroFrequency_norm hN] at hdist
82   have he : signedZeroCenter N m - signedZeroCenter N n =
83       (Real.pi / Real.sin (Real.pi / N)) * ((m : ℝ) - n) := by unfold signedZeroCenter; ring
84   rw [he, abs_mul, abs_of_pos (div_pos Real.pi_pos hs)] at hdist
85   have hmul := (le_div_iff₀ (mul_pos (by norm_num) hs)).mp hdist
86   have hcancel : (Real.pi / Real.sin (Real.pi / N)) * |(m : ℝ) - n| *
87       (2 * Real.sin (Real.pi / N)) = 2 * Real.pi * |(m : ℝ) - n| := by field_simp
88   rw [hcancel] at hmul
89   by_contra hne
90   have habs : 1 ≤ |(m : ℝ) - n| := by
91     rcases lt_or_gt_of_ne hne with h | h
92     · have hh : (m : ℝ) + 1 ≤ n := by exact_mod_cast (show m + 1 ≤ n by omega)
93       rw [abs_of_nonpos (by linarith)]
94       linarith
95     · have hh : (n : ℝ) + 1 ≤ m := by exact_mod_cast (show n + 1 ≤ m by omega)
96       rw [abs_of_nonneg (by linarith)]
97       linarith
98   nlinarith [Real.two_le_pi]
99 
100 /-- In the manuscript's canonical finite set of rotations, all sufficiently
101 large zeros belong to the real strings and are simple at their original point. -/
102 theorem canonicalSignedDenominator_large_zero_orbits {N : ℕ} (hN : 3 ≤ N) (m0 : ℕ) :
103     ∃ R : ℝ, 0 < R ∧ ∀ z : ℂ, R ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
104       ∃ k < N, ∃ m : ℕ, m0 ≤ m ∧
105         canonicalPrimitiveRoot N ^ k * z ∈
106           closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
107         (canonicalPrimitiveRoot N ^ k * z).im = 0 ∧
108         0 < (canonicalPrimitiveRoot N ^ k * z).re ∧
109         analyticOrderAt (canonicalSignedDenominator N) z = 1 := by
110   let : NeZero N := ⟨by omega⟩
111   obtain ⟨R, hR, hex⟩ := canonicalSignedDenominator_global_exhaustion hN m0
112   refine ⟨R, hR, ?_⟩
113   intro z hz hz0
114   obtain ⟨u, m, hu, _, hm, _, hball, him, hpos, hs, _⟩ := hex z hz hz0
115   obtain ⟨k, hk, he⟩ := (canonicalPrimitiveRoot_isPrimitive (by omega : 0 < N)).eq_pow_of_pow_eq_one hu
116   refine ⟨k, hk, m, hm, he.symm ▸ hball, he.symm ▸ him, he.symm ▸ hpos, ?_⟩
117   rw [canonicalSignedDenominator_order_rotation (by omega) hu]
118   exact hs
119 
120 end
121 end Komorebi.PaperIV

Back to source controls