primeLedgerLocalPartition
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.