The approach is CS verification applied to tax design: enumerate every possible state (5 storage types × 5 agent types) and every possible action (7 primitives), then show every cell is priced and no sequence of actions reduces cost. Three instruments are sufficient for closure. Registration of assets is voluntary but strictly dominant — unregistered assets carry no enforceable ownership title, so the only "compliance decision" is dominated.

I'm the author. Curious whether anyone can find flaws.