finiteEulerLedger
plain-language theorem explainer
The finite Euler ledger construction maps a positive real exponent σ and any finite list of primes to a concrete LedgerForcing.Ledger whose events consist of the factors p^{-σ} together with their reciprocals. Researchers establishing the arithmetic-to-ledger bridge in Recognition Science cite this definition when proving balance, zero net flow, and explicit cost formulas for prime-based ledgers. The definition is given by recursion on the input list, delegating the base case to the empty ledger and each inductive step to the add_event operator
Claim. For positive real σ and finite list of primes, the associated ledger is obtained recursively from the empty ledger by adjoining, for each prime p, the recognition event of ratio p^{-σ} together with its reciprocal.
background
The Concrete Euler Ledger module supplies the first explicit arithmetic-to-ledger identification. A LedgerForcing.Ledger is a list of recognition events equipped with a double-entry balance predicate. The upstream add_event operation appends a given event and its reciprocal while preserving the balance condition by construction; empty_ledger supplies the initial object with no events. The sibling primeEulerEvent produces the concrete recognition event carrying ratio p^{-σ} for each prime p.
proof idea
The definition proceeds by recursion on the list of primes. The empty list case returns LedgerForcing.empty_ledger. The cons case p :: ps returns LedgerForcing.add_event applied to the recursive call on ps and the event produced by primeEulerEvent σ hσ p.
why it matters
This definition realizes the concrete bridge object described in the module documentation and directly feeds the downstream results finiteEulerLedger_balanced, finiteEulerLedger_cost_formula, finiteEulerLedger_net_flow_zero, and the membership lemmas for prime and reciprocal events. It supplies the arithmetic ledger required before any proof of RSPhysicalThesis can be attempted and connects Euler-product structure to the balanced-ledger conservation laws appearing in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.