C-D24-REACHABLE

D24 global mod-84 semantics PROVED-INTERNAL: represent reachable states as one common residue multiset modulo 84 = lcm(14,28,42), a single global clock never re-chosen per prime. The frozen exact cut: t=1/14 is a lonely time iff 14 divides no speed, so a bounded counterexample must have at least one V_i divisible by 14 (verified firing on the p=197 witness); the analogous test-time conditions at levels 28 and 42 are exact, not over-generalized to full level-l impropriety

In plain language

One shared clock modulo 84 with an exact rule: any counterexample must have a runner whose speed is a multiple of 14, or the time 1/14 would be lonely.

Exact statement

D24 global mod-84 semantics PROVED-INTERNAL: represent reachable states as one common residue multiset modulo 84 = lcm(14,28,42), a single global clock never re-chosen per prime. The frozen exact cut: t=1/14 is a lonely time iff 14 divides no speed, so a bounded counterexample must have at least one V_i divisible by 14 (verified firing on the p=197 witness); the analogous test-time conditions at levels 28 and 42 are exact, not over-generalized to full level-l impropriety