empty_ledger
plain-language theorem explainer
The empty ledger is the base Ledger with an empty list of recognition events, satisfying the double-entry constraint vacuously. It anchors inductive ledger constructions in the J-symmetry forcing framework and is cited by results on zero-cost conservation and finite Euler ledgers. The definition is a direct record construction whose balanced_list field is discharged by simplification on the nil list.
Claim. Let $L_0$ be the ledger whose events list is empty and whose double-entry predicate holds for the empty collection of recognition events.
background
The Ledger Forcing module shows that J-symmetry forces double-entry ledger structure. A Ledger consists of a list of RecognitionEvent together with a proof that the list satisfies balanced_list, which encodes the requirement that every event has a reciprocal counterpart preserving total cost. The upstream balanced definition simply lifts this predicate to the Ledger record.
proof idea
Direct record construction: events is set to the empty list and the double_entry field is supplied by a proof term that applies simp using List.count_nil to confirm the balanced_list condition on the nil list.
why it matters
This definition supplies the zero element for the ledger forcing principle, which derives conservation laws from J(x) = J(1/x) via paired events and zero-cost ledgers. It is invoked by empty_ledger_balanced, empty_ledger_cost, empty_ledger_net_flow, the ledger_forcing_principle theorem, and the finiteEulerLedger construction. It anchors the inductive step from the empty collection to ledgers built by adding reciprocal pairs, consistent with the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.