C-D25-ADAPTIVE

D25 rational-time cut PROVED-INTERNAL: for a reduced time a/q, B(a,q) = { r mod q : min(a r mod q, q - a r mod q) < q/14 } (strict; the boundary is a lonely, not a bad, residue; integer-exact after clearing 14). A global counterexample is improper, so for every a/q it satisfies OR_i [ V_i mod q in B(a,q) ] (else t=a/q is lonely); the contrapositive cuts any branch lonely at that time. Each cut is a disjunction over ONE small modulus, so moduli stay separate and no giant LCM is materialized. B(1,14)={0} reproduces the D24 t=1/14 cut and the p=197 witness fires

In plain language

A proved rule: for any rational time, a counterexample must have a runner near the origin, giving an exact clause on the speeds modulo just that time's denominator, no giant shared clock needed.

Exact statement

D25 rational-time cut PROVED-INTERNAL: for a reduced time a/q, B(a,q) = { r mod q : min(a r mod q, q - a r mod q) < q/14 } (strict; the boundary is a lonely, not a bad, residue; integer-exact after clearing 14). A global counterexample is improper, so for every a/q it satisfies OR_i [ V_i mod q in B(a,q) ] (else t=a/q is lonely); the contrapositive cuts any branch lonely at that time. Each cut is a disjunction over ONE small modulus, so moduli stay separate and no giant LCM is materialized. B(1,14)={0} reproduces the D24 t=1/14 cut and the p=197 witness fires