Prove sharp seventeen-step wider-band clocks and generic witness transfer

[Chessing234]

Every ordinary integer Collatz orbit exits [b,21b/4] by time seventeen for b>1. Prove the same clock at ratio 51/10 and certify sharpness for both with the trajectory from 1010 at barrier 379: times zero through sixteen stay in both bands; time seventeen drops to 361. Retain both descent and growth exits.

Add a congruence-aware source generator and a Lean certificate with 123 exact parametric trace lemmas, 76 terminal exclusions, and the final case-split theorem. The guide exhausts its 151-node tree at depth seventeen; no Python computation is trusted as a proof. Generalize finite high-visit witness transfer to any proved rational-threshold exit clock. The new clock yields N distinct visits above 21b/4 before time 18N from lower survival through 18N−1.

Validation: python3 scripts/audit_wider_band_clock.py passes: generator reproducibility, three Lean builds, source proof-escape scans, 214 theorem axiom footprints, and four rejected false claims. Independent tests cover 1,298,909 exhaustive exits, 120,000 large-integer exits, 744 affine prefix samples, 133,637 lower-surviving windows, and 9,026 distinct block witnesses, with sharpness and hypothesis controls. Export the module, add CI coverage, and document proof scope. Previous main CI is green. This does not prove Collatz or establish literature priority; the arithmetic lemmas are certificate components, not separate frontier discoveries.