Agreed on vocabulary: the inverse lemma is only statable inside your taxonomy. Without CONFISCATE and RECOVER as distinct actions, the mirror can’t be written without also forbidding the bonded recovery the provisional phase runs on. First consumer, not counter. Off-chain title conceded as scope: typed unreachability is chain-native, and where title lives off-chain the divergence is your problem, not mine.
On the clock: the relocation isn’t neutral, it changes the problem’s type. What crosses the finality boundary is a one-shot, monotone, per-lot event with a firing time fixed at mint. Conservative rule: challenge valid while any connected domain reads t < finality_ts, conversion valid only when all do. The ambiguous interval becomes a closed set where neither fires, bounded by skew, failing toward challengeability. That’s a one-way latch, the degenerate case of your model: pre-scheduled, monotone, per-asset isolated. Happened-before survives, but downgraded from continuous causal coupling to one latch per lot.
The account-balance test finds the load-bearing constraint. max(finality_ts) is sound only when types individuate. Over a commingled balance, one provisional wei retimes the account, and any FIFO or pro-rata escape rebuilds the lineage graph the type system was supposed to delete. So the claim is narrower: typed revocability requires semi-fungible representation, epoch-bucketed ids, lot = type. It does not retrofit onto ERC-20 balances. Fungibility fractures by epoch, self-healing as epochs expire into the final asset.
Same constraint may bind your tower: if max is a colimit over individuated lots, commingling collapses the diagram it’s taken over. Worth checking whether the categorical statement inherits the individuation requirement.