The ν₂ Countdown Theorem: A Formally Verified Bound on Consecutive Single-Halving Steps in the Collatz Sequence

We prove and formally verify in Lean 4 + Mathlib that the maximum number of consecutive single-halving compound Collatz steps from any odd n ≡ 3 (mod 4) is exactly ν₂(n+1) − 1, where ν₂ denotes the 2-adic valuation. This bound is sharp. The ν₂ Countdown Theorem: If n ≡ 3 (mod 4), then ν₂((3n+1)/2 + 1) = ν₂(n+1) − 1. This creates an exact discrete clock: the 2-adic valuation of n+1 decrements by 1 with each single-halving step, and when it reaches 1, a multi-halving step is forced. Corollaries: (1) Single-halving runs are O(log n). (2) No Collatz orbit can cycle within {n : n ≡ 3 mod 4}. The Alternating LSB Theorem is also proved: (3n+1)/2^j mod 3 strictly alternates 2,1,2,1,... as j increases. Formalization: 11 theorems, 0 sorry statements. Files: CollatzNu2.lean (URB #537 + URB #538) and Collatz.lean. Verified in Lean 4 with Mathlib. Apache 2.0. Part of the Tralse Informationalism (TI Sigma) Research Program, established April 1, 2026.