net_zero
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.