Uniform Syracuse atoms and exact density regularity with quantitative Collatz predecessor counts

We prove a lower bound uniform in depth and residue for the finite Syracuse laws: \(\mu_n(r)\ge c3^{-n}\) for every \(n\ge1\) and every unit residue \(r\). The normalized least atom \(3^nc_n\) decreases to a positive limit \(\ell\), giving \(c_n=\ell3^{-n}(1+o(1))\). The limiting \(3\)-adic law has a Haar density \(f\) with optimal lower bound \(\operatorname{ess\,inf}_H f=2\ell/3\). We prove that \(f\in L^q(H)\) exactly for \(1\le q<2\), although \(f\) is essentially unbounded on every unit cylinder. Let \(N_a(x,\tau)\) count distinct starting integers \(|m|\le x\) that reach \(a\) within \(\tau\) steps of the one-division Collatz map, and put \(\Psi(x)=\sqrt{\log x\,\log\log x}\). For every fixed signed target \(a\) not divisible by three, we prove\[N_a\!\left(x,\frac{2}{\log(4/3)}\log x+D_a\Psi(x)\right)\ge\frac{c_0x}{\exp(C_0\Psi(x))}=x^{1-o(1)}\]for all sufficiently large \(x\). Here \(c_0,C_0>0\) are independent of \(a\), while \(D_a\) and the cutoff may depend on it. A standalone Lean 4 development checks 47 named result and input statements and their transitive axiom dependencies. Versioned proof source: https://github.com/neljaouh/uniform-syracuse-atoms-lean/tree/paper-draft-2026-10-14f