pith. sign in
module module high

IndisputableMonolith.NumberTheory.DirectedEulerLedger

show as:
view Lean formalization →

This module assembles definitions that index concrete Euler-ledger stages by finite prime supports, extending the arithmetic-to-ledger map from ConcreteEulerLedger into the directed setting required by UnifiedRH. Researchers formalizing the T1-bounded realizability architecture would cite it when bridging arithmetic ledgers to the proxy physicalization step. The module consists of type definitions, concrete instances, and interface lemmas with no internal proofs.

claimA directed Euler ledger system is a structure that, for each finite prime support $S$ and sensor real part $σ$, produces a balanced ledger whose recognition-event ratios are the Euler factors $p^{-σ}$ ($p∈S$) together with their reciprocals.

background

The module imports ConcreteEulerLedger, which builds an actual LedgerForcing.Ledger whose recognition-event ratios are the Euler terms $p^{-σ}$ together with their reciprocals for any positive real exponent $σ$ and finite prime support. It also imports UnifiedRH, whose three-component T1-bounded realizability architecture replaces the earlier ontological prime ledger that asserted bounded total annular cost. The local setting is therefore the arithmetic-to-ledger identification step inside the NumberTheory domain, with the main objects being the directed system and its concrete and ontology-interface instances.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete directed Euler-ledger system that ProxyPhysicalizationBridge uses to isolate the exact remaining gap after connecting the ledger to the already-proved admissibility and realizability infrastructure. It therefore fills the finite-prime-support indexing step inside the T1-bounded architecture of UnifiedRH.

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)