Conservation: the fourth law

The claim

The registry states three laws: every construct maps to a registry entry, verbs are unit-agnostic, nothing crashes. A fourth is already being enforced in four places and stated in none:

Nothing is created or destroyed. Every effect on a quantity names a source and a destination, and the receipt carries both legs.

That sentence is what makes the language ledgable. A receipt chain carrying both legs of every movement folds into a journal, and an auditor can reconcile a contract without bespoke tooling.

It is already here, four times, unnamed

Where	What it says	Scope
Linear values	a moved value cannot be copied or spent twice; tokens are move semantics	per value
Amendments	the linter checks that a transform cannot mint or vanish value - total capacity and total consumed preserved across a version boundary	per amendment
Splits	parts sum exactly to the whole, with one declared remainder-taker	per split
Computed flows	every computed flow is provably no greater than its source stage, on every branch	per rule

Four statements of one law, each scoped to one mechanism, none general. So the obvious gaps stay invisible: the commit-reservations verb does not name a destination, a register write can record an amount with no source at all, and an emitted payment instruction moves value out of the system entirely.

The boundary problem, and double-entry’s answer

If value leaves through an out-port, what conserves? Double-entry settled this in 1494: nothing leaves a closed system, because the system includes an account for the counterparty. The mechanical equivalent:

• Every party, executor and host has an implicit boundary account.
• Issuing a payment instruction for an amount to a supplier is a movement from a declared pool stage into that supplier’s boundary account - not a disappearance.
• The fold’s trial balance is therefore always zero across pool stages plus boundary accounts, for every contract, after every event.

That is the whole mechanism. It costs one implicit account per participant, and it converts “did every krona come from somewhere and go somewhere” from an audit question into an invariant the evaluator asserts.

# what a receipt carries per quantity effect - both legs, always
effect: move  120_000 SEK
  from: pool money.settlement @ reserved
  to:   party:seller (boundary)
  # trial balance after: 0   (asserted by the evaluator, not hoped for)

What the law does not cover

Precision matters more than volume here:

• Quantities only. Moving title in a property transfers a unique thing, not an amount; that is governed by linearity (exactly one owner) rather than conservation (sums balance). The law applies to money, dimensioned quantities and counters - the types with arithmetic.
• Facts are not quantities. A host function returning a tax rate creates a fact, not value. The standard already draws this line: external functions return facts, internal expressions move money. Conservation governs the movement the contract then performs, never the fact it consulted.
• Unbounded pools sit outside it, visibly. A draw from an unlimited pool mints by construction. That is fine for “unlimited support tickets” and fatal for money, so the rule is: an unbounded pool may not hold a money type, and any contract declaring one says so on its manifest.
• Rounding is where conservation is actually fought. Any division of money must be a conserving split with a declared remainder-taker; a bare division on money feeding a flow is the bug this law exists to catch.

What it buys

1. A journal for free. Fold the receipts and get debits and credits with clause citations. The audit trail stops being “a chain of judgments” and becomes a book of account that an auditor already knows how to read.
2. The encumbrance picture becomes a balance sheet. The available / reserved / disbursed stages are accounts; committed-but-unpaid is a real number, per contract and in aggregate.
3. A cheap, strong linter check. Conservation is provable by place invariants - a weighted sum every transition preserves - which is linear algebra over the effect matrix rather than a search through reachable states. This is the practical answer to the worry that pool safety is expensive in theory (RFC 0009): you do not explore the state space, you prove a sum is constant.
4. Fraud detection without heuristics. “Every krona recomputable from the contract and the log” becomes checkable rather than aspirational.

Honest creaks

1. Implicit accounts are still new state. They are derived - a view over the log - so they add no storage, but a reader must now understand that the state block is not the whole ledger. The manifest should render boundary accounts explicitly rather than leaving them implied.
2. The commit verb has no destination today. Under this law it must name one - the same conclusion the naming work reached from the other side (RFC 0007): staged movements should be spelled as movements. The two decisions belong together.
3. Multi-currency conservation needs the conversion fixing. Balancing across currencies is only meaningful at a declared rate, so a trial balance is per currency, never one number.
4. Compensation is not reversal. A compensating step moves value back; it does not delete the original legs. The journal shows both, which is correct accounting practice - reversal entries, never erasures - and worth saying out loud so nobody expects a net-zero-looking log.

Prior art

Double-entry bookkeeping (1494) - the original conservation law for value, and the reason this vocabulary already exists in every finance department. Linear logic and linear types - the formal reason a value cannot be duplicated or dropped. Petri-net place invariants - the proof technique: a weighted token sum every transition preserves; sixty years old, and exactly the pass this law needs. Conserving money allocation with a declared remainder-taker - the standard fix for rounding. Plain-text accounting tools with balance assertions, and databases whose primitive is a two-sided transfer that must balance - the modern engineering statement that both legs belong in the primitive rather than in a convention. Encumbrance accounting - the public-sector stage vocabulary the pools already borrow.

This RFC is exploratory. It is published as a basis for discussion, not as normative text; where it touches the standard, the standard governs until a decision is recorded.