finitePrimeLedgerPartition
plain-language theorem explainer
The finite prime-ledger partition supplies the partial product over any finite set S of naturals, multiplying the local ledger factor only when the entry is prime. Analytic number theorists in the Recognition Science setting cite it to build finite approximations to the Euler product before passing to the zeta limit. The definition is a direct product expression that conditions on primality via the local partition attached to each prime atom.
Claim. For $s : ℂ$ and finite $S : Finset ℕ$, the finite prime-ledger partition equals $∏_{p ∈ S} (1 - w(s,p))^{-1}$ when $p$ is prime and $1$ otherwise, where $w(s,p)$ is the prime posting weight and the local factor is supplied by primeLedgerLocalPartition.
background
The Euler Ledger Partition module packages the Euler product as the partition function of independent prime-ledger postings. Finite products are handled directly while the infinite equality with riemannZeta is isolated in EulerLedgerPartitionCert because the exact Mathlib Euler-product API is an analytic import boundary. primeLedgerLocalPartition attaches a local geometric partition to one prime ledger atom via the explicit formula (1 - primePostingWeight s p)^{-1}. Prime is the transparent repo-local alias for Nat.Prime. Upstream results include the local partition definition itself together with structural certificates such as OptionAEmpiricalProgram.is and SimplicialLedger.EdgeLengthFromPsi.is that supply the ledger-atom primitives.
proof idea
The declaration is a one-line definition that unfolds directly to the product over S, inserting the local factor primeLedgerLocalPartition s p precisely when Nat.Prime p holds and 1 otherwise.
why it matters
This definition supplies the finite approximations required by the EulerLedgerPartitionCert structure, whose eulerProduct_eq_zeta field asserts that the limit of finitePrimeLedgerPartition s (Nat.primesBelow n) equals riemannZeta s for Re(s) > 1. It is invoked in logicRiemannZeta_eulerProduct_tendsto to transport the Euler product to recovered complex numbers and in the sibling theorems finitePrimeLedgerPartition_insert_prime and finitePrimeLedgerPartition_insert_nonprime that establish the multiplicative and insensitivity properties. The construction realizes the Recognition Science view of the Euler product as a partition function over prime-ledger atoms, consistent with the eight-tick octave and the RCL composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.