---
title: "The finite certificate frontier of the Collatz map: what a finite verification proves, and the quantifier it cannot cross"
subtitle: "The integers a parity prefix has not yet brought down form one residue class cut by one height; a finite verification is exactly the extinction of a finite frontier; K(2^40) = 550 is one value of the frontier function; and a uniform depth is refuted outright by an explicit family"
author:
  - "Aletheia — the series' documents; model: ChatGPT, GPT series"
  - "Neo.K — AMRAL Research Lab"
  - "墜衡 (Zhuì Héng) — AMRAL Research Lab, verification; model: Claude, Opus series"
date: 2026-10-18
version: "0.1"
standard: "1"
headline_problem: "Collatz conjecture"
evidence:
  branch: agent/collatz-verification-zhuiheng
  commit: "a2c25aa757c0704bc110458684ef3d459cb3d9e0"
  dir: collatz-verification-zhuiheng
  sources: "data/gate-logs/ot-paper09-recheck.json, data/gate-logs/coverage.json, data/gate-logs/ot-recheck-drill.json, data/paper-figures.json, data/gate-logs/suite-totals.json, data/results.v1.json"
abstract: |
  The Collatz conjecture is open, and nothing here bears on it. For $T(n) = n/2$ or $(3n+1)/2$, let
  $\sigma(n)$ be the first $j \ge 1$ with $T^j(n) < n$. The conjecture is equivalent to $\sigma(n) < \infty$
  for every $n > 1$, and a verification that $\sigma$ is finite on $[2, N]$ proves the conjecture on
  $[1, N]$ and nowhere else. This paper makes that precise in the terms of the local affine atlas. The
  integers that follow a parity word $w$ and have not descended within its length are one residue class
  cut by one exact height, $\Omega_w \cap [1, h(w)]$, with $h(w)$ read off the word's contracting prefixes;
  a verification on $[2, N]$ is exactly the extinction of a finite frontier of such cylinders, at depth
  $K(N) = \max_{n \le N} \sigma(n)$; and $\sigma(n) = \infty$ exactly when $n$ anchors an infinite hard branch of
  residue classes, so that the conjecture is the absence of such a branch at any integer above 1.

  Measured in these terms: $K(2^{40}) = 550$, attained at $n = 898696369947$, whose orbit climbs to
  395806039507110357728, about $4.4042 \times 10^8$ times the start, before first falling below it. And one
  sentence of the series is sharpened from evidence to proof. The series warns that the depth $K(N)$
  cannot be made uniform in $N$, calling a uniform bound incompatible with observed behaviour; it is
  false outright, because $2^m - 1$ climbs for $m$ steps, and the same family is a nested chain of residue
  classes, hard at every depth, that is anchored at no integer at all. Every statement is checked against
  a referee that assumes none of them, and the equivalence, the absence of a uniform depth and the
  anchored-branch characterization are formalized.
keywords: [Collatz conjecture, stopping time, finite verification, residue classes, certificates, formal verification]
---

> **Status of this document.** Preprint, version 0.1: complete enough to stand in public, and not
> final; a later version may revise it. Not prepared for journal submission. Section 8 records who
> did which part, including the parts this line did not do.

# 0. What is claimed, and what is not

Six kinds of statement are kept apart and never merged; the distinction is not presentational,
it is the content.

| label | meaning |
| --- | --- |
| `COMPUTED_HERE` | recomputed in this line with independently written code, never by running the programme's own scripts |
| `DERIVED_FROM_VERIFIED_INPUTS` | follows from quantities this line already computed |
| `CITED_THEOREM` | a published result, cited and checked as a citation |
| `INHERITED` | taken from the programme's documents and never verified here; every use is marked |
| `UNMEASURED` | well posed, and not established here |
| `FAILED` | attempted and refused |

In particular `PASS` and `PASS by cited theorem` are **different verdicts** and are never written
as one; no result in this paper rests on a cited theorem.

**Not claimed anywhere in this paper:** the Collatz conjecture; any bound on $K(N)$ beyond the one value
measured, or on its growth; that a finite verification at any size says anything about the integers
above it; that the proportion of integers needing explicit work tending to zero implies that none do;
and novelty of the elementary statements, several of which are folklore of computational verification.

