slug: gallardo-rahavandrainy-2023-binary-collatz-3-11
bibkey: gallardo2023binarycollatz
doi: 10.48550/arXiv.2308.01181
url: https://arxiv.org/abs/2308.01181v2
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/GallardoRahavandrainyBinaryCollatz.result

Gallardo–Rahavandrainy Conjecture 3.11

Problem

Gallardo and Rahavandrainy, On Collatz Conjecture for binary polynomials, arXiv:2308.01181v2, Conjecture 3.11, p. 15, state: “If $A=(M^2+M+1{)}^n$ with $n\ge 2$, then ${\ell }_A$ equals $n+1$.” Here $M=x^2+x+1$ in ${\mathbb{F}}_2[x]$. The source calls a polynomial odd when it is coprime to $x(x+1)$, removes all powers of these two linear factors to obtain its odd part, and iterates the odd part of $1+MA$.

Statement echo

The total definition of oddPart also accepts zero. The proof only transports nonzero polynomials with the required oddness; this total extension does not weaken or change the stated conjecture.

Motivation

The source proves the power-of-two case in Lemma 3.3 and gives examples for $n=9,\dots ,16$. The exact formula for every $n\ge 2$ is a tier-1, externally named conjecture, preregistered in #19299. The settling declaration is D5/S1/Recurrence/GallardoRahavandrainyBinaryCollatz.result.

Gap

The binding conjecture is proved. Completeness of the literature screen is ASSUMED-UNVERIFIED; no complete classification of binary-polynomial Collatz lengths, or sharper general bound, is asserted.

Route

Put $m=1+y$ and $q=1+y+y^2$. Composition with $x(x+1)$ sends $m$ to the source’s $M$ and $q$ to $M^2+M+1$. Polynomial reversal conjugates the resulting odd-part process to $R(f)=mf+y^{\mathrm{deg}f+1}$. A degree-gap reduction establishes termination and reduces its first hitting time $h$.

The consumed private declarations Dynamics.square_doubling and Dynamics.q_square_doubling prove, for every $f$ with $f(0)=1$, $h(f^2)=2h(f)$ and $h(q{f}^2)=2h(f)+1$. Dynamics.q_power_height uses the even and odd cases of the exponent to prove $h(q^n)=n$. Dynamics.q_power_hitting_set identifies the exact hitting sets under transport, and Dynamics.length_q_power proves the source length $n+1$ for every natural $n$. The six public prerequisites Dynamics.nonzero_of_odd, Dynamics.nonzero_eq_one, Dynamics.degree_q, Dynamics.q_ne_zero, Dynamics.eq_one_of_degree_zero and Dynamics.oddPart_factor are consumed by GallardoRahavandrainyCollatzLengthBound. The other auxiliary declarations are private helpers; result settles the conjecture.

Falsifier

A natural $n\ge 2$ for which the source process first reaches 1 at a step other than $n$, or fails to reach it, contradicts claim. Failure of the composition or reversal correspondences would invalidate this route; their exact identities are proved in the settling module.

Evidence

The Lean source is D5/S1/Recurrence/GallardoRahavandrainyBinaryCollatz.lean, with its Blueprint Scribe and generated mathematical exposition at the corresponding paths. Its axiom closure is contained in $\{\mathrm{propext},Classical.choice,Quot.sound\}$.

The experiment is the pinned experiment directory. Command: python3 docs/reports/gallardo-rahavandrainy-2023-binary-collatz-3-11/check.py in that experiments checkout; exit 0, RESULT PASS. Script SHA-256: 86f968206e76be2c8db4d0ce65d68113ff1e64d43beee8bf64c8240fab8b6e12. It checks the source lengths for $n=2,\dots ,80$, both doubling identities for all 1024 odd polynomials of degree at most 10, and $h(q^n)=n$ for $n=0,\dots ,199$. Its displayed source degree sequences cover $n=2,\dots ,12$, including $n=9$ with $[36,32,32,32,32,32,30,30,4,0]$ and length 10. These finite checks corroborate the proof and do not establish its universal scope.

The escape audit of all seven public theorems is unfinished under #20796. The exact-domain registration boundary of result is detailed in #19534. No validated four-slot registration is asserted.

Declaration roles and source consumers

The table is extracted from the elaborated declaration dependency graph. Bind-only entries organize consumed proofs. The admission basis is open-problem-resolution (#19299; Proved).

Triage

What the settlement shows

Literature scope

The screen recorded in #19299 includes source versions v1 and v2 (v2 retains Conjecture 3.11), the same authors’ arXiv:2510.07530 and works 2602.13111, 2412.17850, 2406.10748, 2509.00619 and 2606.08640. It includes Alon–Behajaina–Paran arXiv:2401.03210 (the cited family covers power-of-two exponents), Behajaina–Paran arXiv:2312.00390, Matthews–Leigh, Snapp–Tracy, Nichols arXiv:1610.02545 and Lagarias’s bibliography. These are preregistration-reported literature readings, not Lean dependencies. The source and the searches in that issue establish the named target and the searched scope; they do not establish exhaustive absence of prior art.

ASSUMED-UNVERIFIED

Literature completeness remains ASSUMED-UNVERIFIED, including the full text of Hicks–Mullen–Yucas–Zavislak and detailed Nichols proof passages. The escape audit remains unfinished under #20796 and #19534.