Minor errata to Halbeisen–Hungerbühler (1997) and Lagarias (1990) on rational Collatz cycles, found while formalising them in Lean 4

While formalising in Lean 4 two classical papers on rational Collatz cycles, L. Halbeisen and N. Hungerbühler, Optimal bounds for the length of rational Collatz cycles, Acta Arith. 78 (1997) 227–239, and J. C. Lagarias, The set of rational cycles for the 3x+1 problem, Acta Arith. 56 (1990) 33–53, we found a number of slips: misprints in formulas and indices, two wrong rows in a table, numerical constants, claims that fail in edge cases, and steps of proofs that need a repair. This note lists those that are checked by a Lean theorem or by a script, each with the printed text, what is wrong and a correction. None of them invalidates a theorem that we formalised: all the theorems of Halbeisen–Hungerbühler, and those of Lagarias except 3.3 and 4.3, are proved in Lean, in the forms given in §5 of the note (for Lagarias, with the prime number theorem and the Baker–Fel'dman bound as named hypotheses where the paper uses them, and Theorem 3.2 with log2 and |D(v)|). The list is not exhaustive. Files: errata_note.pdf (the note, 6 pages); errata_checks.py (Python 3, standard library only: re-runs the numerical checks of the formalisation and recomputes the small examples quoted in the note) and its recorded output errata_checks.out.txt. The Lean formalisations are archived as software: doi:10.5281/zenodo.23514572 (v1.1, both papers) and doi:10.5281/zenodo.23498096 (v1.0, Halbeisen–Hungerbühler). Use of AI: the Lean statements and proofs, the scripts and this note were written by Claude (Anthropic), an AI system, under the direction of Eric Merle, who is responsible for their content.