**Inherited:** one comparison, marked where it is made (§3): the series' account of how a recent
verification algorithm organizes its sieves. That paper's title, author and date were checked against
its record; the account of its method was not.

Where the other labels sit: the theorems of §§1–3 and §§5–6 are proved in the text and checked; those
of §§1, 5 and 6 are also formalized; the frontier measurements of §4 are `COMPUTED_HERE`; the bounds on
$\sigma$ of the all-ones family are `DERIVED_FROM_VERIFIED_INPUTS`; two readings the series itself warns
against — a uniform depth, and a formal hard branch as a counterexample — are `FAILED`, each refused by
an explicit family (§§5–6); and the growth of $K(N)$ is `UNMEASURED` (§9).

# 1. What a finite verification proves

Let $T(n) = n/2$ for even $n$ and $(3n+1)/2$ for odd $n$, and for $n > 1$ let
$$\sigma(n) = \min\{\, j \ge 1 : T^j(n) < n \,\}, \qquad \sigma(n) = \infty \text{ if there is none.}$$

**Theorem 1.1.** Every positive integer reaches 1 if and only if $\sigma(n) < \infty$ for every $n > 1$.
*Proof.* If every $\sigma$ is finite, strong induction from 1 carries every $n$ down to something already
known to reach 1. Conversely an orbit of $n > 1$ that reaches $1 < n$ falls below $n$ at some first
step. $\square$

**Corollary 1.2 (bounded verification, and only that).** If $\sigma(n) < \infty$ for every $2 \le n \le N$,
every $n \le N$ reaches 1 — and nothing follows about any $n > N$. The formalization states the bounded
conclusion and deliberately contains no theorem bridging it to the unbounded one: that bridge is the
conjecture. An exhaustive descent verification on an interval, such as this line's run to $2^{40}$
recorded in its overview paper, is an instance of the corollary and of nothing more.

# 2. The integers a prefix has not brought down

Let $w$ have prefixes $w_{\le j}$ with $u_j$ odd letters and correction $b_j$, so that on the residue class
$\Omega_w$ of integers following $w$, $T^j(n) = (3^{u_j} n + b_j)/2^j$. With $\Delta_j = 2^j - 3^{u_j}$,
$$T^j(n) - n = \frac{b_j - \Delta_j\, n}{2^j} .$$
A prefix with $\Delta_j < 0$ ascends on all of $\Omega_w$ and so can never certify a descent; a prefix with
$\Delta_j > 0$ has $T^j(n) \ge n$ exactly when $n \le \lfloor b_j/\Delta_j \rfloor$. Let the **hard set** of $w$ be
$H_w = \{ n \in \Omega_w : T^j(n) \ge n \text{ for } 1 \le j \le |w| \}$.

**Theorem 2.1 (hard height).** $H_w = \Omega_w \cap [1, h(w)]$, where
$$h(w) = \min_{j \,:\, \Delta_j > 0} \left\lfloor \frac{b_j}{\Delta_j} \right\rfloor, \qquad h(w) = +\infty \text{ if no prefix contracts.}$$
*Proof.* The expanding prefixes impose nothing; each contracting prefix imposes one upper bound, and the
intersection is the least of them. $\square$

So the obligation left by a prefix is not a dynamical set but **one residue class cut by one height**,
stored as $(r_w, 2^k, h(w))$. It is finite as soon as one prefix contracts, and an entire infinite
progression when none does. Of the 4094 words of length 1 to 11, 3813 have a finite hard height and 281
have none — every prefix on the expanding side, so the whole class is still hard.

**A certificate for a whole class.** Writing $n = r_w + 2^k a$ and $T^k(n) = m_w + 3^u a$, descent at depth $k$
is $(2^k - 3^u)\,a > m_w - r_w$: when $2^k > 3^u$ the class is certified from the quotient
$q_w = \lfloor (m_w - r_w)/(2^k - 3^u) \rfloor + 1$ on, by one integer comparison and no logarithm.

# 3. A verification is a frontier that empties

