IndisputableMonolith.NumberTheory.EulerProductEqualsZeta
This module restates the Mathlib Euler product theorem for riemannZeta under the RS prime-ledger namespace, isolating convergence of finite prime partial products for Re(s) > 1. Number theorists adapting analytic tools to logic-native primes would cite these declarations to bridge discrete ledger partitions with the zeta function. The structure delegates the infinite-product equality to an analytic import boundary rather than deriving it inside RS.
claimFor Re(s) > 1 the partial products over primes recovered from the logic prime ledger converge to the Riemann zeta function: lim_{N→∞} ∏_{p≤N} (1−p^{−s})^{−1} = ζ(s).
background
The module sits inside the NumberTheory domain and imports EulerLedgerPartition, which packages the Euler product as the partition function of independent prime-ledger postings, and LogicPrimeLedgerAtom, which supplies logic-native prime atoms transported through LogicNat.toNat. The DOC_COMMENT identifies the content as the Mathlib Euler product theorem restated in the RS prime-ledger namespace, with the infinite equality isolated in EulerLedgerPartitionCert because the exact Mathlib API is an analytic import boundary. This supplies the analytic substrate for later compatibility layers without redefining holomorphy or contour integration.
proof idea
This module contains no internal proofs; it imports the Mathlib DirichletLSeries Euler-product results and re-exports them under RS names via the prime-ledger atoms. The finite-product statements are taken directly from the imported EulerLedgerPartition module while the convergence claim for Re(s) > 1 is wrapped as an analytic boundary.
why it matters in Recognition Science
The module feeds LogicComplexCompat, the compatibility layer that makes explicit the decision to use Mathlib ℂ as the analytic substrate rather than redefining complex analysis on recovered numbers. It supplies the Euler-product form of zeta required for any prime-ledger treatment of the Riemann hypothesis, exactly as described in the module DOC_COMMENT.
scope and limits
- Does not derive the Euler product from RS forcing axioms or the J-cost functional.
- Does not establish convergence or analytic continuation for Re(s) ≤ 1.
- Does not prove the Riemann hypothesis or any zero-free region.
- Does not replace Mathlib's complex analysis with a custom recovered-number substrate.