det2_log_factor_bound
plain-language theorem explainer
The theorem supplies the uniform bound |det2LogFactor p σ| ≤ p^{-2σ}/(1 - p^{-σ}) for each prime p when σ > 1/2. Workers on the Euler-product instantiation of the RS carrier would cite the estimate to control the prime sum that appears in the logarithm of the regularized determinant. The argument substitutes x = p^{-σ}, invokes the contraction 0 < x < 1 from the eigenvalue lemmas, and reduces the claim to the standard geometric-series bound on |log(1 - x) + x|.
Claim. For real σ > 1/2 and prime p, |log det₂_factor(p, σ)| ≤ p^{-2σ} / (1 - p^{-σ}).
background
The EulerInstantiation module realizes the abstract RS carrier/sensor framework by taking the Euler product of the zeta function as the concrete operator A(σ). Its core objects are the prime sum PrimeSum σ = ∑_p p^{-σ}, the Hilbert-Schmidt norm squared HilbertSchmidtNorm σ = ∑_p p^{-2σ}, and the carrier log series built from the local factors det2LogFactor p σ = log(1 - p^{-σ}) + p^{-σ}. The module sits between the annular-cost axioms and the cost-covering bridge, showing that the resulting C(σ) = det₂²(I - A(σ)) is holomorphic and non-vanishing for Re(s) > 1/2.
proof idea
The tactic proof sets x := p^{-σ}, obtains 0 < x < 1 from eigenvalue_pos and eigenvalue_lt_one, applies the general inequality Real.abs_log_sub_add_sum_range_le to the partial sum of the logarithm series, simplifies the finite sum to x, and rewrites the resulting bound x²/(1 - x) back into powers of p.
why it matters
The local bound feeds directly into det2_log_summable, which establishes absolute convergence of the log-determinant series and therefore that the Euler product satisfies the EulerCarrier interface. This step completes the concrete-to-abstract instantiation chain required for the cost-covering axiom to apply, recovering the conditional Riemann hypothesis inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.