For $N \ge 2$ and $I_N = \{2, \ldots, N\}$, the **depth-$k$ frontier** is the set of words of length $k$ whose
hard set still meets $I_N$:
$$\mathfrak{F}_k(N) = \{\, w \in \{D,U\}^k : H_w \cap I_N \ne \varnothing \,\}.$$

**Theorem 3.1 (extinction).** $\mathfrak{F}_k(N) = \varnothing$ if and only if $\sigma(n) \le k$ for every
$n \in I_N$. Hence the least such $k$ is
$$K(N) = \max_{2 \le n \le N} \sigma(n),$$
and verifying the conjecture on $[2, N]$ is exactly refining residue cylinders until the frontier is
empty. *Proof.* $n \le N$ is in the hard set of its own word of length $k$ exactly when it has not
descended by step $k$. $\square$

The unproved starts $E_k(N) = \{ n \in I_N : \sigma(n) > k \}$ shrink monotonically in $k$, and the frontier
is their compressed form in the residue atlas; refinement only ever expands surviving cylinders.
Descent certificates are not the only finite proof objects the series admits: a start that merges with
the orbit of a smaller one, or lies on it, is settled too, provided the dependencies are ranked so that
every chain ends at 1 or 2. For fixed $N$ every such object is finite arithmetic, and a family of them
covering $I_N$ proves the conjecture there — the series' finite theorem of coverage, which is the bounded
corollary of §1 with more kinds of evidence.

**What a recent algorithm does (`INHERITED`).** The series compares this frontier with Angeltveit's
recent algorithm for checking the conjecture below $2^N$, which it describes as splitting by low bits and
applying descent, preimage and path-merging sieves, and quotes its observation that the proportion of
integers needing explicit work tends to zero while their number still tends to infinity. The paper's
title, author and date were checked against its record; the description of its method is the series',
and it is reported as such. The point it illustrates does not depend on it: a set of density zero can be
infinite, and a frontier whose surviving proportion vanishes need not ever be empty.

**Checked.** Theorem 2.1 was checked on all 4094 words of length at most 11, including that an expanding
prefix imposes no height at all; the quotient certificate as an exact equivalence, in both directions,
on 37441 cases; the extinction theorem and $K(N) = \max \sigma$; the monotonicity of the hard set; and the
stabilization of canonical residues of Theorem 6.1 below — 13 checks, all passing (`COMPUTED_HERE`).

# 4. One value of the frontier function

The exhaustive run to $2^{40}$ measured $\sigma$ at each of its 549755813887 odd starts — the even ones have
$\sigma = 1$ by the definition of the map — so it already contained the frontier function at that size:
$$K(2^{40}) = 550, \qquad\text{attained at } n = 898696369947 .$$
That start was walked again for this paper with arbitrary-precision integers and no sieve: it stays at
or above itself for 549 steps, climbing to 395806039507110357728, about $4.4042 \times 10^8$ times the
start, and first falls below it at step 550 (`COMPUTED_HERE`; the run's Rust engine, the recheck's
Python walk and this walk agree). At a smaller scale, $K(20000) = 105$, attained at 10087.

This is a measurement, not a bound. It says nothing about $K(N)$ for larger $N$, and §5 shows that no
finite depth serves every $N$.

**Pinned against values it did not produce.** The stopping times $\sigma(3) = 4$, $\sigma(7) = 7$,
$\sigma(27) = 59$, $\sigma(703) = 81$ and $\sigma(10087) = 105$ are checked against an independent walk. They
are there because of a drill: a defect that counted $\sigma$ from 0 instead of 1 survived every other check,
since the frontier, the identity $K(N) = \max\sigma$ and the monotonicity all compare $\sigma$ only with
itself, and a uniform shift moves both sides. A quantity compared only with itself is pinned by nothing.

# 5. There is no uniform depth

The conjecture is $\forall N\ \exists K(N)$ with $\mathfrak{F}_{K(N)}(N) = \varnothing$; the series warns that this
must not be read as $\exists K\ \forall N$, a uniform bound on all stopping times, and calls such a bound
incompatible with observed unbounded stopping times. It is false, and the proof is one line.

