IndisputableMonolith.NumberTheory.EulerLedgerPartition
This module supplies the definitions for weighting prime postings at complex scale s in the Recognition Science ledger. It partitions the multiplicative integers into Euler factors ready for the zeta function. The structure includes finite partitions, insertion rules for primes and non-primes, and a certification object. Researchers bridging arithmetic to the Riemann hypothesis in this framework cite it to formalize the prime contributions. The module contains only definitions with no completed proofs.
claimThe Euler ledger partition at scale $s$ decomposes the positive integer ledger into weighted prime postings $p^{-s}$ for each prime $p$, with finite local partitions satisfying the multiplicative composition law.
background
The upstream PrimeLedgerAtom module grounds the arithmetic ledger by identifying primes as the irreducible postings of the multiplicative positive-integer ledger. The RS work begins once these postings receive weights at complex scale s, as stated in the upstream doc-comment: 'This module grounds the arithmetic ledger used by the RH bridge. The content is deliberately classical and small: primes are exactly the irreducible postings of the multiplicative positive-integer ledger. The RS work starts after this point, when the prime postings are weighted into the Euler ledger.'
proof idea
This is a definition module, no proofs. The content organizes the prime ledger into weighted partitions at scale s through successive definitions of local finite partitions and their extensions by prime and non-prime insertions.
why it matters in Recognition Science
The module feeds directly into EulerProductEqualsZeta, which wires the RS prime-ledger partition to Mathlib's theorem equating the Euler product over primes to the Riemann zeta function for Re(s) > 1. It also supplies the arithmetic structure for RSPhysicalThesisDecomposition, replacing an opaque dependency with the exact ingredients for the RH proof. In the Recognition Science framework this completes the step from prime atoms to the complex-weighted Euler ledger required for the zeta program.
scope and limits
- Does not prove any equality between the partition and the zeta function.
- Does not extend the construction beyond the half-plane Re(s) > 1.
- Does not address convergence or analytic properties of the product.
- Does not include the full statement of the Riemann hypothesis.
used by (2)
depends on (1)
declarations in this module (9)
-
def
primePostingWeight -
def
primeLedgerLocalPartition -
def
finitePrimeLedgerPartition -
theorem
finitePrimeLedgerPartition_insert_nonprime -
theorem
finitePrimeLedgerPartition_insert_prime -
def
PrimeLedgerPartition -
theorem
primeLedgerPartition_formal -
structure
EulerLedgerPartitionCert -
def
eulerLedgerPartitionCert