logicRiemannZeta_eulerProduct_tendsto
plain-language theorem explainer
The declaration shows that finite prime-ledger partitions converge to the Riemann zeta function on recovered complex numbers whose real part exceeds 1. Researchers verifying the analytic substrate in Recognition Science would reference this result when confirming the Euler product representation. The argument reduces directly to the corresponding convergence theorem on Mathlib complexes by applying the transport map.
Claim. Let $s$ be a recovered complex number. If the real part of the transported value of $s$ exceeds 1, then the sequence of finite prime-ledger partitions over the primes below $n$, as $n$ tends to infinity, converges to the Riemann zeta function evaluated at the transported value of $s$.
background
LogicComplex is the structure carrying recovered real and imaginary parts. The map toComplex sends such an object to an element of Mathlib's complex numbers. The function logicRiemannZeta is defined by composing the standard Riemann zeta with this transport. The module provides a compatibility layer that reuses Mathlib's analytic substrate rather than rebuilding contour integration or holomorphy from recovered primitives. The upstream ledger_partition_equals_zeta theorem states that these partitions converge to riemannZeta on the half-plane Re(s) > 1.
proof idea
The proof is a one-line wrapper. It applies the ledger_partition_equals_zeta theorem to the image of s under toComplex, using the hypothesis that the real part exceeds 1, and then simplifies the target using the definition of logicRiemannZeta.
why it matters
This result supplies the Euler product field in the logicComplexAnalyticSubstrateCert, which certifies Phase 2 compatibility between recovered complexes and the standard analytic substrate. It embeds the classical Euler product for the zeta function into the Recognition Science foundation by transport. The construction aligns with the use of Mathlib ℂ for all analytic statements in the compatibility module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.