**Theorem 5.1.** For every $m \ge 1$ and $1 \le j \le m$,
$$T^j(2^m - 1) = 3^j\, 2^{m-j} - 1 \;\ge\; 2^m - 1 ,$$
so $\sigma(2^m - 1) > m$, and $\sigma$ is unbounded. *Proof.* $2^m - 1$ is odd and
$T(3^j 2^{m-j} - 1) = (3^{j+1} 2^{m-j} - 2)/2 = 3^{j+1} 2^{m-j-1} - 1$ while $m - j \ge 1$; and
$(3/2)^j \ge 1$. $\square$

For example $T^6(127) = 1457$. The identity was checked step by step for every $m$ up to 40, and the actual
stopping times of these starts — 56 at $m = 5$, 146 at $m = 25$, 119 at $m = 40$ — exceed $m$ in every case
and are far from monotone in it (`DERIVED_FROM_VERIFIED_INPUTS`). The uniform reading is therefore not
merely unsupported by observation; it is refuted (`FAILED`), and the formalization proves the absence of a
uniform depth with exactly this family as the witness.

# 6. Anchored and unanchored branches

The residues of an integer $n$ modulo $2^k$ form a nested chain, and once $2^k > n$ the canonical residue
is $n$ itself; a nested chain that is eventually constant at an integer $n$ is **anchored** at $n$. Call $n$
**hard at depth $k$** if it lies in the hard set of its own word of length $k$.

**Theorem 6.1 (anchored hard branches).** For $n > 1$, $\sigma(n) = \infty$ if and only if $n$ is hard at
every depth, if and only if the chain of $n$'s parity prefixes is an infinite hard branch anchored at $n$.
So every positive integer reaches 1 exactly when no integer above 1 anchors an infinite hard branch.
*Proof.* Unwinding the definitions, with the stabilization of canonical residues. $\square$

**Nested is not anchored.** The all-$U$ chain has canonical residues $2^k - 1$: nested, and anchored at no
integer — as a 2-adic integer it is $-1$. By Theorem 5.1 it is also hard at every depth: $2^{k+2} - 1$ lies in its class at depth $k$ and has not
descended by then. So the tree of hard prefixes does have an infinite
branch, and the conjecture is **not** the statement that this tree is well-founded; it is the weaker
statement that no infinite hard branch is anchored at a positive integer. The series draws exactly this
distinction; the all-ones chain turns it from a caution into a witness, and the reading of an infinite
formal hard branch as a counterexample is refused (`FAILED`).

**Formalized.** Theorem 1.1, the bounded corollary, the absence of a uniform depth (with the all-ones
witness), the minimality of $\sigma$ as defined, and the whole of Theorem 6.1 — nested residues, their
stabilization, the existence of nested chains anchored nowhere, the equivalence and its minimal
obstruction form — are proved in this line's Lean development. Every claim in Theorem 6.1 turned out to
be about canonical residues of integers, so the formal proof needs no 2-adic completion at all; the
2-adic integers are where the theorem is interpreted, not where it is proved. One formal statement was
false as first written: the hard set at depth $k$ is witnessed by $2^{k+2} - 1$, not by $2^{k+1} - 1$, which
at depth 0 is the integer 1 and is excluded from the hard set by definition.

# 7. The instrument, and how it was made to fail

The recheck behind this paper shares one mutation drill with the rest of the series' rechecks: a defect is
planted one at a time and must be caught by the check **named** for it, while null controls must disturb
nothing. Across the series' rechecks: of its 69 planted defects, 67 are caught by the check named for each, one is detected only by a crash and one only by a time-out, and all 9 controls stay undisturbed; its log lists every defect with the recheck it targets.
The line's whole suite at the pinned commit stands at 57 drills and 1474 planted defects: 1472 caught by their named check, one detected only by a crash and one only by a time-out, and 128 controls undisturbed.

For this paper's statements the drill planted the hard height taken over the maximum instead of the
minimum, a hard height that admits expanding prefixes, a quotient threshold with $\ge$ for $>$, a class
counted as contracting one power of two early, a class count one term short, an inverted contraction
exponent, $\sigma$ counted from zero, and the referee itself — each caught by its own check, the broken
referee by nine. The $\sigma$ defect is the one of §4: at first it survived everything, and the independent
anchors were added because of it. Two other things the drill corrected before they shipped: a planted
"defect" that changed $3^u \le 2^k$ into $3^u < 2^k$ was no defect at all, the two predicates being equal
because $3^u$ is odd, and had to be re-aimed; and a mutant running from a scratch directory could not find
the archived coverage record, and the check refused rather than skipping — so the drill now passes the
record's location explicitly instead of the check being softened.

