The theorem

Both orders fail.

Two clearances are individually safe and jointly unsafe. You cannot fix that by doing one and then the other, because by the time the first has committed the second aircraft's window has shut.

Validate-at-commit does not fail because it cannot see. It fails because by the time it has committed and looked, the other aircraft's window is shut.

The windows are physics, the band is latency

Each aircraft has a window: the span during which a clearance can still be issued early enough for the manoeuvre to finish before its gate. That comes from the aircraft, not from us.

aircraft	gate	manoeuvre	window
AAL221 → BAYLR	14.40 NM	150.00 s	44 360 ms
SWA455 → CARDL	7.10 NM	45.56 s	43 684 ms

The admissible band — (34 580, 53 132) ms — comes from measured decision latency and contains no geometry at all. The gate distances are calibrated to land inside it; the band itself is not a free parameter, and a test recomputes it from the latency model rather than asserting it.

Where a serialized system arrives

Both windows have already closed by the time a serialized system reaches its second decision. The concurrent commit, even at its slowest, is still inside both.

A serialized system cannot reach its second decision before 53 132 ms — one turn, plus 8.0 s of single-channel readback, plus another turn. By then:

A then B — B is excluded, window closed, missed by 9 446 ms
B then A — A is excluded, window closed, missed by 8 770 ms

Both orders fail. If only one did, the hazard would be serializable and the theorem would be false. That is what makes it falsifiable rather than rhetorical.

Subtracting the windows from 53 132 gives 9 448 and 8 772 — two milliseconds more than the figures above. Commit times quantise to the 10 ms master tick, so the commit lands on tick 5313, at 53 130 ms, and the misses are measured from there. The numbers are computed, not narrated.

And the hazard does not wait

Commit both clearances later than 53.9 s and the aircraft pass legally — there is nothing left to catch. So the hazard has to outlast the slowest decision the architecture can make, and it does, by 19.3 s. It is also still alive at the serialized instant, which matters: the serialized arm does not get away with it because the danger passed. It fails on the window alone.

It ships as a test

npm run verify:theorem   # 0.7 s, zero tokens, no API key

Two named assertions, both required. The hazard is visible to anything holding both clearances as pending intent — which is exactly what the airlock does and exactly what validate-at-commit does not — and both serialization orders miss their window.

Watch it run