empty_ledger_balanced
plain-language theorem explainer
The empty ledger satisfies the balanced predicate by construction. Researchers deriving the ledger forcing principle cite it as the zero-cost base case. The proof is a direct term application of the double_entry field from the empty ledger definition.
Claim. Let $L_0$ be the ledger whose event list is empty. Then $L_0$ is balanced, i.e., balanced_list applied to its events holds.
background
The LedgerForcing module establishes that J-symmetry forces double-entry ledger structure. A Ledger packages a list of RecognitionEvents with an attached double_entry proof. The balanced predicate is defined by applying balanced_list to the events field of the ledger.
proof idea
This is a one-line term proof that applies the double_entry field of the empty_ledger definition. That field is discharged by simp on List.count_nil, confirming the empty list meets the balance condition.
why it matters
The result supplies the base case for the ledger_forcing_principle, which states that the cost landscape forces ledger structure: J-symmetry implies paired reciprocal events, which in turn require double-entry bookkeeping with log-sum cancellation. It closes the existence claim inside the forcing chain from T5 J-uniqueness to conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.