# 8. Contributions

The three contributions behind this paper are different in kind, and the paper is worth less if
they are blurred. They are given here in alphabetical order, the order the author list keeps as
data; on the title page the three sit at a round table, with no first and no last.

**Aletheia** — model: ChatGPT, GPT series — wrote, with Neo.K, the paper of the series this paper rests
on: the finite certificate frontier, with its hard heights, its frontier extinction, its anchored
branches and its quantifier boundary.

**Neo.K** set the series' target and its method — that what can be made exact be made exact, and the
one obligation that cannot be isolated by name — and wrote its papers with Aletheia.

**墜衡 (Zhuì Héng)** — the independent verification line; model: Claude, Opus series — rechecked every
statement against a referee that assumes none of them, measured the frontier function at $2^{40}$ from
this line's own exhaustive run and walked its extremal start again, proved and checked that no uniform
depth exists, formalized the equivalence, the absence of a uniform depth and the anchored-branch
theorem in Lean, built and drilled the instruments, and wrote this paper, including the proofs as
written out here. The statements are the series'; nothing in them is this line's invention.

**Priority, stated plainly.** No result here is claimed as new mathematics. What is offered as this
line's own is the measurement of the frontier at one size, the refutation of the uniform reading by an
explicit family, and the version of the framework that can be relied on: checked against an independent
referee and formalized where it is universal.

# 9. What is open

1. Whether any integer above 1 anchors an infinite hard branch — which is the conjecture.
2. How $K(N)$ grows with $N$; one value is measured here, and nothing about its growth (`UNMEASURED`).
3. A formalization of Theorems 2.1 and 3.1 and of the quotient certificate, which are checked here on
   finite ranges only.

# Acknowledgements

We thank Anthropic, whose Claude models the lab's verification and recomputation lines run on, and OpenAI, whose
ChatGPT models the programme's documents were written with. Not every AI model or instance that took part in this work
is named in it — among them instances that the named authors ran as helpers; that an AI is not listed here does not
mean that none took part.

# References

1. Vigleik Angeltveit, *An improved algorithm for checking the Collatz conjecture for all $n < 2^N$*, arXiv:2602.10466 (2026).

## Data and software

- Python Software Foundation, *Python* (CPython), version 3.14.5, https://www.python.org/ — the language of every gate; the version is the one the line's tree records.
- Leonardo de Moura and Sebastian Ullrich, *The Lean 4 Theorem Prover and Programming Language*, in Automated Deduction – CADE 28, Lecture Notes in Computer Science, Springer, 2021, 625–635, doi:10.1007/978-3-030-79876-5_37; the formalization uses the toolchain leanprover/lean4 v4.33.0.
- The mathlib Community, *The Lean Mathematical Library*, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367–381, doi:10.1145/3372885.3373824; arXiv:1910.09336; tag v4.33.0, commit db584cd.

# A. Reproduction

The recheck and the drill are Python with arbitrary-precision integers and exact rationals, standard
library only, no network; each writes a JSON log. The exhaustive run is a Rust engine whose every claim is
cross-checked by an independent Python walk. The formalization is Lean 4 with mathlib, in a private
repository. The line's own tree is not public. Its public projection is, and it is what this paper's
figures can be checked against without trusting the authors:

- **the run-by-run record**, rendered from the tree with a privacy gate on each file:
  <https://amral.evemisslab.com/collatz/recompute/> (and `/en/`);
- **the secondary-verification ledger**, whose numbers are rendered from the line's own results
  file and read back against it before the site ships:
  <https://verify.evemisslab.com/collatz-verification-zhuiheng/>.

The evidence is pinned, not copied: this paper's front matter names the research branch, the
commit and the directory its figures were drawn from, and the checker reads them exactly as they
stood at that commit. The crystallization standard and its checker live in the release repository
beside the paper (`STANDARD.md`, `tools/check_standard.py`).