Hausdorff dimension of the 2-adic set of Collatz points with infinite coefficient stopping time

We prove that the set of 2-adic integers whose Collatz coefficient 3^{a_j}/2^j never drops below 1 has Hausdorff and box dimension exactly H₂(log₃2) ≈ 0.949955, where H₂ is the binary entropy. This sharpens Lagarias’s exponential bound (1985, Thm. D) into an exact dimension statement, and we prove the identity 1 − I/ln 3 = H₂(log₃2) with the Cramér rate I of the accelerated walk. Arithmetic and combinatorial parts (Terras isometry, counting N_k = OEIS A076227) are formally verified in Lean 4 (core, no sorry). The result does not prove the Collatz conjecture; it shows that the exceptional set, of measure zero, has almost full dimension.