eulerLedgerPartitionCert
plain-language theorem explainer
The declaration builds the Euler ledger partition certificate that equates finite prime-ledger partitions to the partial Euler products converging to the Riemann zeta function for Re(s) > 1. Researchers embedding number theory into the Recognition Science framework cite it to supply the analytic link between prime postings and zeta without extra hypotheses. The construction invokes Mathlib's riemannZeta_eulerProduct theorem and verifies exact agreement of the finite partitions via unfolding and product congruence.
Claim. The Euler ledger partition certificate consists of three fields: for Re$(s)>1$ the limit of the finite prime-ledger partition over primes below $n$ equals the Riemann zeta function; a formal prime-ledger partition exists for every complex $s$; and primes serve as the ledger atoms via the prime ledger certificate.
background
The module packages the Euler product as the partition function of independent prime-ledger postings. Finite products are proved directly inside the module; the infinite equality with riemannZeta is isolated in the certificate because the Mathlib Euler-product API is treated as an analytic import boundary rather than Recognition Science structure. finitePrimeLedgerPartition computes the product over a finite set S of (1 - p^{-s})^{-1} when p is prime. primeLedgerLocalPartition is the local geometric factor (1 - primePostingWeight s p)^{-1}. primeLedgerPartition_formal asserts that the formal partition exists by taking finite partial products. primeLedgerCert records that primes are exactly the ledger atoms.
proof idea
The definition constructs the structure instance by proving the eulerProduct_eq_zeta field: it calls the upstream Mathlib result riemannZeta_eulerProduct to obtain the limit of partial Euler products, then uses funext, unfold of finitePrimeLedgerPartition and primeLedgerLocalPartition, and Finset.prod_congr to show the finite prime-ledger partitions coincide exactly with those products. The remaining fields are filled by direct reference to primeLedgerPartition_formal and primeLedgerCert.
why it matters
This supplies the eulerPartition field required by rsPhysicalThesisData_of_boundaryTransport and logicData_of_boundaryTransport. It realizes the analytic certificate that connects the formal prime-ledger partition to zeta on the convergence domain Re(s) > 1, as stated in the module documentation. Within the Recognition Science framework it bridges the prime ledger atoms (T5 J-uniqueness and T6 phi fixed point) to the zeta function, supporting the boundary transport step that closes the physical thesis decomposition while leaving BoundaryTransportCert as the remaining obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.