SemanticChecks.lean

1 import KomorebiPaperIV.DiagonalFredholm
2 import KomorebiPaperIV.NormalizedZeroBell
3 import KomorebiPaperIV.NormalizedExactOrder
4 import KomorebiPaperIV.SecantAsymptotic
5 import KomorebiPaperIV.SharpGrowth
6 import KomorebiPaperIV.IndicatorLimit
7 import KomorebiPaperIV.CubicZeroCorrection
8 import KomorebiPaperIV.DerivativeWeightedZeta
9 import KomorebiPaperIV.ZeroZetaConvergence
10 import KomorebiPaperIV.LargeZeroCompletion
11 import KomorebiPaperIV.ZeroSequenceCounting
12 import KomorebiPaperIV.ReducedCanonicalProduct
13 import KomorebiPaperIV.ExactZetaModels
14 import KomorebiPaperIV.CanonicalProductQuotient
15 import KomorebiPaperIV.Wronskians
16 import KomorebiPaperIV.BellCompletion
17 import KomorebiPaperIV.CompanionBridge
18 import KomorebiPaperIV.ExponentialBounds
19 import KomorebiPaperIV.CompanionSpectrum
20 import KomorebiPaperIV.ZeroGeometry
21 import KomorebiPaperIV.ZeroMomentLogarithm
22 import KomorebiPaperIV.ThetaZeroBell
23 
24 import KomorebiPaperIV.SignedZeroCorrection
25 import KomorebiPaperIV.SignedDerivativeAsymptotics
26 import KomorebiPaperIV.SignedDominance
27 
28 /-! Independent closed specializations of the new public API. -/
29 
30 namespace Komorebi.PaperIVChecks
31 open Komorebi.PaperIV
32 
33 /-- The entire signed denominator at order two is actually cosine. -/
34 theorem signed_two_cos (z : ℂ) :
35     entireSigned 2 0 (-1) Complex.I z = Complex.cos z := by
36   rw [entireSigned_zero_eq_average]
37   simp [Finset.sum_range_succ, Complex.cos, mul_comm]
38   ring
39 
40 /-- Nonvacuity of the signed Wronskian hypotheses. -/
41 theorem signed_two_wronskian (z : ℂ) :
42     analyticWronskian (fun j : Fin 2 => entireSigned 2 j.val (-1) Complex.I) z = 1 := by
43   apply signedWronskian_eq_one (by decide)
44   · exact IsPrimitiveRoot.neg_one 0 (by decide)
45   · exact Complex.I_sq
46 
47 /-- The transfer Wronskian has the required dependence on the scale. -/
48 theorem transfer_two_wronskian (lambda z : ℂ) :
49     analyticWronskian (fun j : Fin 2 => entireTransfer 2 j.val (-1) lambda) z = lambda := by
50   simpa using transferWronskian_eq (by decide : 1 < 2)
51     (IsPrimitiveRoot.neg_one 0 (by decide) : IsPrimitiveRoot (-1 : ℂ) 2) lambda z
52 
53 /-- A positive-degree reciprocal polynomial vanishes at parameter zero. -/
54 theorem reciprocal_positive_zero (N : ℕ) {n : ℕ} (hn : 0 < n) :
55     (reciprocalCoeffPolynomialOver (K := ℂ) N n).eval 0 = 0 := by
56   rw [eval_reciprocalCoeffPolynomialOver, reciprocalCoeff_zero_parameter_of_pos N hn]
57 
58 /-- A concrete degree-two leading coefficient checks the factorial normalization. -/
59 theorem reciprocal_two_leading :
60     (reciprocalCoeffPolynomialOver (K := ℂ) 2 2).coeff 2 = 3 := by
61   rw [coeff_reciprocalCoeffPolynomialOver_parameterDegree]
62   norm_num
63 
64 /-- Determinant one holds at an odd order, without root-certificate arguments. -/
65 theorem companion_three_det (z : ℂ) : (signedFundamentalMatrix 3 z).det = 1 :=
66   signedFundamentalMatrix_det_one (by decide) z
67 
68 /-- The real root -1 appears in the odd-order spectrum. -/
69 theorem companion_three_negative_eigenvalue :
70     (-1 : ℂ) ∈ spectrum ℂ (signedShiftMatrix (R := ℂ) 3) := by
71   rw [signedShiftMatrix_mem_spectrum_iff (by decide)]
72   norm_num
73 
74 /-- The first positive cosine zero has analytic multiplicity exactly one. -/
75 theorem signed_two_first_zero_simple :
76     analyticOrderAt (entireSigned 2 0 (-1) Complex.I) ((Real.pi : ℂ) / 2) = 1 := by
77   apply entireSigned_two_zero_order_one (IsPrimitiveRoot.neg_one 0 (by decide)) Complex.I_sq
78   rw [entireSigned_two_zero_iff (IsPrimitiveRoot.neg_one 0 (by decide)) Complex.I_sq]
79   exact ⟨0, by norm_num⟩
80 
81 /-- Exact cancellation is included in the quantitative uniqueness theorem. -/
82 theorem exact_cancellation_unique :
83     ∃! k : ℤ, ‖(Real.pi : ℂ) * Complex.I - oddExponentialCenter k‖ ≤ 0 := by
84   have h := near_cancellation_unique (w := (Real.pi : ℂ) * Complex.I)
85     (by simp [Complex.exp_pi_mul_I])
86   simpa [Complex.exp_pi_mul_I] using h
87 
88 end Komorebi.PaperIVChecks
89 
90 namespace Komorebi.PaperIVChecks
91 open Komorebi.PaperIV
92 
93 /-- A concrete quarter-turn preserves the actual order-four denominator. -/
94 theorem quartic_quarter_turn (z : ℂ) :
95     canonicalSignedDenominator 4 (Complex.I * z) = canonicalSignedDenominator 4 z := by
96   apply canonicalSignedDenominator_rotation (by decide)
97   norm_num [show Complex.I ^ 4 = (Complex.I ^ 2) ^ 2 by ring, Complex.I_sq]
98 
99 /-- The same quarter-turn has the inverse derivative weight. -/
100 theorem quartic_derivative_quarter_turn (z : ℂ) :
101     deriv (canonicalSignedDenominator 4) (Complex.I * z) * Complex.I =
102       deriv (canonicalSignedDenominator 4) z := by
103   apply canonicalSignedDenominator_derivative_rotation (by decide)
104   norm_num [show Complex.I ^ 4 = (Complex.I ^ 2) ^ 2 by ring, Complex.I_sq]
105 
106 /-- The derived cubic strip width is log(2)/sqrt(3). -/
107 theorem cubic_sector_width : signedSectorWidth 3 = Real.log 2 / Real.sqrt 3 := by
108   unfold signedSectorWidth
109   norm_num [Real.sin_pi_div_three]
110   ring
111 
112 #print axioms quartic_quarter_turn
113 #print axioms quartic_derivative_quarter_turn
114 #print axioms cubic_sector_width
115 end Komorebi.PaperIVChecks
116 
117 #print axioms Komorebi.PaperIVChecks.signed_two_cos
118 #print axioms Komorebi.PaperIVChecks.signed_two_wronskian
119 #print axioms Komorebi.PaperIVChecks.transfer_two_wronskian
120 #print axioms Komorebi.PaperIVChecks.reciprocal_positive_zero
121 #print axioms Komorebi.PaperIVChecks.reciprocal_two_leading
122 #print axioms Komorebi.PaperIVChecks.companion_three_det
123 #print axioms Komorebi.PaperIVChecks.companion_three_negative_eigenvalue
124 #print axioms Komorebi.PaperIVChecks.signed_two_first_zero_simple
125 #print axioms Komorebi.PaperIVChecks.exact_cancellation_unique
126 
127 namespace Komorebi.PaperIVChecks
128 open Komorebi.PaperIV
129 
130 /-- A nonzero positive constant remainder exercises the local existence theorem. -/
131 theorem nonzero_remainder_unique_zero :
132     ∃! z : ℂ, z ∈ Metric.closedBall ((Real.pi : ℂ) * Complex.I) 1 ∧
133       1 + Complex.exp z + (1 / 4 : ℂ) = 0 := by
134   have h := perturbed_exponential_unique_zero (a := 1)
135     (t := (Real.pi : ℂ) * Complex.I) (R := fun _ => (1 / 4 : ℂ))
136     (R' := fun _ => (0 : ℂ)) (by norm_num)
137     (by simp)
138     (by intro z hz; norm_num)
139     (by intro z hz; exact hasDerivAt_const z (1 / 4 : ℂ))
140     (by intro z hz; norm_num)
141   simpa using h
142 
143 /-- The cubic polygon has the exact spectral gap 3/2. -/
144 theorem cubic_polygon_gap : signedPolygonGap 3 = 3 / 2 := by
145   unfold signedPolygonGap
146   norm_num only [Nat.cast_ofNat, Real.cos_pi_div_three,
147     show 3 * (Real.pi / 3) = Real.pi by ring, Real.cos_pi]
148 
149 #print axioms nonzero_remainder_unique_zero
150 #print axioms cubic_polygon_gap
151 end Komorebi.PaperIVChecks
152 
153 namespace Komorebi.PaperIVChecks
154 open Komorebi.PaperIV
155 
156 theorem reduced_two_first_zero :
157     entireReducedDenominator 2 (((Real.pi : ℂ) / 2) ^ 2) = 0 := by
158   apply entireReducedDenominator_two_zero_iff.mpr
159   exact ⟨0, by norm_num; ring⟩
160 
161 theorem reduced_two_negative_nonzero : entireReducedDenominator 2 (-1) ≠ 0 := by
162   intro h
163   obtain ⟨m, hm⟩ := entireReducedDenominator_two_zero_iff.mp h
164   have he := congrArg Complex.re hm
165   have hp : 0 ≤ (((m : ℝ) + 1 / 2) * Real.pi) ^ 2 := sq_nonneg _
166   have hr : (((m : ℂ) + 1 / 2) * Real.pi) = ((((m : ℝ) + 1 / 2) * Real.pi : ℝ) : ℂ) := by push_cast; rfl
167   rw [hr, ← Complex.ofReal_pow] at he
168   change (-1 : ℝ) = (((m : ℝ) + 1 / 2) * Real.pi) ^ 2 at he
169   linarith
170 
171 theorem cubic_reduced_reciprocals_summable :
172     Summable (fun m => 1 / reducedPositiveZero 3 m) :=
173   reducedPositiveZero_reciprocal_summable (by norm_num)
174 
175 theorem cubic_critical_exponent_diverges :
176     ¬ Summable (fun m => 1 / reducedPositiveZero 3 m ^ (1 / 3 : ℝ)) := by
177   rw [reducedPositiveZero_reciprocal_rpow_summable_iff (by norm_num)]
178   norm_num
179 
180 #print axioms reduced_two_first_zero
181 #print axioms reduced_two_negative_nonzero
182 #print axioms cubic_reduced_reciprocals_summable
183 #print axioms cubic_critical_exponent_diverges
184 end Komorebi.PaperIVChecks
185 
186 namespace Komorebi.PaperIVChecks
187 open Komorebi.PaperIV
188 
189 /-- An exceptional zero of order three must contribute three, not one. -/
190 theorem triple_zero_weight : analyticZeroCount (fun z : ℂ => z ^ 3) 1 = 3 := by
191   have hz : zeroDisk (fun z : ℂ => z ^ 3) 1 = {0} := by
192     ext z
193     simp only [zeroDisk, Set.mem_ofPred_eq, pow_eq_zero_iff (by norm_num : (3 : ℕ) ≠ 0), Set.mem_singleton_iff]
194     constructor
195     · exact fun h => h.2
196     · intro h; subst z; norm_num
197   rw [analyticZeroCount, hz, finiteWeight_of_finite _ (Set.finite_singleton 0)]
198   rw [Set.Finite.toFinset_singleton, Finset.sum_singleton]
199   change analyticOrderNatAt ((id : ℂ → ℂ) ^ 3) 0 = 3
200   rw [analyticOrderNatAt_pow (show AnalyticAt ℂ (id : ℂ → ℂ) 0 from analyticAt_id)]
201   norm_num [analyticOrderNatAt, show (fun z : ℂ => z) = id from rfl]
202 
203 /-- The cosine disk count has the classical density 2/pi. -/
204 theorem cosine_full_count_density :
205     ∃ K : ℝ, 0 < K ∧ ∀ R : ℝ, 0 ≤ R →
206       |(analyticZeroCount (canonicalSignedDenominator 2) R : ℝ) - (2 / Real.pi) * R| ≤ K := by
207   simpa only [Nat.cast_ofNat, Real.sin_pi_div_two, mul_one] using
208     canonicalSignedDenominator_zero_counting (by norm_num : 2 ≤ 2)
209 
210 /-- The full cosine zero multiset diverges at its critical exponent. -/
211 theorem cosine_full_critical_exponent_diverges :
212     ¬ ZeroPowerSummable (canonicalSignedDenominator 2) 1 := by
213   rw [canonicalSignedDenominator_zero_power_summable_iff (by norm_num)]
214   norm_num
215 
216 /-- Every reduced cosine zero, including the finite prefix, is included. -/
217 theorem reduced_cosine_full_reciprocals_summable :
218     ZeroPowerSummable (entireReducedDenominator 2) 1 :=
219   entireReducedDenominator_reciprocal_zeros_summable (by norm_num)
220 
221 /-- A nonreal point on the boundary still fails absolute convergence. -/
222 theorem cubic_zeta_nonreal_boundary_diverges :
223     ¬ Summable (fun z => ‖absoluteZeroZetaTerm (entireReducedDenominator 3) z
224       (1 / 3 + 7 * Complex.I)‖) := by
225   rw [entireReducedDenominator_zeta_absolute_convergence (by norm_num)]
226   norm_num
227 
228 /-- The reduced cubic zeta is holomorphic at a genuinely complex interior point. -/
229 theorem cubic_zeta_interior_holomorphic :
230     DifferentiableAt ℂ (absoluteZeroZeta (entireReducedDenominator 3)) (1 + 7 * Complex.I) := by
231   apply (entireReducedDenominator_zeta_holomorphic (by norm_num : 2 ≤ 3)).differentiableAt
232   apply (isOpen_lt continuous_const Complex.continuous_re).mem_nhds
233   norm_num
234 
235 #print axioms triple_zero_weight
236 #print axioms cosine_full_count_density
237 #print axioms cosine_full_critical_exponent_diverges
238 #print axioms reduced_cosine_full_reciprocals_summable
239 #print axioms cubic_zeta_nonreal_boundary_diverges
240 #print axioms cubic_zeta_interior_holomorphic
241 end Komorebi.PaperIVChecks
242 
243 namespace Komorebi.PaperIVChecks
244 open Komorebi.PaperIV
245 
246 /-- The explicit correction alternates: its first two values have opposite signs. -/
247 theorem cubic_correction_even_positive : 0 < (signedLeadingCorrection 3 0).re := by
248   rw [signedLeadingCorrection_three]
249   norm_num only [pow_zero, Complex.ofReal_re]
250   positivity
251 
252 theorem cubic_correction_odd_negative : (signedLeadingCorrection 3 1).re < 0 := by
253   rw [signedLeadingCorrection_three]
254   norm_num only [pow_one, Complex.ofReal_re]
255   have hs : 0 < Real.sqrt 3 := Real.sqrt_pos.mpr (by norm_num)
256   have he := Real.exp_pos (-3 * signedZeroCenter 3 1 / 2)
257   exact mul_neg_of_neg_of_pos (div_neg_of_neg_of_pos (by norm_num) hs) he
258 
259 /-- Principal logarithms give a concrete entire derivative-weighted cubic zeta;
260 the branch hypotheses are satisfied, not merely assumed by this check. -/
261 theorem cubic_principal_derivative_zeta_entire :
262     Differentiable ℂ (derivativeWeightedZeroZeta 3 1 (fun z => Complex.log z.val)) := by
263   apply (derivativeWeightedZeroZeta_entire (by norm_num : 3 ≤ 3) (by norm_num : 0 < 1)
264     (fun z => Complex.log z.val) ?_ Real.pi_pos.le ?_).2
265   · intro z
266     apply Complex.exp_log
267     exact norm_pos_iff.mp (zero_norm_pos_of_value_at_zero
268       (by rw [canonicalSignedDenominator_zero (by norm_num : 0 < 3)]; exact one_ne_zero) z.toZero)
269   · intro z
270     simpa only [Complex.log_im] using Complex.abs_arg_le_pi z.val
271 
272 /-- The derivative weight retains its complex sign. It is -1 at the first
273 cosine zero, so replacing the denominator by its norm would fail this test. -/
274 theorem cosine_first_derivative_weight_signed
275     (z : SimpleZeros (canonicalSignedDenominator 2)) (hz : z.val = (Real.pi : ℂ) / 2) :
276     derivativeZeroWeight 2 1 z = -1 := by
277   have he : canonicalSignedDenominator 2 = Complex.cos := funext
278     (entireSigned_two_eq_cos (canonicalPrimitiveRoot_isPrimitive (by norm_num : 0 < 2))
279       (canonicalSignedRoot_pow (by norm_num : 0 < 2)))
280   simp only [derivativeZeroWeight, he, Complex.deriv_cos, hz, Complex.sin_pi_div_two,
281     pow_one, inv_neg, inv_one]
282 
283 #print axioms cubic_correction_even_positive
284 #print axioms cubic_correction_odd_negative
285 #print axioms cubic_principal_derivative_zeta_entire
286 #print axioms cosine_first_derivative_weight_signed
287 end Komorebi.PaperIVChecks
288 
289 namespace Komorebi.PaperIVChecks
290 open Komorebi.PaperIV
291 
292 /-- Original and reduced zeta really have different pole locations in order two. -/
293 theorem orderTwo_distinct_pole_locations :
294     meromorphicOrderAt (reducedZetaContinuation (by norm_num : 2 ≤ 2)) (1 / 2 : ℂ) = (-1 : ℤ) ∧
295     DifferentiableAt ℂ (absoluteZetaContinuation (by norm_num : 2 ≤ 2)) (1 / 2 : ℂ) := by
296   constructor
297   · exact reducedZetaContinuation_simple_pole (by norm_num)
298   · exact absoluteZetaContinuation_holomorphic_off_pole (by norm_num) (by norm_num)
299 
300 /-- The explicit quartic zero calculation agrees with the global comparison. -/
301 theorem orderFour_correction_vanishes :
302     absoluteZetaCorrection (by norm_num : 2 ≤ 4) = 0 ∧
303     reducedZetaCorrection (by norm_num : 2 ≤ 4) = 0 := orderFour_zeta_corrections_zero
304 
305 /-- The complete product retains the actual multiplicity of the first reduced cosine zero. -/
306 theorem first_cosine_reduced_product_order :
307     analyticOrderAt (fullCanonicalProduct (entireReducedDenominator 2))
308       (((Real.pi : ℂ) / 2) ^ 2) = 1 := by
309   rw [entireReducedDenominator_full_product_same_orders (by norm_num)]
310   apply entireReducedDenominator_two_zero_order_one
311   rw [← canonicalSignedDenominator_eq_reduced_power (by norm_num)]
312   exact (entireSigned_two_zero_iff_nat (canonicalPrimitiveRoot_isPrimitive (by norm_num))
313     (canonicalSignedRoot_pow (by norm_num))).mpr ⟨0, Or.inl (by norm_num; ring)⟩
314 
315 end Komorebi.PaperIVChecks
316 
317 #print axioms Komorebi.PaperIVChecks.orderTwo_distinct_pole_locations
318 #print axioms Komorebi.PaperIVChecks.orderFour_correction_vanishes
319 #print axioms Komorebi.PaperIVChecks.first_cosine_reduced_product_order
320 
321 namespace Komorebi.PaperIVChecks
322 open Komorebi.PaperIV
323 
324 /-- The new full product includes the smallest allowed order, where the
325 original entire denominator is cosine. -/
326 theorem cosine_complete_product (z : ℂ) :
327     Complex.cos z = ∏' i : ZeroMultiplicityIndex (entireReducedDenominator 2),
328       (1 - z ^ 2 / indexedZero i) := by
329   rw [← canonicalSignedDenominator_hadamard (by decide : 2 ≤ 2)]
330   exact (entireSigned_two_eq_cos (canonicalPrimitiveRoot_isPrimitive (by decide : 0 < 2)) (canonicalSignedRoot_pow (by decide : 0 < 2)) z).symm
331 
332 /-- Newton's first step tests the sign and factorial against a known value. -/
333 theorem cosine_first_zero_moment :
334     zeroPowerSum (entireReducedDenominator 2) 1 = (1 / 2 : ℂ) := by
335   have h := reducedZeroPowerSum_newton (by decide : 2 ≤ 2) 0
336   norm_num [coeff_reducedDenominator] at h
337   exact h
338 
339 /-- The second moment tests the nontrivial convolution term in Newton's rule. -/
340 theorem cosine_second_zero_moment :
341     zeroPowerSum (entireReducedDenominator 2) 2 = (1 / 6 : ℂ) := by
342   have h := reducedZeroPowerSum_newton (by decide : 2 ≤ 2) 1
343   norm_num [Finset.sum_range_succ, coeff_reducedDenominator, cosine_first_zero_moment] at h
344   exact h
345 
346 /-- The zero-data Bell formula retains the empty Bell polynomial at n=0. -/
347 theorem reciprocal_zero_data_constant (r : ℂ) : reciprocalCoeff 3 0 r = 1 := by
348   rw [reciprocalCoeff_zero_sum_bell (by decide : 2 ≤ 3)]
349   simp
350 
351 #print axioms cosine_complete_product
352 #print axioms cosine_first_zero_moment
353 #print axioms cosine_second_zero_moment
354 #print axioms reciprocal_zero_data_constant
355 end Komorebi.PaperIVChecks
356 
357 
358 namespace Komorebi.PaperIVChecks
359 open Komorebi.PaperIV Filter
360 open scoped Topology
361 
362 /-- Cosine on the real axis exercises a tie direction with infinitely many zeros. -/
363 theorem cosine_real_axis_indicator :
364     limsup (fun r : ℝ => Real.log ‖canonicalSignedDenominator 2 (r : ℂ)‖ / r) atTop = 0 := by
365   have h := canonicalSignedDenominator_indicator (by decide : 2 ≤ 2) 0
366   have hp (k : ℕ) (hk : k < 2) : signedProjection 2 0 k = 0 := by
367     interval_cases k
368     · norm_num [signedProjection_cos]
369     · rw [signedProjection_cos]
370       norm_num only [Nat.cast_one, Nat.cast_ofNat]
371       rw [show (0 : ℝ) + 3 * (Real.pi / 2) = Real.pi / 2 + Real.pi by ring,
372         Real.cos_add_pi, Real.cos_pi_div_two, neg_zero]
373   have hi : signedIndicator 2 (by decide) 0 = 0 := by
374     apply le_antisymm
375     · exact (Finset.sup'_le_iff _ _).mpr (fun k hk => (hp k (Finset.mem_range.mp hk)).le)
376     · exact signedIndicator_nonneg (by decide) 0
377   simpa only [hi, rayDirection, Complex.ofReal_zero, zero_mul, Complex.exp_zero, mul_one] using h
378 
379 /-- The reduced quartic has growth order 1/4, rather than the original order one. -/
380 theorem reduced_quartic_sharp_order : entireGrowthOrder (entireReducedDenominator 4) = (1 / 4 : ℝ) := by
381   simpa using entireReducedDenominator_order_exact (by decide : 0 < 4)
382 
383 /-- The signed cubic has exact type one despite its smaller growth on the real axis. -/
384 theorem cubic_sharp_type : entireExponentialType (canonicalSignedDenominator 3) = 1 :=
385   canonicalSignedDenominator_type_one (by decide)
386 
387 /-- Negative imaginary phases use positive radii and still align exactly. -/
388 theorem negative_phase_aligned_radius : alignedRadii (-1) 2 = 4 * Real.pi := by
389   norm_num [alignedRadii]
390   ring
391 
392 #print axioms cosine_real_axis_indicator
393 #print axioms reduced_quartic_sharp_order
394 #print axioms cubic_sharp_type
395 #print axioms negative_phase_aligned_radius
396 end Komorebi.PaperIVChecks
397 
398 namespace Komorebi.PaperIVChecks
399 open Komorebi.PaperIV
400 noncomputable section
401 -- The order-one boundary is retained even though the zero-product theorem requires N>=2.
402 theorem normalized_order_one : entireGrowthOrder (entireNormalizedSection 1 0) = 1 := by
403   simpa using entireNormalizedSection_order_exact (by norm_num : 0 < 1) (by norm_num : 0 < 1)
404 
405 -- Actual normalized-section zeros have a negative first reciprocal moment: the sign is essential.
406 theorem normalized_first_zero_moment : zeroPowerSum (entireNormalizedSection 2 1) 1 = -(1/6 : ℂ) := by
407   have h := normalized_zeroPowerSum (by norm_num : 2 ≤ 2) 1 0
408   norm_num [coeff_one_normalizedResidueNegativeLog] at h
409   exact h
410 
411 -- The actual Hilbert-space diagonal operator has the denominator's first logarithmic moment.
412 theorem diagonal_trace_cosine : hilbertBasisTrace (diagonalHilbertBasis (ZeroMultiplicityIndex (entireReducedDenominator 2)))
413     (reducedZeroOperator 2) = (1/2 : ℂ) := by
414   have h := reducedZeroOperator_trace_power (by norm_num : 2 ≤ 2) (by norm_num : 0 < 1)
415     (diagonalHilbertBasis (ZeroMultiplicityIndex (entireReducedDenominator 2)))
416   norm_num [kappaCoeff, coeff_one_negativeLogDenominator] at h
417   exact h
418 
419 -- Integer order zero repeats no variables and kills every positive-degree reciprocal coefficient.
420 theorem symmetric_zero_order : completeHomogeneous (repeatedEigenvalue
421     (fun i : ZeroMultiplicityIndex (entireReducedDenominator 2) => (indexedZero i)⁻¹) 0) 1 = 0 := by
422   have h := reciprocalCoeff_completeHomogeneous (by norm_num : 2 ≤ 2) 1 0
423   simpa [reciprocalCoeff, blockCoeff, reciprocalSeries_zero] using h.symm
424 end
425 end Komorebi.PaperIVChecks
426 
427 #print axioms Komorebi.PaperIVChecks.normalized_order_one
428 #print axioms Komorebi.PaperIVChecks.normalized_first_zero_moment
429 #print axioms Komorebi.PaperIVChecks.diagonal_trace_cosine
430 #print axioms Komorebi.PaperIVChecks.symmetric_zero_order

Back to source controls