primeLedgerLocalPartition
The local geometric partition factor for a single prime ledger atom at complex parameter s is the reciprocal of one minus the posting weight. Number theorists extending Euler products to ledger structures in Recognition Science cite this when assembling finite prime decompositions of the partition function. The definition proceeds by direct algebraic inversion of the weight term.
claimFor complex number $s$ and natural number $p$, the local partition factor attached to the prime ledger atom equals $(1 - w(s,p))^{-1}$, where $w$ denotes the prime posting weight.
background
The Euler Ledger Partition module packages the Euler product as the partition function of independent prime-ledger postings. Finite product statements are proved directly; the infinite equality with riemannZeta is isolated in a separate certificate because the exact Mathlib Euler-product API forms an analytic import boundary rather than Recognition Science structure. The local factor is attached to one prime ledger atom. Upstream, LedgerFactorization supplies the structure of positive reals under multiplication together with J calibration, while PhysicsComplexityStructure records that J-cost minimization is convex with unique global minimum at unity.
proof idea
One-line definition that inverts the prime posting weight at the supplied complex parameter and natural number.
why it matters in Recognition Science
This supplies the atomic building block for finitePrimeLedgerPartition and eulerLedgerPartitionCert, which recovers the Riemann zeta function on Re(s) > 1 via the finite prime-ledger partitions. It realizes the multiplicative decomposition required by the ledger factorization structure, consistent with the Recognition Science treatment of the Euler product as arising from independent prime postings.
scope and limits
- Does not prove equality of the infinite product to the Riemann zeta function.
- Does not address convergence of the product for Re(s) <= 1.
- Does not compute explicit numerical values for any prime.
- Does not restrict the domain of the complex parameter s.
formal statement (Lean)
29def primeLedgerLocalPartition (s : ℂ) (p : ℕ) : ℂ :=
proof body
Definition body.
30 (1 - primePostingWeight s p)⁻¹
31
32/-- A finite prime-ledger partition over a finite set of primes. -/