Type the coordination bus as a choreography #363

The bus (peer registration, mutex task claims, gated envelopes, quarantine
review) is a multiparty protocol. choreographic-types (PR #23) now proves
K-CUT for the finite synchronous fragment: each agent's local protocol is
the projection, with a certified grade; occupancy-types (PR #9) bounds
envelopes in flight by the high-water-mark algebra. Ask: write the bus as a
Global, project per role, record the grades; the asynchrony extension
(pre-registered) is what the bus actually needs, so this repo is its first
customer and its falsifier (sender-knows must fail with queues).

Filed from the 2026-10-12 family session; see nextgen-typing docs/TYPE-CONNECTIONS.adoc for the connection statuses.