ledger_balanced
plain-language theorem explainer
Every ledger satisfies the balanced property by construction of its record. Researchers constructing Euler ledgers or verifying zero net flow in recognition accounting cite this result. The proof is a direct field projection from the Ledger structure.
Claim. For every ledger $L$, the predicate balanced$(L)$ holds, where balanced means the list of recognition events satisfies the double-entry constraint.
background
The Ledger Forcing module shows that J-symmetry forces double-entry ledger structure. A Ledger is a structure consisting of a list of RecognitionEvent together with a proof that the list is balanced. The balanced predicate is defined as balanced_list applied to the events of the ledger. Upstream, the net function computes debit minus credit at each state, and the ledger net is required to be zero.
proof idea
This is a one-line wrapper that extracts the double_entry field from the Ledger record.
why it matters
The result is invoked by the finite Euler ledger balanced theorem in NumberTheory.ConcreteEulerLedger. It supplies the double-entry structure required by J-symmetry in the Recognition framework and confirms that ledger net remains zero. It closes one step in the forcing chain from J-uniqueness to concrete ledger constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.