Bound six-band witness sizes and extend ordinary prefix duration

[Chessing234]

The finite-prefix obstruction previously gave existence at each horizon but discarded ordinary steps hidden by acceleration and used a loose growth bound. Lean now proves that for every K and N, an integer n>N with n>1 and n≤2^K·N+10·8^K stays in [n,6n] through K+ceil(3K/5) ordinary steps.

The proof strengthens accelerated growth from factor four to factor two, transfers coverage through the full duration K+oddCount, and applies the existing heavy-coefficient parity-count bound. It also excludes clocks of that duration on the explicitly bounded source domain whenever B≥10·8^K. Existing shorter-duration statements remain available.

Validation: Lean build and audit passed; 30 theorem axiom footprints checked; 133 residues through horizon 2048 and 2,133 scaled witnesses tested, covering 234,532 ordinary states; five false claims rejected. Mathematical priority and optimality are unverified; witnesses depend on the horizon and do not assert an infinite trapped orbit.