DirectedEulerLedgerSystem
plain-language theorem explainer
DirectedEulerLedgerSystem equips any DefectSensor with a directed family of finite Euler ledgers indexed by finite prime sets. Number theorists assembling the arithmetic interface for the Recognition Science Euler trace cite it to enforce stage coherence under support enlargement. The declaration is a structure definition whose fields directly encode the stage map, balance and net-flow zero conditions, prime-pair inclusion with monotonicity, directedness of the index poset, and the explicit J-cost summation formula.
Claim. Let $S$ be a DefectSensor with positive real part $s$. A directed Euler ledger system for $S$ consists of a map assigning to each finite set of primes $P$ a ledger $L_P$ such that each $L_P$ is balanced with zero net flow for every agent; for every prime $p$ in $P$ the Euler event at $p^{-s}$ and its reciprocal both belong to the events of $L_P$; the assignment is monotone under inclusion of prime sets; the collection of finite prime sets is directed under inclusion; and the cost of $L_P$ equals twice the sum of $J(p^{-s})$ over primes in $P$.
background
PrimeSupport is the type of finite subsets of the primes, forming a directed poset under inclusion whose upper bounds are given by unions. The module packages concrete finite Euler ledgers from ConcreteEulerLedger into this directed system for each sensor, supplying the admissible Euler trace and T1-bounded realizability proxy. Upstream, the reciprocal automorphism from CostAlgebra pairs each Euler event with its inverse, while LedgerForcing supplies the balanced predicate and net_flow function that enforce zero net flow at every stage.
proof idea
This declaration is a structure definition. Its fields are stated directly as the required properties of the stage map, balance conditions, prime-pair inclusion, monotonicity, directedness, and cost formula, with no lemmas or tactics applied inside the declaration itself.
why it matters
The structure supplies the directed finite-stage package that feeds the concreteDirectedEulerLedgerSystem definition and the EulerLedgerOntologyInterface. It fills the directed-system step in the Euler ledger construction described in the module documentation. The remaining gap to RSPhysicalThesis is the global physical-identification step that would transport the concrete directed ledger into the eulerLedgerScalarState predicate rather than the bounded proxy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.