Length of Collatz descent certificates after an ascent of length K: a proved lower bound and a limit law

For finite descent certificates of the Collatz map, we prove that an initial ascent of K steps forces every certificate to have length k ≥ K; hence no finite certificate archive can close the descent. Both results are formally verified in Lean 4 (core, no sorry). Exact computations give k ≈ 2.41K ± 4.05√K, matching the exact 2-adic law of the slope stopping time and a random-walk first-passage model; the tail decays like t^{-3/2}e^{-0.055t}. No upper bound on k is proved; the note does not claim a proof of the Collatz conjecture.