pith. sign in
module module high

IndisputableMonolith.NumberTheory.DirectedEulerLedger

show as:
view Lean formalization →

Finite prime supports index concrete Euler-ledger stages in the Recognition number theory layer. The module builds directed Euler ledger systems by extending the arithmetic identification of Euler terms p^{-σ} from ConcreteEulerLedger. Researchers on the unified RH realizability architecture cite it to prepare the concrete directed structures for the physicalization bridge. The module is entirely definitional and supplies no new theorems.

claimA directed Euler ledger system for finite prime support $P$ and real part $σ$ is the LedgerForcing.Ledger whose recognition-event ratios are the Euler terms $p^{-σ}$ ($p∈P$) together with their reciprocals.

background

The module imports ConcreteEulerLedger, which builds an actual LedgerForcing.Ledger whose events are the Euler terms $p^{-σ}$ for any positive real $σ$ and any finite prime support, and UnifiedRH, which supplies the three-component T1-bounded realizability architecture that replaced earlier ontological prime ledger attempts. It introduces PrimeSupport as finite sets of primes and DirectedEulerLedgerSystem as the directed extension of the concrete ledger construction. The local setting is the arithmetic-to-ledger identification step that precedes proxy physicalization.

proof idea

This is a definition module, no proofs. It defines PrimeSupport, constructs primeSupport_directed and concreteDirectedEulerLedgerSystem by applying the concrete ledger construction to directed subsets, and records basic containment lemmas such as concreteDirectedEulerLedgerSystem_union_contains.

why it matters in Recognition Science

The module supplies the concrete directed Euler-ledger system that ProxyPhysicalizationBridge consumes to isolate the remaining gap to admissibility and realizability. It advances the arithmetic-to-ledger identification inside the UnifiedRH T1-bounded architecture, linking finite prime supports to the structured realizability components that replaced the earlier OntologicalPrimeLedger.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)