pith. sign in
module module high

IndisputableMonolith.NumberTheory.EulerLedgerPartition

show as:
view Lean formalization →

This module defines the Euler ledger partition by weighting prime postings at complex scale s. It extends the prime ledger atoms into the structure required for the Euler product representation of zeta. The module contains only definitions and partition constructions with no internal proofs. Researchers on the RS-native Riemann hypothesis proof cite it as the formal bridge from arithmetic ledger to analytic product.

claimThe Euler ledger partition weights each prime posting $p$ by the factor $p^{-s}$ at complex scale $s$, yielding the local factors that assemble into the Euler product over primes.

background

The upstream PrimeLedgerAtom module establishes that primes are the irreducible postings of the multiplicative positive-integer ledger; the RS work begins once those postings receive weights. This module introduces the weighting at complex $s$ to produce the Euler ledger partition, with sibling definitions such as primePostingWeight, primeLedgerLocalPartition, and EulerLedgerPartitionCert. The setting is the classical arithmetic ledger before any analytic continuation or RS-physical decomposition is applied.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds EulerProductEqualsZeta, which wires the partition to Mathlib's theorem that the Euler product equals the Riemann zeta function on Re(s) > 1, and RSPhysicalThesisDecomposition, which replaces the opaque RSPhysicalThesis with the exact ingredients needed for the RH proof. It supplies the prime-ledger partition step in Phase 1 of the RS-native zeta program.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)