rs_riemannZeta_eulerProduct_hasProd
plain-language theorem explainer
rs_riemannZeta_eulerProduct_hasProd states that for complex s with real part greater than 1 the infinite product over primes of (1 - p^{-s})^{-1} equals the Riemann zeta function at s. Number theorists connecting prime-ledger constructions to classical analytic number theory would cite the result. The proof is a one-line term wrapper that invokes the corresponding Mathlib theorem on Euler products.
Claim. For a complex number $s$ with real part exceeding 1, the product over all primes $p$ of $(1 - p^{-s})^{-1}$ converges to the Riemann zeta function evaluated at $s$.
background
The module EulerProductEqualsZeta forms phase 1 of the RS-native zeta program. It replaces an earlier True stub in EulerLedgerPartitionCert by wiring the formal RS prime-ledger partition directly to Mathlib's classical result that the Euler product equals zeta on the half-plane Re(s) > 1. The local setting is the set of prime numbers defined as Primes := {n | Nat.Prime n}, with the product taken over this set in the HasProd sense.
proof idea
The proof is a one-line term wrapper that applies the Mathlib theorem riemannZeta_eulerProduct_hasProd directly to the hypothesis hs.
why it matters
This theorem supplies the first verified analytic link between the RS prime-ledger partition and the classical Euler product identity for zeta. It closes the placeholder in EulerLedgerPartitionCert for the region Re(s) > 1 and supports later extensions of zeta constructions inside the Recognition Science framework. No downstream uses appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.