ledger_cost
plain-language theorem explainer
The total cost of a ledger is the sum of J-costs over its list of recognition events. Researchers deriving conservation from J-symmetry and double-entry bookkeeping cite this when establishing zero-net-cost balanced structures. It is realized as a direct left-fold accumulation that applies the per-event J-cost to each entry.
Claim. For a ledger $L$ with event list $E$, the total cost equals $J(r_1) + J(r_2) + ...$ where each $r_i$ is the ratio of the $i$-th recognition event and $J$ is the cost function $J(x) = (x + x^{-1})/2 - 1$.
background
A Ledger is a structure whose events field holds a list of RecognitionEvent values together with a balanced_list predicate that enforces double-entry pairing. The per-event cost is defined by applying the J function directly to the event ratio, which inherits reciprocity from the upstream J_symmetric result. The module establishes that J-symmetry forces this paired structure, with the active-edge count A from IntegrationGap supplying the discrete tick background.
proof idea
One-line wrapper that applies List.foldl to accumulate event_cost over the events list, starting from zero.
why it matters
This supplies the cost functional inside the ledger_forcing_principle theorem, which chains J-symmetry to paired events, double-entry, and zero net cost. It is invoked in the explicit summation formulas for finite and sensor-indexed Euler ledgers, closing the step from the Recognition Composition Law to concrete accounting. The definition sits inside the T5-T8 forcing chain that derives D=3 and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.