Collatz, but stop at the drop; A game with two letters: the proofs

Under the reduced Collatz map T, every finite parity word determines a residue class of starting values. An admissible word is a first passage of the associated multiplicative level below 1; every sufficiently large positive member of its residue class first falls below its starting value at the end of that word. The affine iteration formula and the counts a(n) of admissible words with n odd steps (OEIS A100982) are known. Here we study the combinatorial structure of these words. New here, as far as we know: 1. Chains. Cut at its record lows, every admissible word is, in exactly one way, a chain of smaller admissible words, and admissible words glue into an admissible word if and only if an inequality holds that depends on their numbers of ones only. This gives a recurrence for a(n). 2. Trees. The same cuts make the words plane trees, characterized by a local condition, and read off a bracket word. 3. Sweeps. The sweep map of rational Catalan combinatorics permutes the admissible words with a given number of ones; two variants of it are permutations exactly at the upper, and at the lower, semiconvergent denominators of log2(3). Items 1 to 3 hold for every odd multiplier q >= 3. 4. A finite check. Terras's coefficient stopping time conjecture reduces, at each number n of odd steps, to the class ids up to n 3^(n-1)/d, where d is the distance from 3^n up to the next power of 2. With a range check up to 9.8 x 10^11 it holds for every n up to 10,781,273, that is, for coefficient stopping times up to 17,087,914 (Terras proved it below 2593, Garner below 105,000), and by Rhin's bound the range to check grows only polynomially with n. Every result with a Lean name, the known ones included, is proved in Lean 4 with Mathlib, without sorry; open statements, the range check and two published theorems enter as named hypotheses.