Exact lengths and a quadratic bound for a Collatz variant over binary polynomials

Gallardo and Rahavandrainy studied the map O ↦ op((x²+x+1)O+1) on odd binary polynomials, where op removes all factors x and x+1. They proved that every trajectory reaches 1, with an odd sequence of length at most 2n−1 for a starting polynomial of degree n ≥ 1, and stated several conjectures based on computation. We show that a run of consecutive terms of degree d ≥ 2 has at most ⌊d/2⌋ terms, with equality attainable for each d. This gives the quadratic bound ⌊n²/4⌋+1 for the length of every odd sequence starting from a polynomial of degree n. We determine exactly the length and the degree structure of the odd sequence of xⁿ+x+1: for n ≥ 3 its length is 2⌈log₂ n⌉−2+1. This proves the trinomial length conjecture in the formulation of the authors' earlier preprint (arXiv:2308.01181). We also give a short recursive proof of the known length formula for (x²+x+1)ⁿ+1. All numbered lemmas, propositions, theorems and corollaries have been formally verified in Lean 4 with Mathlib; the formalization is available at https://github.com/coo001/binpoly-collatz-lean. The proofs, the manuscript and the formalization were written with the help of AI assistants, as stated in the manuscript.