The invariant m₀ of Sawin–Shusterman–Stoll for the pairs (1+kx, l): a stopping rule, every prime l, and a proved range

Abstract

Sawin, Shusterman and Stoll attach to a pair (c,d) of integer polynomials with c(0),d(0) ≠ 0 an integer m₀(c,d): the least M such that for every m>M, every pair (a,b) with deg a,deg b<m, ab ≡ cd mod xᵐ and wt(a)+wt(b) ≤ wt(c)+wt(d) already satisfies ab=cd, where wt(·) is the squared Euclidean length of the coefficient vector. It controls the threshold beyond which the non-reciprocal part of x^(N)c(x⁻¹)+d(x) is irreducible. For the two-parameter family (c,d)=(1+kx, l) they prove m₀=1 on a range, and remark that outside it m₀(1+kx,l) ≤ 2 appears to hold, with the two exceptions m₀(1+2x,4)=4 and m₀(1+3x,9)=3; a proof "should be possible", they write, "but the arguments seem to get rather technical". No verification range is stated. We contribute three things. First, a stabilisation lemma: for a weakly robust pair with (cd)(0) ≠ 0, the property "every element of Tₘ satisfies ab=cd" is monotone in m. This is what makes the authors' own procedure — compute T₁,T₂,… until ab=cd throughout — a stopping rule, and it turns the infinite assertion m₀(c,d) ≤ M into a single condition on the one set T_(M+1); the source does not state it. Second, an infinite unconditional sub-family: m₀(1+kx,l) ≤ 2 for every k ≥ 1 and every prime l, with no computation, by a sum-of-squares certificate; the source's lemma reaches prime l only for l ≥ 5 and k ≤ l²/2. Third, two narrowing inequalities which confine a hypothetical further exception to the band 2 ≤ a₀ ≤ b₀ ≤ k ≤ sqrta₀²+b₀², where a₀b₀=l. They leave k in an interval of length about a₀²/2b₀ rather than in a box, and enumerating that interval — each of the two levels of the enumeration being a line meeting a disk, which is what makes it affordable — proves the remark's bound m₀ ≤ 2 for every k ≥ 1 and every l with 2 ≤ l ≤ 4 · 10⁴ such that (1+kx,l) is weakly robust and (k,l) is not one of the two exceptions; no upper bound on k is imposed. We also certify the two exceptional values themselves, m₀(1+2x,4)=4 and m₀(1+3x,9)=3, and that the constant 2 cannot be lowered. All of this is machine-checked in Lean 4.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 2 · current (opens in a new tab)

   Source snapshot 2026-09-07 03:53 UTC

   File fingerprint

   9637d8779b0c9026cfa71d38be41a78860b7df22a71522fcc0ddaf556ae5d294