finiteEulerLedger_cost_formula
plain-language theorem explainer
The finite Euler ledger cost formula states that for positive real σ and any finite prime list support, the total ledger cost equals twice the sum of the individual prime Euler event costs. Researchers bridging arithmetic structures to Recognition Science ledgers cite this when evaluating explicit costs in prime-supported models. The proof proceeds by induction on the support list, invoking the empty-ledger zero-cost property in the base case and the add-event formula plus algebraic simplification in the inductive step.
Claim. For any real number $σ > 0$ and any finite list $S$ of primes, the total cost of the ledger constructed from the Euler events at those primes equals twice the sum of the costs of the individual events, where each event cost is the $J$-value of the corresponding ratio $p^{-σ}$.
background
In the Concrete Euler Ledger module a finite Euler ledger for positive real exponent σ is built by associating to each prime p the recognition event whose ratio is p^{-σ} together with its reciprocal. The ledger_cost function sums the event_cost values over the event list, and event_cost itself is defined as J applied to the event ratio. The empty ledger has zero cost by the empty_ledger_cost theorem, while adding an event augments the total by the corresponding event_cost via the add_event_cost_formula lemma.
proof idea
The proof is by induction on the support list. The empty-list case unfolds the ledger definition and applies the empty_ledger_cost lemma. The cons case rewrites the ledger definition, invokes add_event_cost_formula together with the inductive hypothesis on the tail, then finishes with simp and ring.
why it matters
This result supplies the explicit total-cost formula that the immediate successor theorem finiteEulerLedger_cost_formula_J rewrites directly in terms of J(p^{-σ}). It completes the first arithmetic-to-ledger identification step described in the module documentation, furnishing a balanced ledger with positive nontrivial recognition cost for each prime event inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.