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: \(μ_n(r)≥ c3⁻ⁿ\) for every \(n≥1\) and every unit residue \(r\). The normalized least atom \(3^nc_n\) decreases to a positive limit \(\), giving \(c_n=3⁻ⁿ(1+o(1))\). The limiting \(3\)-adic law has a Haar density \(f\) with optimal lower bound \(ess\,inf_H f=2/3\). We prove that \(f∈ L^q(H)\) exactly for \(1≤ q<2\), although \(f\) is essentially unbounded on every unit cylinder. Let \(N_a(x,τ)\) count distinct starting integers \(|m|≤ x\) that reach \(a\) within \(τ\) steps of the one-division Collatz map, and put \(Ψ(x)=√log x\,loglog x\). For every fixed signed target \(a\) not divisible by three, we prove\[N_a\!(x,2/log(4/3)log x+D_aΨ(x))_0x/exp(C_0Ψ(x))=x¹⁻ᵒ⁽¹⁾\]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