Prove sharp twelve-step band exits and conditional high-visit frequency

[Chessing234]

Every ordinary Collatz orbit exits the inclusive band [b,5b] within twelve steps when b>1. Prove the universal clock and certify sharpness with b=40, n=114, whose first exit occurs at time twelve. The arithmetic certificate also works for the relaxed halving/3x+1 relation without parity guards: an exact-rational generator selects fifty terminal prefixes and Lean proves each independently.

For an orbit retaining the fixed lower barrier, prove a high visit above 5b in every thirteen-point window and distinct witnesses in disjoint blocks. The finite witness theorem needs only lower survival through time 13N−1. Keep the downward/growth alternatives and all kernel assumptions explicit; this does not prove Collatz, unboundedness, or literature novelty.

Validation: python3 scripts/audit_five_band_clock.py passes (61 theorem axiom footprints; four false claims rejected). Independent tests cover 627,742 exhaustive and 60,000 large-integer ordinary starts, 20,295 relaxed-transition starts, 150,670 lower-surviving windows, and 13,565 distinct block witnesses. Generator reproducibility, sharpness and hypothesis controls, the full repository proof-escape scan, and diff whitespace checks pass. Add the audit to CI and export the module from Collatz.lean.