Remark: Verification gap versus mathematical gap

Propositions prop:simultaneous and prop:pacing are not absence-of-machine-checking observations. They identify an incompatible definition and an insufficient estimate. Additional problems with lane separation, charging, and local inner simulation are documented in Appendix app:audit. They do not establish that every alternative transport construction is impossible.