SignedZeroCorrection.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedZeroLocalization
6 
7 /-! # Quantified leading correction for the actual signed zero strings -/
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Metric
12 
13 /-- The explicit coefficient in the exponential remainder envelope. -/
14 def signedRemainderScale (N : ℕ) : ℝ :=
15   ((N - 2 : ℕ) : ℝ) * Real.exp (signedPolygonGap N * (1 / ‖signedZeroFrequency N‖) +
16     2 * (1 / ‖signedZeroFrequency N‖))
17 
18 def signedRemainderEnvelope (N : ℕ) (t : ℝ) : ℝ :=
19   signedRemainderScale N * Real.exp (-signedPolygonGap N * t)
20 
21 theorem signedRemainderEnvelope_pos {N : ℕ} (hN : 3 ≤ N) (t : ℝ) :
22     0 < signedRemainderEnvelope N t := by
23   unfold signedRemainderEnvelope signedRemainderScale
24   have hn : 0 < N - 2 := by omega
25   positivity
26 
27 theorem signedRemainderEnvelope_bounds {N : ℕ} (hN : 3 ≤ N) {t : ℝ}
28     (ht : 1 / ‖signedZeroFrequency N‖ ≤ t) {z : ℂ}
29     (hz : z ∈ closedBall (t : ℂ) (1 / ‖signedZeroFrequency N‖)) (q : ℕ) :
30     ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) q z‖ ≤
31       2 ^ q * signedRemainderEnvelope N t := by
32   have h := canonicalSignedRemainder_disk_bound hN ht hz q
33   unfold signedRemainderEnvelope signedRemainderScale
34   convert h using 1
35   ring
36 
37 /-- The error after subtracting the actual leading correction is quadratic
38 in the exponentially decaying remainder envelope. -/
39 theorem canonicalSignedDenominator_first_correction {N : ℕ} (hN : 3 ≤ N)
40     {t : ℝ} (ht : 1 / ‖signedZeroFrequency N‖ ≤ t)
41     (hc : Complex.exp (signedZeroFrequency N * (t : ℂ)) = -1)
42     (hsmall : signedRemainderEnvelope N t ≤ 1 / 2)
43     {z : ℂ} (hz : z ∈ closedBall (t : ℂ) (1 / ‖signedZeroFrequency N‖))
44     (hz0 : canonicalSignedDenominator N z = 0) :
45     ‖z - (t : ℂ) -
46       signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 (t : ℂ) /
47         signedZeroFrequency N‖ ≤
48       ((1 + 3 / ‖signedZeroFrequency N‖) / ‖signedZeroFrequency N‖) *
49         signedRemainderEnvelope N t ^ 2 := by
50   have ha := signedZeroFrequency_ne_zero (show 2 ≤ N by omega)
51   have h := perturbed_exponential_first_correction
52     (R := signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0)
53     (R' := signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 1) ha hc hsmall
54     (fun w hw => by simpa using signedRemainderEnvelope_bounds hN ht hw 0)
55     (fun w _ => hasDerivAt_finiteExponentialRemainder _ _ _ 0 w)
56     (fun w hw => by simpa using signedRemainderEnvelope_bounds hN ht hw 1)
57     hz ((signed_two_term_zero_iff (by omega) _ _ z).mp hz0)
58   convert h using 1
59   ring
60 
61 /-- The quadratic envelope is exactly a constant times exp(-2 gamma t). -/
62 theorem signedRemainderEnvelope_sq (N : ℕ) (t : ℝ) :
63     signedRemainderEnvelope N t ^ 2 =
64       signedRemainderScale N ^ 2 * Real.exp (-(2 * signedPolygonGap N) * t) := by
65   unfold signedRemainderEnvelope
66   rw [mul_pow, pow_two (Real.exp _), ← Real.exp_add]
67   congr 2
68   ring
69 
70 /-- The actual normalized derivative has a quantified exponentially small error. -/
71 theorem canonicalSignedDenominator_normalized_derivative_error {N : ℕ} (hN : 3 ≤ N)
72     {t : ℝ} (ht : 1 / ‖signedZeroFrequency N‖ ≤ t) {z : ℂ}
73     (hz : z ∈ closedBall (t : ℂ) (1 / ‖signedZeroFrequency N‖))
74     (hz0 : canonicalSignedDenominator N z = 0) :
75     ‖(signedZeroFrequency N * Complex.exp (signedZeroFrequency N * z) +
76       signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 1 z) +
77         signedZeroFrequency N‖ ≤
78       (‖signedZeroFrequency N‖ + 2) * signedRemainderEnvelope N t := by
79   have h := perturbed_exponential_derivative_error
80     (a := signedZeroFrequency N)
81     (R := signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0)
82     ((signed_two_term_zero_iff (by omega) _ _ z).mp hz0)
83     (Rz' := signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 1 z)
84   have h0 := signedRemainderEnvelope_bounds hN ht hz 0
85   have h1 := signedRemainderEnvelope_bounds hN ht hz 1
86   simp only [pow_zero, one_mul, pow_one] at h0 h1
87   exact h.trans (by nlinarith [mul_le_mul_of_nonneg_left h0 (norm_nonneg (signedZeroFrequency N))])
88 
89 end
90 end Komorebi.PaperIV

Back to source controls