net_zero
Any ledger's net balance is identically zero by its global balance invariant. Researchers establishing conservation in Recognition Science or discrete gauge models cite this when closing accounting structures. The proof is a direct one-line projection from the ledger's built-in global_balance field.
claimFor any ledger $L$, the net balance satisfies $net(L) = 0$.
background
A ledger is a list of transactions equipped with total_debit and total_credit fields whose sum is forced to zero by the global_balance hypothesis. This structure encodes double-entry bookkeeping so that every debit is matched by a credit, making each conservation law an instance of ledger closure. The net function is defined directly as total_debit plus total_credit, and the upstream net definition in the same module supplies the same quantity.
proof idea
One-line wrapper that applies the global_balance field of the Ledger structure.
why it matters in Recognition Science
This supplies the zero-net condition required by ValidTrajectory for 8-tick neutrality. It instantiates the conservation laws of the RRF ledger algebra and aligns with the eight-tick octave (T7) in the forcing chain. The result closes accounting closure for any finite sequence of transactions.
scope and limits
- Does not constrain the values of individual transactions beyond their aggregate sum.
- Does not extend to structures lacking the global_balance invariant.
- Does not address real-valued or continuous balances.
formal statement (Lean)
110theorem net_zero (L : Ledger) : L.net = 0 := L.global_balance
proof body
Term-mode proof.
111
112/-- Concatenate two ledgers. -/