PrimeLedgerPartition
PrimeLedgerPartition(s) asserts the existence of a map from finite sets of natural numbers to complex numbers that reproduces the finite prime-ledger partition for every input set. Number theorists formalizing the Euler product representation in Recognition Science cite this when building the formal object over prime atoms. The definition is realized as a direct existential wrapper around the finite product construction.
claimThe proposition PrimeLedgerPartition(s) holds if there exists a function $F$ from finite subsets of natural numbers to complex numbers such that $F(S)$ equals the finite prime-ledger partition of $s$ over $S$ for every finite set $S$.
background
The Euler Ledger Partition module packages the Euler product as the partition function of independent prime-ledger postings. Finite products are proved directly; the infinite equality with riemannZeta is isolated in EulerLedgerPartitionCert because the exact Mathlib Euler-product API is an analytic import boundary rather than RS structure.
proof idea
The definition directly encodes the required existence using the finite prime-ledger partition. It is a one-line wrapper that applies finitePrimeLedgerPartition to witness the existential quantifier over all finite sets S.
why it matters in Recognition Science
This definition supplies the formal prime-ledger partition object that EulerLedgerPartitionCert relies on to certify agreement with riemannZeta for Re(s) > 1 via convergence of finite partitions. It also supports the theorem primeLedgerPartition_formal. In the Recognition Science framework it formalizes the Euler product over prime atoms, aligning with the prime-ledger postings that underpin the zeta function representation.
scope and limits
- Does not prove convergence of the infinite product for any s.
- Does not equate the partition to the Riemann zeta function.
- Does not define the local partition function primeLedgerLocalPartition.
- Does not address regions where Re(s) <= 1.
formal statement (Lean)
52def PrimeLedgerPartition (s : ℂ) : Prop :=
proof body
Definition body.
53 ∃ F : (Finset ℕ → ℂ), ∀ S, F S = finitePrimeLedgerPartition s S
54
55/-- The formal partition exists, by finite partial products. -/