Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Certified Syracuse descent on 26 progressions inside n≡15(mod16)n \equiv 15 \pmod{16}n≡15(mod16)

Proved
syracuse_descent_progressions_fifteen_mod16

by Zexuan Liu · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemsiterationnumber-theoryopen-problemstopping-time

For every nnn in any of the 26 arithmetic progressions listed below, the Syracuse orbit of nnn drops below its starting point within at most 777 steps:

∃ t≤7:Tt(n)<n.\exists\, t \le 7 : \quad T^{t}(n) < n .∃t≤7:Tt(n)<n.

These are exactly the residue classes modulo a power of 222 up to 2122^{12}212, inside n≡15(mod16)n \equiv 15 \pmod{16}n≡15(mod16), on which the Terras affine certificate closes. Together they cover a proportion 0.46880.46880.4688 of that class; the complement is left open in the companion statement.

The progressions:

  • n≡15(mod128)n \equiv 15 \pmod{128}n≡15(mod128)
  • n≡79(mod256)n \equiv 79 \pmod{256}n≡79(mod256)
  • n≡95(mod256)n \equiv 95 \pmod{256}n≡95(mod256)
  • n≡175(mod256)n \equiv 175 \pmod{256}n≡175(mod256)
  • n≡287(mod1024)n \equiv 287 \pmod{1024}n≡287(mod1024)
  • n≡367(mod1024)n \equiv 367 \pmod{1024}n≡367(mod1024)
  • n≡575(mod1024)n \equiv 575 \pmod{1024}n≡575(mod1024)
  • n≡735(mod1024)n \equiv 735 \pmod{1024}n≡735(mod1024)
  • n≡815(mod1024)n \equiv 815 \pmod{1024}n≡815(mod1024)
  • n≡975(mod1024)n \equiv 975 \pmod{1024}n≡975(mod1024)
  • n≡383(mod4096)n \equiv 383 \pmod{4096}n≡383(mod4096)
  • n≡463(mod4096)n \equiv 463 \pmod{4096}n≡463(mod4096)
  • n≡879(mod4096)n \equiv 879 \pmod{4096}n≡879(mod4096)
  • n≡1087(mod4096)n \equiv 1087 \pmod{4096}n≡1087(mod4096)
  • n≡1231(mod4096)n \equiv 1231 \pmod{4096}n≡1231(mod4096)
  • n≡1647(mod4096)n \equiv 1647 \pmod{4096}n≡1647(mod4096)
  • n≡1823(mod4096)n \equiv 1823 \pmod{4096}n≡1823(mod4096)
  • n≡1855(mod4096)n \equiv 1855 \pmod{4096}n≡1855(mod4096)
  • n≡2031(mod4096)n \equiv 2031 \pmod{4096}n≡2031(mod4096)
  • n≡2239(mod4096)n \equiv 2239 \pmod{4096}n≡2239(mod4096)
  • n≡2351(mod4096)n \equiv 2351 \pmod{4096}n≡2351(mod4096)
  • n≡2591(mod4096)n \equiv 2591 \pmod{4096}n≡2591(mod4096)
  • n≡2975(mod4096)n \equiv 2975 \pmod{4096}n≡2975(mod4096)
  • n≡3119(mod4096)n \equiv 3119 \pmod{4096}n≡3119(mod4096)
  • n≡3295(mod4096)n \equiv 3295 \pmod{4096}n≡3295(mod4096)
  • n≡4063(mod4096)n \equiv 4063 \pmod{4096}n≡4063(mod4096)

The certificate

Let T(n)=(3n+1)/2 v2(3n+1)T(n) = (3n+1)/2^{\,v_2(3n+1)}T(n)=(3n+1)/2v2​(3n+1) be the Syracuse (accelerated Collatz) map, which sends an odd nnn to the odd part of 3n+13n+13n+1.

Terras's observation is that a residue class fixes an initial segment of the orbit's 222-adic data. Write n=2kq+rn = 2^k q + rn=2kq+r. Then 3n+1=(3r+1)+3⋅2kq3n+1 = (3r+1) + 3\cdot 2^k q3n+1=(3r+1)+3⋅2kq, so v2(3n+1)=v2(3r+1)=:a1v_2(3n+1) = v_2(3r+1) =: a_1v2​(3n+1)=v2​(3r+1)=:a1​ as soon as a1<ka_1 < ka1​<k, and

