expense-approval: two signatures, one person

[sajonaro]

Stacked on #4 (base entitlement-problems). Retarget to main once #4 merges.

Adds expense-approval/: one large expense moving through submit, manager approval, finance approval and payment, with reject/resubmit, cancel, and a bank-account change that throws away both signatures. Amounts are bands (small/large), because the rules only ask which side of the threshold an amount is on.

• The safe process pays a large expense on two different signatories. Everything holds, exit 0.
• The shortcut pays when both slots are filled. Bob is Ann's manager and finance's deputy, so submit → bob-approves-as-manager → bob-approves-for-finance → pay gets the expense paid on one person's say-so. derive paid-by lists 13 bob bob.
• compare: never-on-one-person LOST, while the law it breaks (two-for-large) reads preserved, because laws compare by declaration. The README says so.
• A process question the model raised: in the safe process, an expense Bob has signed twice can only be undone by rejecting it, cancelling it, or changing its bank account.

Differences from the plan: with reject, cancel and bank change in the model, the plan's paradox ("the shortcut is the one that terminates") does not occur. Both processes settle. In .rules, independence is a join, because a rules guard cannot compare a path with a path (the claims language can). That is a small asymmetry between the two engines.

Cross-check: 41 → 45 properties (43 compared; settles is the second fair property skipped). ./run-tests.sh all: 270 checks, 0 failed.

🤖 Generated with Claude Code

[sajonaro]

Superseded: reached main through #10.