finiteEulerLedger_cost_formula_J
plain-language theorem explainer
The theorem equates the total recognition cost of a finite Euler ledger, built from a list of primes at positive exponent sigma, to twice the sum of J applied to each p to the power negative sigma. Researchers constructing explicit arithmetic ledgers from prime data would cite this when deriving closed-form expressions for ledger costs. The proof is a one-line wrapper that substitutes the single-event J-cost identity into the general ledger cost formula.
Claim. For real number $σ > 0$ and finite list of primes $support$, the total cost of the ledger constructed by adding prime Euler events equals $2$ times the sum over $p$ in $support$ of $J(p^{-σ})$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost function.
background
The Concrete Euler Ledger module constructs an explicit LedgerForcing.Ledger from finite prime data. For positive real exponent σ, each prime p contributes a recognition event with ratio p^{-σ} together with its reciprocal; the finiteEulerLedger definition builds the ledger by folding add_event over the support list, starting from the empty ledger. Ledger cost is the sum of event costs across the list. Upstream, defect coincides with J for positive arguments, and primeEulerEvent_cost_eq_J states that each prime event costs exactly J of its ratio. The general finiteEulerLedger_cost_formula already expresses total cost as twice the sum of individual event costs.
proof idea
One-line wrapper that applies finiteEulerLedger_cost_formula and rewrites each event cost via the identity primeEulerEvent_cost_eq_J, using simpa to perform the substitution.
why it matters
This supplies the explicit J-based cost formula for the concrete arithmetic ledger, completing the first arithmetic-to-ledger identification step described in the module. It is invoked by the downstream sensorEulerLedger_cost_formula, which indexes the same construction on a DefectSensor via its realPart coordinate. The result realizes positive nontrivial recognition costs and double-entry balance by construction while remaining short of the full RSPhysicalThesis; it directly employs the J functional whose uniqueness is established in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.