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 nativedecide 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.
julian redero (Thu,) studied this question.