rs_riemannZeta_eulerProduct_tprod
plain-language theorem explainer
The theorem states that the infinite Euler product over all primes of (1 - p^{-s})^{-1} equals the Riemann zeta function for complex s with real part exceeding 1. Researchers developing the Recognition Science zeta program cite it to anchor the prime-ledger partition in classical analytic number theory. The proof is a direct one-line wrapper applying Mathlib's riemannZeta_eulerProduct_tprod to the given half-plane hypothesis.
Claim. For a complex number $s$ with real part greater than 1, the product over all primes $p$ of $(1 - p^{-s})^{-1}$ equals the Riemann zeta function $zeta(s)$.
background
The EulerProductEqualsZeta module constitutes Phase 1 of the RS-native zeta program. It wires the formal RS prime-ledger partition, built from the Primes set of natural numbers satisfying the primality predicate, to Mathlib's classical result that the Euler product converges to riemannZeta on the half-plane Re(s) > 1. The module's explicit goal is to replace an earlier True stub inside EulerLedgerPartitionCert with a genuine analytic theorem rather than reprove continuation.
proof idea
The proof is a one-line wrapper that applies the Mathlib theorem riemannZeta_eulerProduct_tprod directly to the hypothesis hs.
why it matters
This declaration supplies the analytic identity required for the RS zeta program, equating the product over prime ledger atoms to zeta(s) in the classically valid domain. It closes the placeholder left by the stub in EulerLedgerPartitionCert and thereby opens the path to later links with the Recognition Composition Law and the phi-ladder. No downstream uses are yet recorded, leaving open the question of how the identity will be lifted into the full Recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.