C-D23-REFINEMENT

Branch B refinement cuts 14/28/42 PROVED-INTERNAL: by O-A a counterexample is improper on every refinement grid, so a state proper at level 14, 28 or 42 is soundly cut without integer reconstruction. The cheap mechanism: t=1/14 is a lonely time iff 14 divides no speed, carried as a small-modulus residue mod (14,28,42)

Proved (internal)Evidence I2Scope: Branch B, early impropriety on refinement grids 14/28/42Since gate-d23

In plain language

A state can be thrown out simply because it already has a lonely runner on the finer level-14 grid, no reconstruction needed.

Exact statement

Branch B refinement cuts 14/28/42 PROVED-INTERNAL: by O-A a counterexample is improper on every refinement grid, so a state proper at level 14, 28 or 42 is soundly cut without integer reconstruction. The cheap mechanism: t=1/14 is a lonely time iff 14 divides no speed, carried as a small-modulus residue mod (14,28,42)

All claimsSee in map