The 2^k-Family Construction for the Collatz Conjecture: A Rigorous Mathematical Audit

Abstract

Referee-style audit of the n·2^k family and reverse-chain construction for the Collatz conjecture. Results: (1) the family step is exactly the even branch of the Collatz map and reduces the conjecture, without loss, to the odd integers; (2) chain reversal is legitimate but circular, since coverage of the reverse tree of 1 is equivalent to the conjecture; (3) the two inductions hidden in the construction are identified and three natural repairs are each proven equivalent to the full problem; (4) the single missing step is isolated as the Descent Lemma (every odd m > 1 has an iterate strictly below itself), also equivalent to the conjecture. Computational audit: all n ≤ 10^6 converge (max shortcut stopping time 329 at n = 837,799; max C-flight peak 56,991,483,520 at n = 704,511); the Descent Lemma holds for all odd m ≤ 10^7 (deepest 155 odd-steps at m = 8,088,063; j(m) = 1 exactly on the residue class m ≡ 1 mod 4, i.e. 2,499,999 values); the reverse-tree BFS reproduces the exhibited chains of 3, 5 and 7 exactly and shows canonical tree paths can be forced far above their targets (the path to 27 peaks at 9,232). Machine verification: the twelve core results are additionally formalized and machine-checked in Lean 4 (version 4.33.1, core Lean only, no sorry; axiom dependencies limited to propext, Classical.choice and Quot.sound). The Lean certificate accompanies this record as a supplementary file.