Prove a universal ratio-six band-clock obstruction

[Chessing234]

For every finite horizon K and size threshold N, Lean now proves the existence of an integer n>N with n>1 whose ordinary Collatz prefix stays in [n,6n] through time K. This rules out uniform finite band-exit clocks at every rational ratio at least six, complementing the existing sharp seventeen-step clock at ratio 21/4.

The proof constructs balanced parity residues, controls exact affine accelerated traces, and bounds the intermediate ordinary odd peaks. Each horizon has an entire sufficiently large arithmetic progression of witnesses. Witnesses may change with the horizon; this does not assert an infinite trapped orbit or settle Collatz. Mathematical priority remains unverified.

Validation: targeted Lean build passed; 22 theorem axiom footprints checked; independent Python tests checked 133 residues through horizon 2048, 2,133 scaled witnesses, and 143,992 ordinary states; four false claims were rejected. The audit is included in CI.