A computer-assisted well-founded descent for Collatz components under dyadic leaf certificates in the 6-bit hierarchy Mt = 9 · 214+6t (shifts64 scale M1 = 9 · 220, version m = 7

Collatz, 3x+1, théorie des nombres, certificats, vérification computationnelle, descendance bien fondée This revision does not modify the mathematical argument or the structure of the proof. It addresses five points of clarity and rigour identified during a careful re-reading. --- 1. Base case u = 7 (new Remark 7.1) The value u = 7 is the unique fixed point of the descent procedure in the regime e(u) <= 6. One computes Y(7) = 1, and since S(1) = 1 the sequence (y_k) is constantly 1; the anti-9 lift then returns w = (64-1)/9 = 7 = u, so no decrease occurs. This case is now explicitly excluded from the certificate tables, explained in a dedicated remark, and handled as a second base case with direct verification: 21 -> 64 -> 32 -> 16 -> 8 -> 4 -> 2 -> 1. 2. Strong induction — two base cases Theorem 3 now states two explicit base cases (u = 1 and u = 7), and the induction step is restricted to odd u > 1 with u ≠ 7, making the logical structure fully transparent. 3. Theorem 1 — explicit conclusion The statement of Theorem 1 previously read as a hypothesis without a formal consequence. It now carries an explicit "Then..." clause establishing the descent for the regime e(u) <= 6, making it a proper conditional theorem. 4. Lemma 2 — conditional nature clarified The original proof referred to orbits being "eventually periodic," which could appear to presuppose what the paper aims to prove. A short note has been added making explicit that the lemma is purely conditional: it asserts only that convergence propagates within a component, and assumes nothing about global convergence of Collatz orbits. 5. Proposition 1 — positivity and parity of w The facts w > 0 and w odd were previously asserted without justification. Both are now established in a brief paragraph: since r >= 1, 2^r * y_k is even, so 2^r * y_k - 1 >= 1 is odd; divisibility by 9 then gives w >= 1 odd. --- The companion archive and the Python verifier are unchanged. All four verification reports continue to end with RESULT: OK.