finitePrimeLedgerPartition_primesBelow
plain-language theorem explainer
The finite prime-ledger partition of s over primes below n equals the partial Euler product over those primes. Number theorists in the Recognition Science zeta program cite this to identify ledger partitions with classical partial products. The proof unfolds the partition definition then applies a finite-set product congruence after extracting primality from the membership predicate.
Claim. For $s$ complex and $n$ a natural number, the finite prime-ledger partition of $s$ over the primes below $n$ equals the product over those primes $p$ of $(1 - p^{-s})^{-1}$.
background
The EulerProductEqualsZeta module forms phase 1 of the RS-native zeta program. It identifies the RS prime-ledger partition, built from local factors on prime atoms via the J-cost and ledger factorization structures, with Mathlib's Euler product. The finite version restricts the product to the finite set of primes below $n$, matching the classical partial product exactly on that set. Upstream structures calibrate the posting weights and J-cost that enter the local factors, while the module replaces an earlier True stub with this concrete equality.
proof idea
The tactic proof unfolds finitePrimeLedgerPartition together with its local partition and posting-weight components. It applies Finset.prod_congr to reduce the claim to a pointwise identity. Inside the congruence, primality of each $p$ is extracted from the Nat.mem_primesBelow membership hypothesis and the local factor is simplified directly from that primality fact.
why it matters
This theorem is invoked by ledger_partition_equals_zeta to obtain the tendsto statement that the RS partitions converge to riemannZeta for Re(s) > 1. It thereby supplies the ledger reading of Mathlib's Euler-product theorem and closes the replacement of the prior True stub in EulerLedgerPartitionCert. The result anchors the prime-ledger atoms in classical analytic number theory while preserving the RS forcing chain and phi-ladder calibration of constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.