CubicZeroCorrection.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedCorrectionCompletion
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 
10 theorem signedPolygonGap_three : signedPolygonGap 3 = 3 / 2 := by
11   unfold signedPolygonGap
12   norm_num only [Nat.cast_ofNat, Real.cos_pi_div_three,
13     show 3 * (Real.pi / 3) = Real.pi by ring, Real.cos_pi]
14 
15 theorem signedZeroCenter_three (m : ℕ) :
16     signedZeroCenter 3 m = (2 * Real.pi / Real.sqrt 3) * (m + 1 / 2) := by
17   unfold signedZeroCenter
18   norm_num only [Nat.cast_ofNat, Real.sin_pi_div_three]
19   ring
20 
21 theorem canonicalSignedVertex_three_one : canonicalSignedVertex 3 1 = -1 := by
22   rw [canonicalSignedVertex_exp]
23   norm_num only [Nat.cast_one, Nat.cast_ofNat]
24   convert Complex.exp_pi_mul_I using 1
25   congr 1
26   push_cast
27   ring
28 
29 theorem canonicalSignedVertex_three_two :
30     canonicalSignedVertex 3 2 = 1 / 2 - (Real.sqrt 3 : ℂ) / 2 * Complex.I := by
31   apply Complex.ext
32   · have h := canonicalSignedVertex_last_re (by norm_num : 0 < 3)
33     norm_num only [Nat.reduceSub, Nat.cast_ofNat, Real.cos_pi_div_three] at h
34     convert h using 1
35     norm_num
36   · have h := canonicalSignedVertex_last_im (by norm_num : 0 < 3)
37     norm_num only [Nat.reduceSub, Nat.cast_ofNat, Real.sin_pi_div_three] at h
38     convert h using 1
39     norm_num
40 
41 theorem signedExponentialRemainder_three (z : ℂ) :
42     signedExponentialRemainder 3 (canonicalPrimitiveRoot 3) (canonicalSignedRoot 3) 0 z =
43       Complex.exp ((-3 / 2 + (Real.sqrt 3 : ℂ) / 2 * Complex.I) * z) := by
44   unfold signedExponentialRemainder finiteExponentialRemainder
45   have hs : (((Finset.range 3).erase 0).erase (3 - 1)) = {1} := by decide
46   rw [hs, Finset.sum_singleton, pow_zero, one_mul]
47   change Complex.exp ((canonicalSignedVertex 3 1 - canonicalSignedVertex 3 2) * z) = _
48   rw [canonicalSignedVertex_three_one, canonicalSignedVertex_three_two]
49   congr 2
50   ring
51 
52 theorem signedLeadingCorrection_three (m : ℕ) :
53     signedLeadingCorrection 3 m =
54       (((-1 : ℝ) ^ m / Real.sqrt 3 * Real.exp (-3 * signedZeroCenter 3 m / 2) : ℝ) : ℂ) := by
55   have hr : (Real.sqrt 3 : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (Real.sqrt_ne_zero'.mpr (by norm_num))
56   rw [signedLeadingCorrection, signedExponentialRemainder_three]
57   have he : (-3 / 2 + (Real.sqrt 3 : ℂ) / 2 * Complex.I) * (signedZeroCenter 3 m : ℂ) =
58       ((-3 * signedZeroCenter 3 m / 2 : ℝ) : ℂ) +
59       ((Real.sin (Real.pi / 3) * signedZeroCenter 3 m : ℝ) : ℂ) * Complex.I := by
60     rw [Real.sin_pi_div_three]
61     push_cast
62     ring
63   rw [he, Complex.exp_add]
64   have hp := signedZeroCenter_positive_phase (by norm_num : 2 ≤ 3) m
65   norm_num only [Nat.cast_ofNat] at hp
66   rw [hp, signedZeroFrequency, canonicalSignedVertex_adjacent_difference (by norm_num : 0 < 3)]
67   norm_num only [Nat.cast_ofNat, Real.sin_pi_div_three]
68   rw [← Complex.ofReal_exp]
69   push_cast
70   field_simp
71 
72 /-- The exact cubic correction and the O(exp(-3t)) remainder, at the actual
73 zeros rather than at a hypothetical approximate root. -/
74 theorem signedPositiveZero_three_correction :
75     ∃ C : ℝ, 0 < C ∧ ∃ M : ℕ, ∀ m ≥ M,
76       |signedPositiveZero 3 m - signedZeroCenter 3 m -
77         (-1 : ℝ) ^ m / Real.sqrt 3 * Real.exp (-3 * signedZeroCenter 3 m / 2)| ≤
78           C * Real.exp (-3 * signedZeroCenter 3 m) := by
79   obtain ⟨_, C, hC, M, hM⟩ := signedPositiveZero_first_correction (by norm_num : 3 ≤ 3)
80   refine ⟨C, hC, M, ?_⟩
81   intro m hm
82   have h := hM m hm
83   rw [signedLeadingCorrection_three, signedPolygonGap_three] at h
84   norm_num only [show -(2 * (3 / 2 : ℝ)) = -3 by norm_num] at h
85   simpa only [← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs] using h
86 
87 end
88 end Komorebi.PaperIV

Back to source controls