ExactZetaModels.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.QuarticExactZeros
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 open scoped Topology
11 
12 /-- Construction used only after all zeros and their simplicity have been proved. -/
13 def exactLatticeEnumeration {N : ℕ} (hN : 2 ≤ N)
14     (hz : ∀ m, canonicalSignedDenominator N (signedZeroCenter N m : ℂ) = 0)
15     (hs : ∀ m, analyticOrderAt (canonicalSignedDenominator N) (signedZeroCenter N m : ℂ) = 1)
16     (he : ∀ z, canonicalSignedDenominator N z = 0 → ∃ k : Fin N, ∃ m,
17       z = canonicalPrimitiveRoot N ^ k.val * (signedZeroCenter N m : ℂ)) : SignedZeroEnumeration N where
18   root := signedZeroCenter N
19   positive := signedZeroCenter_positive hN
20   zero := hz
21   simple := hs
22   injective := by
23     intro m n h
24     have hA := ne_of_gt (div_pos Real.pi_pos (signed_sine_pos hN))
25     exact_mod_cast add_right_cancel (mul_left_cancel₀ hA h)
26   shift := 1
27   windows := by
28     intro m
29     have hA := div_pos Real.pi_pos (signed_sine_pos hN)
30     unfold signedZeroCenter
31     norm_num only [Nat.cast_one]
32     constructor <;> nlinarith
33   offset := 0
34   displacement := ⟨1, by norm_num, 1, by norm_num, fun m => by
35     simp only [Nat.add_zero, sub_self, abs_zero, one_mul]
36     exact (Real.exp_pos _).le⟩
37   radius := 1
38   radius_pos := by norm_num
39   exhaustive := fun z _ hz0 => he z hz0
40 
41 theorem SignedZeroEnumeration.reducedZero_surjective_of_orbitZero {N : ℕ} (hn : 0 < N)
42     (e : SignedZeroEnumeration N) (he : Function.Surjective (e.orbitZero hn)) :
43     Function.Surjective (e.reducedZero hn) := by
44   intro w
45   obtain ⟨z, hz⟩ := exists_complex_nth_root hn (w : ℂ)
46   have hd : canonicalSignedDenominator N z = 0 := by
47     rw [canonicalSignedDenominator_eq_reduced_power hn, hz]
48     exact w.property
49   obtain ⟨p, hp⟩ := he ⟨z, hd⟩
50   refine ⟨p.2, Subtype.ext ?_⟩
51   have heq : e.orbit p = z := congrArg Subtype.val hp
52   have hu : (canonicalPrimitiveRoot N ^ p.1.val) ^ N = 1 := by
53     rw [← pow_mul, Nat.mul_comm, pow_mul, (canonicalPrimitiveRoot_isPrimitive hn).pow_eq_one, one_pow]
54   rw [← hz, ← heq, SignedZeroEnumeration.orbit, mul_pow, hu, one_mul]
55   rfl
56 
57 theorem SignedZeroEnumeration.exceptions_zero_of_surjective {N : ℕ} (hn : 0 < N)
58     (e : SignedZeroEnumeration N) (he : Function.Surjective (e.orbitZero hn)) (s : ℂ) :
59     e.absoluteExceptionZeta hn s = 0 ∧ e.reducedExceptionZeta hn s = 0 := by
60   have hr := e.reducedZero_surjective_of_orbitZero hn he
61   have : IsEmpty ↥((range (e.orbitZero hn))ᶜ) := ⟨fun z => z.property (he z.val)⟩
62   have : IsEmpty ↥((range (e.reducedZero hn))ᶜ) := ⟨fun z => z.property (hr z.val)⟩
63   simp [SignedZeroEnumeration.absoluteExceptionZeta, SignedZeroEnumeration.reducedExceptionZeta]
64 
65 /-- Both exact models follow from a fully proved, simple, exhaustive lattice. -/
66 theorem zero_zeta_exact_of_lattice {N : ℕ} (hN : 2 ≤ N)
67     (hz : ∀ m, canonicalSignedDenominator N (signedZeroCenter N m : ℂ) = 0)
68     (hsimple : ∀ m, analyticOrderAt (canonicalSignedDenominator N) (signedZeroCenter N m : ℂ) = 1)
69     (hex : ∀ z, canonicalSignedDenominator N z = 0 → ∃ k : Fin N, ∃ m,
70       z = canonicalPrimitiveRoot N ^ k.val * (signedZeroCenter N m : ℂ)) :
71     (∀ s : ℂ, 1 < s.re → absoluteZeroZeta (canonicalSignedDenominator N) s =
72       (N : ℂ) * hurwitzLatticeModel (Real.pi / Real.sin (Real.pi / N)) 1 s) ∧
73     (∀ s : ℂ, 1 / (N : ℝ) < s.re → absoluteZeroZeta (entireReducedDenominator N) s =
74       hurwitzLatticeModel (Real.pi / Real.sin (Real.pi / N)) N s) := by
75   let e := exactLatticeEnumeration hN hz hsimple hex
76   have he : Function.Surjective (e.orbitZero (by omega)) := by
77     intro z
78     obtain ⟨k, m, hm⟩ := hex z z.property
79     exact ⟨(k, m), Subtype.ext hm.symm⟩
80   have hc : ∀ s, e.latticeCorrection s = 0 := by
81     intro s
82     simp only [SignedZeroEnumeration.latticeCorrection, exponentialZetaDifference, e,
83       exactLatticeEnumeration, Nat.add_zero, sub_self, tsum_zero]
84   have hp : ∀ s, e.latticePrefix s = 0 := by
85     intro s
86     simp only [SignedZeroEnumeration.latticePrefix, e, exactLatticeEnumeration, Finset.range_zero, Finset.sum_empty]
87   constructor
88   · intro s hs
89     rw [e.absoluteZeta_decomposition hN hs, e.root_zeta_eq_model hN hs, hc, hp,
90       (e.exceptions_zero_of_surjective (by omega) he s).1, add_zero, sub_zero, add_zero]
91   · intro s hs
92     have hsN : 1 < ((N : ℂ) * s).re := by
93       simp only [Complex.mul_re, Complex.natCast_re, Complex.natCast_im, zero_mul, sub_zero]
94       have hn : (0 : ℝ) < N := by exact_mod_cast (show 0 < N by omega)
95       exact (div_lt_iff₀ hn).mp hs |>.trans_eq (mul_comm _ _)
96     rw [e.reducedZeta_decomposition hN hs, e.root_zeta_eq_model hN hsN, hc, hp,
97       (e.exceptions_zero_of_surjective (by omega) he s).2, add_zero, sub_zero, add_zero]
98     simp only [hurwitzLatticeModel, Nat.cast_one, one_mul]
99 
100 theorem signedZeroCenter_four (m : ℕ) : signedZeroCenter 4 m = quarticPositiveZero m := by
101   have hq : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num)
102   have hq0 : Real.sqrt 2 ≠ 0 := by positivity
103   unfold signedZeroCenter quarticPositiveZero
104   simp only [Nat.cast_ofNat, Real.sin_pi_div_four]
105   field_simp
106   nlinarith
107 
108 theorem orderTwo_full_lattice :
109     (∀ m, canonicalSignedDenominator 2 (signedZeroCenter 2 m : ℂ) = 0) ∧
110     (∀ m, analyticOrderAt (canonicalSignedDenominator 2) (signedZeroCenter 2 m : ℂ) = 1) ∧
111     (∀ z, canonicalSignedDenominator 2 z = 0 → ∃ k : Fin 2, ∃ m,
112       z = canonicalPrimitiveRoot 2 ^ k.val * (signedZeroCenter 2 m : ℂ)) := by
113   have homega := canonicalPrimitiveRoot_isPrimitive (by norm_num : 0 < 2)
114   have hrho := canonicalSignedRoot_pow (by norm_num : 0 < 2)
115   have hc : ∀ m, (signedZeroCenter 2 m : ℂ) = ((m : ℂ) + 1 / 2) * (Real.pi : ℂ) := by
116     intro m
117     simp only [signedZeroCenter, Nat.cast_ofNat, Real.sin_pi_div_two, div_one]
118     push_cast
119     ring
120   have hz : ∀ m, canonicalSignedDenominator 2 (signedZeroCenter 2 m : ℂ) = 0 := by
121     intro m
122     exact (entireSigned_two_zero_iff_nat homega hrho).mpr ⟨m, Or.inl (hc m)⟩
123   refine ⟨hz, fun m => entireSigned_two_zero_order_one homega hrho (hz m), ?_⟩
124   intro z hz0
125   obtain ⟨m, hm | hm⟩ := (entireSigned_two_zero_iff_nat homega hrho).mp hz0
126   · exact ⟨⟨0, by norm_num⟩, m, by simpa only [pow_zero, one_mul, hc m] using hm⟩
127   · exact ⟨⟨1, by norm_num⟩, m, by simpa only [pow_one, homega.eq_neg_one_of_two_right, neg_one_mul, hc m] using hm⟩
128 
129 theorem orderFour_full_lattice :
130     (∀ m, canonicalSignedDenominator 4 (signedZeroCenter 4 m : ℂ) = 0) ∧
131     (∀ m, analyticOrderAt (canonicalSignedDenominator 4) (signedZeroCenter 4 m : ℂ) = 1) ∧
132     (∀ z, canonicalSignedDenominator 4 z = 0 → ∃ k : Fin 4, ∃ m,
133       z = canonicalPrimitiveRoot 4 ^ k.val * (signedZeroCenter 4 m : ℂ)) := by
134   refine ⟨fun m => ?_, fun m => ?_, ?_⟩
135   · rw [signedZeroCenter_four]
136     exact canonicalSignedDenominator_four_zero_iff.mpr ⟨m, Or.inl rfl⟩
137   · rw [signedZeroCenter_four]
138     exact quarticPositiveZero_simple m
139   · intro z hz
140     have homega := canonicalPrimitiveRoot_isPrimitive (by norm_num : 0 < 4)
141     have hu : ∀ u : ℂ, u ^ 4 = 1 → ∀ m, ∃ k : Fin 4, ∃ j,
142         u * (quarticPositiveZero m : ℂ) = canonicalPrimitiveRoot 4 ^ k.val * (signedZeroCenter 4 j : ℂ) := by
143       intro u hu m
144       obtain ⟨k, hk, he⟩ := homega.eq_pow_of_pow_eq_one hu
145       exact ⟨⟨k, hk⟩, m, by rw [signedZeroCenter_four, he]⟩
146     obtain ⟨m, hm | hm | hm | hm⟩ := canonicalSignedDenominator_four_zero_iff.mp hz
147     · rw [hm]
148       simpa only [one_mul] using hu 1 (by norm_num) m
149     · rw [hm]
150       simpa only [neg_one_mul] using hu (-1) (by norm_num) m
151     · rw [hm]
152       exact hu Complex.I Complex.isPrimitiveRoot_I.pow_eq_one m
153     · rw [hm]
154       simpa only [neg_mul] using hu (-Complex.I) Complex.isPrimitiveRoot_neg_I.pow_eq_one m
155 
156 /-- Corollary 14.4, with no omitted zeros in either order. -/
157 theorem orderTwo_exact_zero_zeta_models :
158     (∀ s : ℂ, 1 < s.re → absoluteZeroZeta (canonicalSignedDenominator 2) s =
159       2 * hurwitzLatticeModel Real.pi 1 s) ∧
160     (∀ s : ℂ, 1 / 2 < s.re → absoluteZeroZeta (entireReducedDenominator 2) s =
161       hurwitzLatticeModel Real.pi 2 s) := by
162   simpa only [Nat.cast_ofNat, Real.sin_pi_div_two, div_one] using
163     zero_zeta_exact_of_lattice (by norm_num) orderTwo_full_lattice.1 orderTwo_full_lattice.2.1 orderTwo_full_lattice.2.2
164 
165 theorem orderFour_exact_zero_zeta_models :
166     (∀ s : ℂ, 1 < s.re → absoluteZeroZeta (canonicalSignedDenominator 4) s =
167       4 * hurwitzLatticeModel (Real.sqrt 2 * Real.pi) 1 s) ∧
168     (∀ s : ℂ, 1 / 4 < s.re → absoluteZeroZeta (entireReducedDenominator 4) s =
169       hurwitzLatticeModel (Real.sqrt 2 * Real.pi) 4 s) := by
170   have hA : Real.pi / Real.sin (Real.pi / 4) = Real.sqrt 2 * Real.pi := by
171     have h := signedZeroCenter_four 0
172     simp only [signedZeroCenter, quarticPositiveZero, Nat.cast_zero, zero_add, Nat.cast_ofNat] at h
173     linarith
174   simpa only [Nat.cast_ofNat, hA] using
175     zero_zeta_exact_of_lattice (by norm_num) orderFour_full_lattice.1 orderFour_full_lattice.2.1 orderFour_full_lattice.2.2
176 
177 theorem entire_zero_of_halfplane {f : ℂ → ℂ} (hf : Differentiable ℂ f) (c : ℝ)
178     (hz : ∀ s : ℂ, c < s.re → f s = 0) : f = 0 := by
179   have he : f =ᶠ[𝓝 ((c + 1 : ℝ) : ℂ)] 0 := by
180     have ho : IsOpen {s : ℂ | c < s.re} := isOpen_lt continuous_const Complex.continuous_re
181     filter_upwards [ho.mem_nhds (show ((c + 1 : ℝ) : ℂ) ∈ {s : ℂ | c < s.re} by
182       simp only [mem_ofPred_eq, Complex.ofReal_re]; linarith)] with s hs
183     exact hz s hs
184   exact (show AnalyticOnNhd ℂ f univ from fun s _ => hf.analyticAt s).eq_of_eventuallyEq
185     (show AnalyticOnNhd ℂ (0 : ℂ → ℂ) univ from fun _ _ => analyticAt_const) he
186 
187 /-- The corrections chosen in Theorem 14.3 themselves vanish in the exact cases. -/
188 theorem zero_zeta_corrections_of_lattice {N : ℕ} (hN : 2 ≤ N)
189     (hz : ∀ m, canonicalSignedDenominator N (signedZeroCenter N m : ℂ) = 0)
190     (hsimple : ∀ m, analyticOrderAt (canonicalSignedDenominator N) (signedZeroCenter N m : ℂ) = 1)
191     (hex : ∀ z, canonicalSignedDenominator N z = 0 → ∃ k : Fin N, ∃ m,
192       z = canonicalPrimitiveRoot N ^ k.val * (signedZeroCenter N m : ℂ)) :
193     absoluteZetaCorrection hN = 0 ∧ reducedZetaCorrection hN = 0 := by
194   have he := zero_zeta_exact_of_lattice hN hz hsimple hex
195   constructor
196   · apply entire_zero_of_halfplane (absoluteZetaCorrection_entire hN) 1
197     intro s hs
198     have h := canonicalSignedDenominator_zeta_eq_hurwitz hN hs
199     rw [he.1 s hs] at h
200     linear_combination -h
201   · apply entire_zero_of_halfplane (reducedZetaCorrection_entire hN) (1 / (N : ℝ))
202     intro s hs
203     have h := entireReducedDenominator_zeta_eq_hurwitz hN hs
204     rw [he.2 s hs] at h
205     linear_combination -h
206 
207 theorem orderTwo_zeta_corrections_zero :
208     absoluteZetaCorrection (by norm_num : 2 ≤ 2) = 0 ∧
209     reducedZetaCorrection (by norm_num : 2 ≤ 2) = 0 :=
210   zero_zeta_corrections_of_lattice (by norm_num) orderTwo_full_lattice.1
211     orderTwo_full_lattice.2.1 orderTwo_full_lattice.2.2
212 
213 theorem orderFour_zeta_corrections_zero :
214     absoluteZetaCorrection (by norm_num : 2 ≤ 4) = 0 ∧
215     reducedZetaCorrection (by norm_num : 2 ≤ 4) = 0 :=
216   zero_zeta_corrections_of_lattice (by norm_num) orderFour_full_lattice.1
217     orderFour_full_lattice.2.1 orderFour_full_lattice.2.2
218 
219 end
220 end Komorebi.PaperIV

Back to source controls