LiquidationWaterfall
On a breach of the minimum-value rule or a pooling event, proceeds are distributed in a fixed order: holders first up to par value, then any further holder entitlement under the white paper, then general creditors.
The two properties
The first tier is capped at par. Holders receive min(pool, parTotal) —
never more, whatever the pool.
General creditors wait. While the pool does not cover par, the third tier receives nothing.
Both are proved in the formal development and tested unconditionally here: for every pool size tested, the first tier never exceeds par and never exceeds the pool.
Conservation
The three tiers sum to exactly the pool. Nothing is created or lost in the distribution — the contract-level echo of the surplus identity.
Tests
| Test | Discharges |
|---|---|
| holders first, capped at par | frt_distribute_holders_first_par_capped |
| general creditors get nothing while par is short | same theorem, third conjunct |
| the pool is conserved exactly | surplus_identity |
| the cap holds for every pool | unconditional reading |