primeLedgerPartition_formal
The declaration proves that for any complex s the formal Euler ledger partition exists as an infinite product over prime atoms. Researchers separating the combinatorial structure of the Euler product from its analytic continuation would cite this result. The proof exhibits the finite prime-ledger partition function as the witness and confirms the defining equality by reflexivity.
claimFor every complex number $s$, there exists a function $F$ from finite subsets of the positive integers to the complex numbers such that $F(S)$ equals the finite prime-ledger partition of $s$ over $S$ for every finite set $S$.
background
The 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. PrimeLedgerPartition (s) is the proposition asserting existence of a map F from Finset ℕ to ℂ such that F(S) equals finitePrimeLedgerPartition s S for all S. finitePrimeLedgerPartition itself is the product over p in S of (if p is prime then primeLedgerLocalPartition s p else 1). This rests on the arithmetic zeta function and the ILG action S[g, ψ; C_lag, α].
proof idea
The proof is a term-mode construction that directly supplies the finitePrimeLedgerPartition function as the witness for the existential quantifier in PrimeLedgerPartition. The universal quantification over finite sets S is discharged by reflexivity, since the defining equality holds by construction of the finite product.
why it matters in Recognition Science
This theorem supplies the formal existence statement required by the downstream eulerLedgerPartitionCert, which then invokes Mathlib's Euler-product theorem to equate the partition with riemannZeta on Re(s) > 1. It completes the separation of the finite combinatorial structure from the analytic certificate in the Euler ledger partition module. In the Recognition Science framework this corresponds to the number-theoretic foundation underlying the constants and mass formulas derived from the phi-ladder.
scope and limits
- Does not prove convergence of the infinite product for any s.
- Does not identify the partition function with the Riemann zeta function.
- Does not address the behavior at the poles or zeros of the zeta function.
- Does not incorporate the J-cost or defectDist from the forcing chain.
formal statement (Lean)
56theorem primeLedgerPartition_formal (s : ℂ) : PrimeLedgerPartition s :=
proof body
Term-mode proof.
57 ⟨fun S => finitePrimeLedgerPartition s S, fun _ => rfl⟩
58
59/-- Analytic certificate connecting the formal prime-ledger partition to zeta
60on a convergence domain. -/