T(n)  =  3r+12a1+3⋅2 k−a1q.T(n) \;=\; \frac{3r+1}{2^{a_1}} + 3\cdot 2^{\,k-a_1} q .T(n)=2a1​3r+1​+3⋅2k−a1​q.

Iterating, as long as the running total Vi=a1+⋯+aiV_i = a_1 + \dots + a_iVi​=a1​+⋯+ai​ stays below kkk, the valuations aia_iai​ are the ones read off the representative rrr, and

Tt(n)  =  3tn+ct2Vt,ct  =  2VtTt(r)−3tr  ≥  0,T^{t}(n) \;=\; \frac{3^{t} n + c_t}{2^{V_t}}, \qquad c_t \;=\; 2^{V_t} T^{t}(r) - 3^{t} r \;\ge\; 0 ,Tt(n)=2Vt​3tn+ct​​,ct​=2Vt​Tt(r)−3tr≥0,

an affine function of nnn on the whole class.

Two further points make the certificate sharp:

  • Truncated last step. When the remaining budget j=k−Vt−1j = k - V_{t-1}j=k−Vt−1​ is at most ata_tat​, the valuation is no longer pinned down, but 2j∣3nt−1+12^{j} \mid 3n_{t-1}+12j∣3nt−1​+1 still holds, so T(nt−1)≤(3nt−1+1)/2jT(n_{t-1}) \le (3n_{t-1}+1)/2^{j}T(nt−1​)≤(3nt−1​+1)/2j. A one-sided bound is all a strict inequality needs, so this final step may be spent even though it is not exact.
  • The least representative decides. Since ct≥0c_t \ge 0ct​≥0, the inequality Tt(n)<nT^{t}(n) < nTt(n)<n for every nnn in the class is equivalent to ct<(2Vt−3t) rc_t < (2^{V_t} - 3^{t})\,rct​<(2Vt​−3t)r, i.e. to the same inequality at the smallest member rrr of the class. So checking the representative certifies the entire progression.

Consequently each progression listed below carries a finite, purely computational witness, and the bound t≤Tmax⁡t \le T_{\max}t≤Tmax​ is uniform across the class.

Formalization note. No oddness or positivity hypothesis is needed: each congruence already forces nnn odd and nnn at least the stated residue. The step bound is stated as t≤7t \le 7t≤7 so that the lemma composes with a case split without re-deriving a bound.

Preamble
import Mathlib
import Definitions.Def_syracuseStep
Formal statement
theorem syracuse_descent_progressions_fifteen_mod16 (n : ℕ)
    (h : n % 128 = 15 ∨
      n % 256 = 79 ∨
      n % 256 = 95 ∨
      n % 256 = 175 ∨
      n % 1024 = 287 ∨
      n % 1024 = 367 ∨
      n % 1024 = 575 ∨
      n % 1024 = 735 ∨
      n % 1024 = 815 ∨
      n % 1024 = 975 ∨
      n % 4096 = 383 ∨
      n % 4096 = 463 ∨
      n % 4096 = 879 ∨
      n % 4096 = 1087 ∨
      n % 4096 = 1231 ∨
      n % 4096 = 1647 ∨
      n % 4096 = 1823 ∨
      n % 4096 = 1855 ∨
      n % 4096 = 2031 ∨
      n % 4096 = 2239 ∨
      n % 4096 = 2351 ∨
      n % 4096 = 2591 ∨
      n % 4096 = 2975 ∨
      n % 4096 = 3119 ∨
      n % 4096 = 3295 ∨
      n % 4096 = 4063) :
    ∃ t : ℕ, t ≤ 7 ∧ syracuseStep^[t] n < n := by sorry
Source
https://en.wikipedia.org/wiki/Collatz_conjecture; supporting lemma for the prove2.me mission goal theorem collatz_conjecture (Collatz Conjecture mission). Riho Terras, A stopping time problem on the positive integers, Acta Arith. 30 (1976), 241-252, Section 2 (the coefficient/parity vector and the affinity of T^t on residue classes mod 2^k); Jeffrey C. Lagarias, The 3x+1 Problem and Its Generalizations, Amer. Math. Monthly 92 (1985), 3-23, Section 2, https://websites.umich.edu/~lagarias/3x%2B1.html

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me