SignedDominance.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 
10 /-- The manuscript's argument-based sector implies the Cartesian inequalities. -/
11 theorem signedFundamentalSector_of_arg {N : ℕ} (hN : 3 ≤ N) {z : ℂ}
12     (hz : |z.arg| ≤ Real.pi / N) : signedFundamentalSector N z := by
13   have h := (signedFundamentalSector_polar hN (norm_nonneg z) hz).1
14   simpa only [Complex.norm_mul_exp_arg_mul_I] using h
15 
16 /-- One constant controls the first three remainder jets on a fixed strip. -/
17 theorem canonicalSignedRemainder_three_jet_bound {N : ℕ} (hN : 3 ≤ N)
18     {Y : ℝ} {z : ℂ} (hx : 0 ≤ z.re) (hy : |z.im| ≤ Y) {q : ℕ} (hq : q ≤ 2) :
19     ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) q z‖ ≤
20       (((N - 2 : ℕ) : ℝ) * 4 * Real.exp (2 * Y)) * Real.exp (-signedPolygonGap N * z.re) := by
21   have hpow : (2 : ℝ) ^ q ≤ 4 := by
22     have hh : q = 0 ∨ q = 1 ∨ q = 2 := by omega
23     rcases hh with rfl | rfl | rfl <;> norm_num
24   have hb := canonicalSignedRemainder_strip_bound hN hx hy q
25   calc
26     _ ≤ ((N - 2 : ℕ) : ℝ) * 2 ^ q * Real.exp (-signedPolygonGap N * z.re + 2 * Y) := hb
27     _ ≤ ((N - 2 : ℕ) : ℝ) * 4 * Real.exp (-signedPolygonGap N * z.re + 2 * Y) := by
28       gcongr
29     _ = _ := by rw [Real.exp_add]; ring
30 
31 /-- The full argument-sector, normalization, and three-jet conclusion of
32 manuscript Lemma 11.5, with actual derived positive constants. -/
33 theorem canonicalSignedDenominator_two_term_dominance {N : ℕ} (hN : 3 ≤ N) :
34     ∃ Y R C : ℝ, 0 < Y ∧ 0 < R ∧ 0 < C ∧
35       (∀ z : ℂ, |z.arg| ≤ Real.pi / N → R ≤ z.re →
36         canonicalSignedDenominator N z = 0 → |z.im| ≤ Y) ∧
37       (∀ z : ℂ, (N : ℂ) * Complex.exp (-(canonicalSignedVertex N (N - 1) * z)) *
38         canonicalSignedDenominator N z =
39         1 + Complex.exp (signedZeroFrequency N * z) +
40           signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 z) ∧
41       (∀ z : ℂ, R ≤ z.re → |z.im| ≤ Y → ∀ q : ℕ, q ≤ 2 →
42         ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) q z‖ ≤
43           C * Real.exp (-signedPolygonGap N * z.re)) := by
44   let Y := signedSectorWidth N
45   refine ⟨Y, 1, ((N - 2 : ℕ) : ℝ) * 4 * Real.exp (2 * Y),
46     signedSectorWidth_pos hN, by norm_num, ?_, ?_, ?_, ?_⟩
47   · have hn : 0 < N - 2 := by omega
48     positivity
49   · intro z harg _ hz
50     exact canonicalSignedDenominator_sector_zero_bound hN (signedFundamentalSector_of_arg hN harg) hz
51   · intro z
52     exact signed_two_term_normalization (by omega) _ _ z
53   · intro z hx hy q hq
54     exact canonicalSignedRemainder_three_jet_bound hN (by linarith) hy hq
55 
56 end
57 end Komorebi.PaperIV

Back to source controls