slug: arxiv-2510-07530-gallardo-rahavandrainy-collatz-length-bound
bibkey: gallardo2025collatzlength
doi: 10.48550/arXiv.2510.07530
url: https://arxiv.org/abs/2510.07530v1
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/GallardoRahavandrainyCollatzLengthBound.result

A polynomial bound for binary-polynomial Collatz length

Problem

Gallardo and Rahavandrainy, A variant of Collatz’s Conjecture over Binary Polynomials, arXiv:2510.07530v1, §1, state: “However, several computations suggest that here also r_A is bounded by a polynomial in deg(A) (see Section 3).” The question is preregistered in #20129. For every nonzero $A\in {\mathbb{F}}_2[x]$, the theorem rA_quadratic proves $r_A\le 2+\lfloor \mathrm{deg}(A{)}^2/4\rfloor$. The theorem result proves the literal polynomial-bound prediction, using $p(X)=X^2+2\in \mathbb{N}[X]$.

Statement echo

The natural degree agrees with polynomial degree on the nonzero domain. Definitions are total at zero; the theorem excludes zero. The existential polynomial witness is an upper envelope of the sharper floor estimate.

Motivation

The source’s Theorem 1.2 proves termination with an exponential bound. The settling GID is D5/S1/Recurrence/GallardoRahavandrainyCollatzLengthBound.result. The imported owner also settles the distinct Conjecture 3.11 of arXiv:2308.01181v2 under #19299; its dossier and resolution claim remain attached to that owner’s result.

Gap

The polynomial-bound prediction is proved. The Lean proof gives a bound on plateau duration and the quadratic length estimate. Exact plateau duration and sharpness examples below are proved in prose, rather than asserted as additional kernel-checked theorems. A linear uniform bound remains open. Literature completeness is ASSUMED-UNVERIFIED.

Route

Let $P=x(x+1)$ and $T(F)=\mathrm{oddPart}(1+M_{1}F)$. For odd $F\ne 1$, put $k=\min (v_x(F+1),v_{x+1}(F+1))$. Both multiplicities are positive and $k\le \lfloor \mathrm{deg}(F)/2\rfloor$. A degree-preserving step removes one factor of each linear polynomial, and decreases this minimum by one. Strong induction on $k$ gives a strict degree decrease within $k$ steps (plateau_escape). Strong induction on degree, using the consumed square_budget_step, bounds the first odd hitting index by $\lfloor \mathrm{deg}(A{)}^2/4\rfloor$ (oddSeq_hit). The terminal pair holds from the next index onward (rA_le_hit), giving the extra two in rA_quadratic. The public settling result chooses $X^2+2$ and applies that estimate.

Falsifier

A nonzero binary polynomial whose length exceeds the stated estimate would contradict rA_quadratic. A mismatch between the source’s terminal-pair count and rA would invalidate fidelity; the statement echo and the source examples use that exact count.

Evidence

The Lean modules are D5/S1/Recurrence/GallardoRahavandrainyBinaryCollatz.lean and D5/S1/Recurrence/GallardoRahavandrainyCollatzLengthBound.lean, with their corresponding Blueprint Scribes. The axiom closure of every public declaration is contained in $\{\mathrm{propext},Classical.choice,Quot.sound\}$.

The experiment is the pinned experiment directory. Command: python3 docs/reports/gallardo-rahavandrainy-2025-binary-collatz-length-bound/check.py in that experiments checkout; exit 0. Script SHA-256: 4f0db8a8d3cf2081c030bc3b8df0bb194c991b58c8831c2ef48f015531422238. It reproduces the source’s degree sequences for $M_1^n+1$, $9\le n\le 16$; $x^n+x+1$, $31\le n\le 34$; and its three polynomials $P_1,P_2,P_3$. It enumerates every nonzero binary polynomial of degree at most 14. The longest degree-$n$ plateau is $\lfloor n/2\rfloor$ for $2\le n\le 14$; at degree 14 the maximum length is 16 and the quadratic bound is 51. These exact finite readings corroborate the conventions and do not prove an unbounded claim.

The four-slot escape audit is unfinished under #20796 for rA_quadratic, result, and the six published owner prerequisites. The existing owner’s result is also included in #20796, with its exact-domain registration boundary detailed in #19534. No declared_validated registration is asserted.

Declaration roles and source consumers

The table is extracted from the elaborated declaration dependency graph; consumer names refer to source declarations. Bind-only entries organize the proof. The admission basis is open-problem-resolution (#20129; Proved).

Triage

What the settlement shows

Exact plateaus and attaining examples

This paragraph is a proof in prose. Fix an odd $F\ne 1$ of degree $d$. Write $F+1=P^{k}C$ with $k=\min (v_x(F+1),v_{x+1}(F+1))\ge 1$. At least one of $C(0),C(1)$ is 1: otherwise both root multiplicities exceed $k$. For $0\le j\le k$ define $B_j=1+M_1^j{P}^{k-j}C$. For $j<k$, both evaluations of $B_j$ are 1 and its degree is $d$, since $\mathrm{deg}{M}_1=\mathrm{deg}P=2$ and $d>0$. The identity $1+M_1=P$ gives $1+M_1{B}_j=P{B}_{j+1}$. For $j<k-1$, $B_{j+1}$ is odd, so $T(B_j)=B_{j+1}$. At a root $\alpha \in \{0,1\}$ where $C(\alpha )=1$, one has $B_k(\alpha )=0$ since $M_1(\alpha )=1$. Also $B_k\ne 0$, because $M_1^{k}C=1$ is impossible for $k\ge 1$. Thus removing the linear factors from $B_k$ strictly decreases degree. The plateau consists of exactly $B_0,\dots ,B_{k-1}$. Since $2k\le d$, its length is at most $\lfloor d/2\rfloor$. For degree $2k$, the odd polynomial $1+P^k$ has minimum multiplicity $k$; for degree $2k+1$, use $1+x{P}^k$, whose multiplicities are $k+1$ and $k$. They attain the bound. This proves $g(d)=\lfloor d/2\rfloor$ for every $d\ge 2$. These are consequences of the displayed polynomial identities; they are not additional Lean declarations in this delivery.

For the source’s conditional estimate (4), write $n=2q$ or $n=2q+1$. For even $n\ge 2$, the difference $n(n+1)/2-(2+\lfloor n^2/4\rfloor )=q^2+q-2$ is nonnegative for $q\ge 1$. For odd $n\ge 3$, it is $q^2+2q-1$, also nonnegative for $q\ge 1$. Hence that estimate is unconditional on this range.

Literature scope

The preregistration records searches by title, identifier, authors and polynomial Collatz terminology. It reports that the journal version Revista de la Unión Matemática Argentina 69(1), 295–302, DOI 10.33044/revuma.5555, retains the prediction. Alon–Behajaina–Paran (arXiv:2401.03210) and Behajaina–Paran (arXiv:2312.00390) use multiplier $x+1$ and remove only powers of $x$; those statements do not settle the present two-root process. The distinct Conjecture 3.11 is settled by the imported owner. These are preregistration-reported literature readings.

ASSUMED-UNVERIFIED

Prior-art completeness, including full-text and citation-index coverage, is ASSUMED-UNVERIFIED. The journal-version reading is preregistration-reported. The four-slot escape audit remains unfinished under #20796 and #19534.