Prove a sharp thirty-step clock plateau with infinitely many witnesses

[Chessing234]

Lean now proves that every ordinary Collatz orbit exits [b,11b/2] by time thirty for every integer b>1. The duration is sharp throughout the rational-width interval [382948/71803,11/2], including [16/3,11/2].

An infinite family n=262144q+201714, b=93312q+71803 has its prefix minimum at time seventeen and maximum at time twelve, with 3·max+4=16·b. Every member first exits at time thirty: even parameters exit downward and odd parameters exit upward. These are finite-prefix statements and conditional high-visit consequences, not universal descent or a Collatz solution. Mathematical priority remains unverified.

The reproducible certificate uses 469 tree nodes and 235 terminal branches. It is split into dependency modules, with a generic affine lifting lemma and arithmetic-context pruning to control Lean memory use. Generated branch clauses are proof bookkeeping, not independent discoveries. The generator still reproduces the older ratio-21/4 certificate by default.

Validation: Lean builds passed; 640 axiom footprints checked and six false claims rejected; independent tests checked 690,242 exhaustive exits, 60,000 large-integer exits, 2,274 affine prefixes, 99,313 windows, 4,438 distinct witnesses, and 1,004 family members. The previous seventeen-step audit also passed (215 footprints, four false claims rejected). Exploratory wider-clock candidates are explicitly marked as not yet formalized.