pith. sign in
module module high

IndisputableMonolith.NumberTheory.DirectedEulerLedger

show as:
view Lean formalization →

Finite prime supports index concrete Euler-ledger stages in the number theory layer. Researchers bridging arithmetic Euler products to directed ledgers cite this module when linking to the proxy physicalization step. It is a definition module with no proofs, built from imports of ConcreteEulerLedger and UnifiedRH.

claimFinite prime supports indexing concrete Euler-ledger stages, with main objects $DirectedEulerLedgerSystem$ and $concreteDirectedEulerLedgerSystem$ built from Euler terms $p^{-\sigma}$.

background

The module operates in the arithmetic-to-ledger identification step of Recognition Science. ConcreteEulerLedger builds an actual LedgerForcing.Ledger for any positive real exponent $\sigma$ and finite prime support, with recognition-event ratios given by the Euler terms $p^{-\sigma}$ together with their reciprocals; for a DefectSensor this uses $\sigma = sensor.realPart$ to produce a finite balanced arithmetic ledger.

UnifiedRH supplies the T1-Bounded Realizability Architecture, a structured three-component replacement for the former OntologicalPrimeLedger that avoids direct contradiction with the proved not_realizedDefectAnnularCostBounded. The present module adds the directed variant indexed by finite prime supports.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds ProxyPhysicalizationBridge, which isolates the exact remaining gap after constructing the concrete directed Euler-ledger system and connecting it to the already-proved admissibility and realizability infrastructure. It supplies the finite-prime-support indexing required for the T1-Bounded Realizability Architecture in 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)