Finite Adaptive Dyadic Certificates for the Six Canonical 3n+b CollatzMaps: Verification on[1,9·2^14] and a Lean4 Formal Audit

For an odd shift b with gcd(3,b) = 1, the generalized Collatz map T3,b is defined by T3,b(n) = 3n + b when n is odd, and T3,b(n) = n/2 when n is even. We study the six canonical representatives b in {1, 5, 7, 11, 13, 17} of the admissible residue classes modulo 18. For each representative, we provide a complete finite adaptive dyadic certificate tree on the domain [1, M0], where M0 = 147,456. The certificates are verified computationally with zero failures across all six representatives, covering 294,903 admissible sources. The maximum observed depth is Bmax = 146, against the common analytic budget 323, and the inventory contains 25 terminal cycles. A Lean 4 formal audit, verified by native_decide inside the kernel, confirms the finite certification for each representative. This finite Lean audit is unconditional: no sorry, no axiom, no admit. The result is deliberately finite and representative-level: it does not assert a conjugacy or a uniform certification for all shifts b = r + 18t.