PrimeLedgerPartition
plain-language theorem explainer
PrimeLedgerPartition defines the formal Euler ledger partition for a complex s as the existence of a function F from finite sets of naturals to complexes that agrees with the finite prime-ledger product on every finite set. Number theorists formalizing Euler products or zeta factorizations cite this when isolating the formal structure before convergence arguments. It is realized directly as an existential quantification over the finitePrimeLedgerPartition construction.
Claim. For a complex number $s$, the prime ledger partition at $s$ holds when there exists a map $F$ from finite sets of natural numbers to complex numbers such that $F(S)$ equals the product over primes $p$ in $S$ of the local partition value at $p$ (or 1 for non-primes) for every finite set $S$.
background
This module packages the Euler product as the partition function of independent prime-ledger postings. The finitePrimeLedgerPartition is the product over a finite set $S$ of the local partition at each prime (defaulting to 1 otherwise). The local theoretical setting isolates formal finite products, with the infinite equality to riemannZeta deferred to EulerLedgerPartitionCert because the exact Mathlib Euler-product API is an analytic import boundary rather than RS structure.
proof idea
This is a direct definition that asserts existence of a function $F$ pointwise equal to finitePrimeLedgerPartition on all finite sets. It functions as a one-line wrapper lifting the finite product construction to a formal infinite statement without additional lemmas.
why it matters
This definition supplies the formal partition object that primeLedgerPartition_formal proves exists and that EulerLedgerPartitionCert employs to connect finite products to zeta for Re(s) > 1. It fills the formal partition step in the Euler ledger packaging before analytic arguments. In the Recognition framework it supports the number-theoretic backbone for structures that may link to constants derived from zeta or Euler products.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.