EulerLedgerPartitionCert
plain-language theorem explainer
The analytic certificate asserts that finite prime-ledger partitions converge to the Riemann zeta function for Re(s) > 1, that the formal infinite product over primes exists at every complex scale, and that primes coincide with ledger atoms. Researchers deriving arithmetic from the J-cost functional and Recognition Composition Law cite this when linking ledger partitions to classical zeta. The structure is assembled directly by packaging the finite-partition definition with the Mathlib Euler-product theorem.
Claim. For $s$ complex with real part greater than 1, the finite prime-ledger partitions converge to the Riemann zeta function as the cutoff tends to infinity. A formal infinite product over prime atoms exists for every complex $s$. Primes are exactly the ledger atoms.
background
The Euler Ledger Partition module treats the Euler product as the partition function of independent prime-ledger postings. PrimeLedgerPartition is the proposition that there exists a map from finite sets of naturals to complexes agreeing with the finite prime-ledger partition on every set. The module isolates the infinite equality inside this certificate because it crosses an analytic import boundary rather than arising from pure RS structure. Upstream results supply the ledger factorization of the multiplicative group, the phi-derived J-cost calibration, and the simplicial continuum bridge that identifies the underlying additive structure.
proof idea
This is a structure definition that directly assembles three fields. The convergence field imports the Mathlib Euler-product theorem for riemannZeta on Re(s) > 1 and substitutes the finite prime-ledger partition. The formal partition field invokes the sibling PrimeLedgerPartition definition. The prime atoms field pulls in the PrimeLedgerCert from the prime ledger atom module. No tactics or reductions are performed.
why it matters
The certificate supplies the Euler partition component required by RSPhysicalThesisData and RSPhysicalThesisDataLogic in the number theory decomposition. It completes the analytic link between the formal prime-ledger partition and classical zeta, consistent with the Recognition Composition Law and the forcing chain that derives D = 3 and the eight-tick octave. It touches the open question of recovering full analytic continuation from ledger axioms without external imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.