RegularPolygonGap.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ExponentialRemainder
6 
7 /-! # The canonical polygon gap and actual signed-remainder bounds -/
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 
12 def canonicalSignedVertex (N l : ℕ) : ℂ :=
13   canonicalSignedRoot N * canonicalPrimitiveRoot N ^ l
14 
15 def signedPolygonGap (N : ℕ) : ℝ :=
16   Real.cos (Real.pi / N) - Real.cos (3 * (Real.pi / N))
17 
18 theorem canonicalSignedVertex_exp (N l : ℕ) :
19     canonicalSignedVertex N l =
20       Complex.exp ((((2 * (l : ℝ) + 1) * (Real.pi / N) : ℝ) : ℂ) * Complex.I) := by
21   unfold canonicalSignedVertex canonicalSignedRoot canonicalPrimitiveRoot
22   rw [← Complex.exp_nat_mul, ← Complex.exp_add]
23   congr 1
24   push_cast
25   ring
26 
27 theorem canonicalSignedVertex_re (N l : ℕ) :
28     (canonicalSignedVertex N l).re = Real.cos ((2 * l + 1) * (Real.pi / N)) := by
29   rw [canonicalSignedVertex_exp, Complex.exp_ofReal_mul_I_re]
30 
31 theorem canonicalSignedVertex_im (N l : ℕ) :
32     (canonicalSignedVertex N l).im = Real.sin ((2 * l + 1) * (Real.pi / N)) := by
33   rw [canonicalSignedVertex_exp, Complex.exp_ofReal_mul_I_im]
34 
35 theorem norm_canonicalSignedVertex (N l : ℕ) : ‖canonicalSignedVertex N l‖ = 1 := by
36   rw [canonicalSignedVertex_exp, Complex.norm_exp]
37   simp
38 
39 theorem canonicalSignedVertex_last_angle {N : ℕ} (hN : 0 < N) :
40     (2 * ((N - 1 : ℕ) : ℝ) + 1) * (Real.pi / N) =
41       2 * Real.pi - Real.pi / N := by
42   rw [Nat.cast_sub (by omega : 1 ≤ N)]
43   have hn : (N : ℝ) ≠ 0 := by exact_mod_cast hN.ne'
44   push_cast
45   field_simp
46   ring
47 
48 theorem canonicalSignedVertex_last_re {N : ℕ} (hN : 0 < N) :
49     (canonicalSignedVertex N (N - 1)).re = Real.cos (Real.pi / N) := by
50   rw [canonicalSignedVertex_re, canonicalSignedVertex_last_angle hN, Real.cos_two_pi_sub]
51 
52 theorem canonicalSignedVertex_last_im {N : ℕ} (hN : 0 < N) :
53     (canonicalSignedVertex N (N - 1)).im = -Real.sin (Real.pi / N) := by
54   rw [canonicalSignedVertex_im, canonicalSignedVertex_last_angle hN, Real.sin_two_pi_sub]
55 
56 theorem signedPolygonGap_pos {N : ℕ} (hN : 3 ≤ N) : 0 < signedPolygonGap N := by
57   have hn : (3 : ℝ) ≤ N := by exact_mod_cast hN
58   have hp : 0 < Real.pi / N := div_pos Real.pi_pos (by linarith)
59   have he : Real.pi / N * N = Real.pi := div_mul_cancel₀ _ (by linarith)
60   have h3 : 3 * (Real.pi / N) ≤ Real.pi := by nlinarith
61   exact sub_pos.mpr (Real.cos_lt_cos_of_nonneg_of_le_pi hp.le h3 (by linarith))
62 
63 /-- Every nonadjacent vertex has the precise positive real-part gap. -/
64 theorem canonicalSignedVertex_re_gap {N l : ℕ} (hN : 3 ≤ N)
65     (hl : l ∈ ((Finset.range N).erase 0).erase (N - 1)) :
66     (canonicalSignedVertex N l - canonicalSignedVertex N (N - 1)).re ≤
67       -signedPolygonGap N := by
68   have hi : 1 ≤ l ∧ l ≤ N - 2 := by
69     simp only [Finset.mem_erase, Finset.mem_range] at hl
70     omega
71   have hn : (3 : ℝ) ≤ N := by exact_mod_cast hN
72   have hl1 : (1 : ℝ) ≤ l := by exact_mod_cast hi.1
73   have hl2 : (l : ℝ) ≤ N - 2 := by
74     have hh : (l : ℝ) + 2 ≤ N := by exact_mod_cast (show l + 2 ≤ N by omega)
75     linarith
76   let α : ℝ := Real.pi / N
77   let θ : ℝ := (2 * l + 1) * α
78   have hp : 0 < α := div_pos Real.pi_pos (by linarith)
79   have he : α * N = Real.pi := div_mul_cancel₀ _ (by linarith)
80   have hlo : 3 * α ≤ θ := by dsimp [θ]; nlinarith
81   have hhi : θ ≤ 2 * Real.pi - 3 * α := by dsimp [θ]; nlinarith
82   have hc : Real.cos θ ≤ Real.cos (3 * α) := by
83     by_cases hθ : θ ≤ Real.pi
84     · exact Real.cos_le_cos_of_nonneg_of_le_pi (by positivity) hθ hlo
85     · have hc := Real.cos_le_cos_of_nonneg_of_le_pi
86         (by positivity : 0 ≤ 3 * α) (by linarith : 2 * Real.pi - θ ≤ Real.pi)
87         (by linarith : 3 * α ≤ 2 * Real.pi - θ)
88       simpa [Real.cos_two_pi_sub] using hc
89   rw [Complex.sub_re, canonicalSignedVertex_re, canonicalSignedVertex_last_re (by omega)]
90   unfold signedPolygonGap
91   change Real.cos θ - Real.cos α ≤ -(Real.cos α - Real.cos (3 * α))
92   linarith
93 
94 /-- The actual remainder satisfies the paper's exponential bound for every q. -/
95 theorem canonicalSignedRemainder_strip_bound {N : ℕ} (hN : 3 ≤ N)
96     {Y : ℝ} {z : ℂ} (hx : 0 ≤ z.re) (hy : |z.im| ≤ Y) (q : ℕ) :
97     ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) q z‖ ≤
98       ((N - 2 : ℕ) : ℝ) * 2 ^ q *
99         Real.exp (-signedPolygonGap N * z.re + 2 * Y) := by
100   have hnorm (l : ℕ) : ‖canonicalSignedVertex N l - canonicalSignedVertex N (N - 1)‖ ≤ 2 := by
101     calc _ ≤ ‖canonicalSignedVertex N l‖ + ‖canonicalSignedVertex N (N - 1)‖ := norm_sub_le _ _
102          _ = 2 := by rw [norm_canonicalSignedVertex, norm_canonicalSignedVertex]; norm_num
103   have hs : (((Finset.range N).erase 0).erase (N - 1)).card = N - 2 := by
104     rw [Finset.card_erase_of_mem, Finset.card_erase_of_mem, Finset.card_range]
105     · omega
106     · simp; omega
107     · simp; omega
108   have h := finiteExponentialRemainder_strip_bound (a := canonicalSignedVertex N)
109     (b := canonicalSignedVertex N (N - 1)) (by norm_num : (0 : ℝ) ≤ 2) (by norm_num : (0 : ℝ) ≤ 2)
110     (fun l hl => canonicalSignedVertex_re_gap hN hl)
111     (fun l _ => (Complex.abs_im_le_norm _).trans (hnorm l)) (fun l _ => hnorm l) hx hy q
112   rw [hs] at h
113   convert h using 1
114   rfl
115 
116 /-- The difference between the adjacent exponents is exactly 2 i sin(pi/N). -/
117 theorem canonicalSignedVertex_adjacent_difference {N : ℕ} (hN : 0 < N) :
118     canonicalSignedRoot N - canonicalSignedVertex N (N - 1) =
119       (2 * (Real.sin (Real.pi / N) : ℂ)) * Complex.I := by
120   have hzero : canonicalSignedRoot N = canonicalSignedVertex N 0 := by
121     simp [canonicalSignedVertex]
122   rw [hzero]
123   apply Complex.ext
124   · simp only [Complex.sub_re, Complex.mul_re, Complex.mul_im, Complex.ofReal_re,
125       Complex.ofReal_im, Complex.I_re, Complex.I_im]
126     rw [canonicalSignedVertex_last_re hN, canonicalSignedVertex_re]
127     norm_num only [Nat.cast_zero, mul_zero, zero_add, one_mul, sub_self, mul_one,
128       sub_zero, zero_mul, (show (2 : ℂ).im = 0 from rfl)]
129   · simp only [Complex.sub_im, Complex.mul_im, Complex.mul_re, Complex.ofReal_re,
130       Complex.ofReal_im, Complex.I_re, Complex.I_im]
131     rw [canonicalSignedVertex_last_im hN, canonicalSignedVertex_im]
132     norm_num only [Nat.cast_zero, mul_zero, zero_add, one_mul, mul_one, add_zero,
133       sub_neg_eq_add, zero_mul, (show (2 : ℂ).re = 2 from rfl)]
134     ring
135 
136 end
137 end Komorebi.PaperIV

Back to source controls