concat_preserves_balance
plain-language theorem explainer
Concatenating two ledgers that each satisfy global balance produces a ledger whose net is zero. Ledger algebraists in the RRF framework cite this when assembling composite conservation laws from smaller balanced components. The proof is a direct term that extracts the global_balance field of the concatenated structure.
Claim. If $L_1$ and $L_2$ are ledgers (sequences of transactions whose total debit plus total credit equals zero), then the net of their concatenation equals zero.
background
The Ledger structure consists of a list of transactions together with computed total debit and total credit, plus the global_balance field asserting their sum is zero. This encodes double-entry bookkeeping so that every conservation law appears as an instance of ledger closure. The module documentation states that each conservation law (energy, charge, momentum) is realized this way.
proof idea
The proof is a one-line term that applies the global_balance field directly to the result of concatenation.
why it matters
This theorem supplies the basic closure property for building larger ledgers in the RRF foundation. It supports the module's claim that conservation laws are ledger instances and aligns with the double-entry constraint described in the module documentation. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.