eulerLedgerPartitionCert
The definition constructs the Euler ledger partition certificate equating the limit of finite prime-ledger partitions to the Riemann zeta function for Re(s) > 1. Researchers building the Recognition Science physical thesis decomposition cite it to link the prime ledger to analytic zeta. The construction invokes Mathlib's riemannZeta_eulerProduct theorem and verifies equality of the ledger partitions with Euler products via extensionality and product congruence on prime sets.
claimThe Euler ledger partition certificate is the structure whose first field states that the limit as $N$ tends to infinity of the product over primes $p < N$ of $(1 - p^{-s})^{-1}$ equals the Riemann zeta function whenever the real part of $s$ exceeds 1, whose second field asserts existence of a formal prime-ledger partition at every complex scale $s$, and whose third field identifies primes with the ledger atoms.
background
This module packages the Euler product as the partition function of independent prime-ledger postings. The finite prime-ledger partition over a finite set $S$ is defined as the product over primes $p$ in $S$ of $(1 - p^{-s})^{-1}$, where the local factor at each prime is the reciprocal of one minus the prime posting weight $p^{-s}$. The infinite equality with zeta is isolated in this certificate because the Mathlib Euler-product API forms an analytic import boundary rather than Recognition Science structure.
proof idea
The definition fills the equality field by applying the Mathlib theorem riemannZeta_eulerProduct to obtain the tendsto statement for the Euler products. It then uses function extensionality together with Finset.prod_congr after unfolding the finite partition, local partition, and posting weight definitions to show the ledger partitions coincide with those products. The remaining fields are supplied directly by the formal partition theorem and the prime ledger certificate.
why it matters in Recognition Science
This certificate supplies the analytic link between the formal prime-ledger partition and the zeta function required by the logic data of boundary transport and the RS physical thesis data of boundary transport. It completes the Euler product side of the ledger decomposition in the Recognition Science framework, leaving only the boundary transport certificate as the remaining obstruction.
scope and limits
- Does not establish convergence of the Euler product for Re(s) ≤ 1.
- Does not address the Riemann hypothesis or any of its equivalents.
- Does not compute explicit values, residues, or zeros of the zeta function.
- Does not incorporate non-prime ledger states into the partition.
Lean usage
eulerPartition := eulerLedgerPartitionCertformal statement (Lean)
76def eulerLedgerPartitionCert : EulerLedgerPartitionCert where
77 eulerProduct_eq_zeta := by
proof body
Definition body.
78 intro s hs
79 have hmathlib :
80 Filter.Tendsto (fun n : ℕ ↦ ∏ p ∈ Nat.primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹)
81 Filter.atTop (𝓝 (riemannZeta s)) :=
82 _root_.riemannZeta_eulerProduct hs
83 have hpart : (fun n : ℕ ↦ finitePrimeLedgerPartition s (Nat.primesBelow n)) =
84 (fun n : ℕ ↦ ∏ p ∈ Nat.primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹) := by
85 funext n
86 unfold finitePrimeLedgerPartition primeLedgerLocalPartition primePostingWeight
87 apply Finset.prod_congr rfl
88 intro p hp
89 have hprime : Nat.Prime p := (Nat.mem_primesBelow.mp hp).2
90 simp [hprime]
91 simpa [hpart] using hmathlib
92 formal_partition := primeLedgerPartition_formal
93 prime_atoms := primeLedgerCert
94
95end
96
97end NumberTheory
98end IndisputableMonolith