ledger_cost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not verify the balanced_list constraint on the input ledger.
- Does not incorporate the active-edge count A or integration-gap corrections.
- Does not extend the summation to infinite or continuous event collections.
- Does not encode reciprocity beyond the single-event level already present in event_cost.
Lean usage
theorem empty_ledger_cost : ledger_cost empty_ledger = 0 := by simp [ledger_cost, empty_ledger]formal statement (Lean)
89noncomputable def ledger_cost (L : Ledger) : ℝ :=
proof body
Definition body.
90 L.events.foldl (fun acc e => acc + event_cost e) 0
91
92/-- A ledger is balanced if its event list is balanced. -/