det2_log_summable
plain-language theorem explainer
Absolute convergence of the summed logarithms of the per-prime factors holds for σ > 1/2. Analysts studying the holomorphic properties of the regularized determinant det₂(I − A(σ)) cite this result to justify interchanging sums and products in the Euler product. The argument reduces the absolute sum to a constant multiple of the Hilbert-Schmidt series via an explicit per-prime bound and comparison of geometric denominators.
Claim. For real σ > 1/2 the series ∑_{p prime} |log(1 − p^{-σ}) + p^{-σ}| converges.
background
The EulerInstantiation module instantiates the abstract RS carrier from AnnularCost and CostCoveringBridge by realizing the Euler product of ζ(s) as a concrete Hilbert–Schmidt operator A(s) whose regularized determinant supplies the carrier C(s). The per-prime log-factor is given by det2LogFactor(p, σ) := log(1 − p^{-σ}) + p^{-σ}, whose absolute value satisfies the bound |det2LogFactor p σ| ≤ p^{-2σ}/(1 − p^{-σ}) from the upstream theorem det2_log_factor_bound. The comparison series ∑ p^{-2σ} is known to converge for σ > 1/2 by the upstream result hilbert_schmidt_convergent, which states that the squared Hilbert–Schmidt norm of A(s) remains finite in this half-plane.
proof idea
The proof constructs the explicit constant C := 1/(1 − 2^{-σ}) and verifies 0 ≤ C together with positivity of the denominator via linarith. It applies hilbert_schmidt_convergent to obtain summability of the scaled series C ⋅ p^{-2σ}. For each prime the bound from det2_log_factor_bound is invoked; the remaining inequality p^{-2σ}/(1 − p^{-σ}) ≤ C ⋅ p^{-2σ} is established by showing that the reciprocal of the denominator for p is at most C, using rpow monotonicity to compare 2^σ and p^σ and then applying one_div_le_one_div_of_le.
why it matters
This result supplies the absolute summability needed for det2_product_convergent to conclude that the infinite product ∏_p det₂_factor(p, σ) converges, which in turn guarantees that the carrierValue σ is well-defined, positive, and nonvanishing for σ > 1/2 as recorded in carrier_pos. It completes the concrete step in the module’s instantiation chain from primes through the Hilbert–Schmidt operator to a holomorphic nonvanishing C(s) on Re(s) > 1/2, thereby enabling the EulerCarrier interface and the subsequent application of the cost-covering axiom toward conditional RH. Within the Recognition Science framework the convergence supplies the analytic control required for the regularized determinant to function as the carrier in the Euler product instantiation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.