Number theory · Formalized mathematics
For every fixed \(0<\delta<0.251245530155874\ldots\), almost every integer's Collatz orbit falls below \(\exp\!\left((\log n)^{1-\delta}\right)\) — with the principal theorem chain formalized in Lean 4.
A later, independent paper supersedes this range. Polylogarithmic Descent for Almost All Collatz Orbits in Natural Density reaches a polylogarithmic target by a different first-passage architecture, and extends the stretched-logarithmic range below to every \(0<\delta<1\). This page records the earlier result as published.
The Collatz conjecture asks for termination of every orbit. This paper asks a different quantitative question: how far down can one force the orbit for most starting integers, where “most” is measured by ordinary counting? A natural-density-one result permits exceptions, but requires their proportion among the first \(X\) integers to vanish as \(X\) grows. That distinction turns typical descent into a precise asymptotic statement without pretending to settle any exceptional orbit. Here the certified landing scale is prescribed in advance and is eventually smaller than every fixed power of the starting value, with both an exceptional-count rate and a logarithmic witnessing time.
Work with the shortcut map, which halves even numbers and takes one combined step on odd ones:
\[ T(n)=\begin{cases} n/2, & n\equiv 0 \pmod 2,\\[2pt] (3n+1)/2, & n\equiv 1 \pmod 2,\end{cases} \qquad T_{\min}(n)=\min_{k\ge 0}T^k(n). \]Put \(\delta_0=\log(1/a_0)/\log(2/a_0) =0.251245530155874\ldots\), where \(a_0=(\log_2 3)/2\). For every fixed \(0<\delta<\delta_0\),
\[ T_{\min}(n)\;\le\;\exp\!\left((\log n)^{1-\delta}\right) \]on a set of natural density one.
The endpoint \(\delta_0\) is a supremum of the strict parameter ranges used in the proof; equality at \(\delta=\delta_0\) is not claimed.
For every fixed \(0<\delta<\delta_0\) and every \(0<\sigma<1-\delta/\delta_0\),
\[ \#\left\{n\le X: T_{\min}(n)>\exp\!\left((\log n)^{1-\delta}\right)\right\} \;\le\; 5X\exp\!\left(-c_{\delta,\sigma}(\log X)^{\sigma}\right) \]for all sufficiently large \(X\).
There is a natural-density-one set on which every sufficiently large \(n\) reaches the threshold at some step
\[ 0\le k < 6.953\log n, \]with \(T^k(n)\le\exp((\log n)^{1-\delta})\).
What this does not do. These are almost-all statements in natural density. They do not prove the Collatz conjecture, do not establish descent for every initial value, and do not exclude exceptional cycles or divergent trajectories. They are compatible with arbitrarily long individual exceptional orbits.
Elementary foundations
Four elementary ideas carry most of the notation. Keeping them separate makes it easier to see where dynamics ends and counting begins.
Starting from \(n\), the orbit is \(n,T(n),T^2(n),\ldots\). Its smallest attained value is \(T_{\min}(n)=\min_{k\ge0}T^k(n)\). A witness is one particular time \(k\) at which the desired threshold is reached.
Used for: separating “the orbit eventually gets low” from “every intermediate iterate is controlled.”
Each shortcut step records one bit: even or odd. For a block of \(m\) steps, the first \(m\) parities are determined by the starting residue modulo \(2^m\); over a complete residue system, every parity word occurs once.
Used for: replacing one block of dynamics by finite arithmetic on the Boolean cube.
A set \(A\subseteq\mathbb N\) has natural density one when \[ \frac{\#(A\cap[1,X])}{X}\longrightarrow1. \] It may still omit infinitely many integers; their relative frequency must vanish.
Used for: stating an almost-all theorem without turning it into a pointwise claim.
The target can be rewritten as \[ \exp((\log n)^{1-\delta}) =n^{(\log n)^{-\delta}}. \] For fixed \(\delta>0\), the effective exponent tends to zero, so this scale eventually lies below every fixed power \(n^\varepsilon\).
Used for: reading the theorem as a genuinely sub-power descent statement.
Logical separation. The parity-word description is exact finite combinatorics. Natural density and the exceptional-count estimate are asymptotic statements. The orbit plots later on the page are finite illustrations, not a bridge between those two scopes.
Literature ladder
On the ordinary-natural-density line, the certified landing target has become progressively smaller. The comparison below holds the density notion and shortcut map fixed, so the mathematical gain is visible.
| Work | Density-one conclusion | What changes |
|---|---|---|
| Terras (1976) | For almost every \(n\), some iterate satisfies \(T^k(n)<n\). | Establishes density-one finite stopping below the starting value; the parity-word periodicity behind dyadic counting is also classical in this work. |
| Korec (1994) | For every fixed \(\theta>\log_4 3=0.79248125\ldots\), almost every \(n\) reaches below \(n^\theta\). | Replaces the starting-value target by a nontrivial fixed power. |
| Inselmann (2024) | For every fixed \(\theta>0\), almost every \(n\) reaches below \(n^\theta\), within \(6.952\ldots\log n\) steps. | Extends the fixed-power conclusion to every positive exponent. |
| This paper (2026) | For every fixed \(0<\delta<\delta_0\), almost every \(n\) reaches below \(n^{(\log n)^{-\delta}}\). | The exponent now tends to zero with \(n\), with a quantified exceptional count and a witness before \(6.953\log n\). |
The outcome. Inselmann allows any fixed horizontal exponent \(\theta>0\). This paper supplies one descending exponent, \((\log n)^{-\delta}\to0\), so its target eventually lies below every fixed power. It remains an almost-all theorem, not a proof of the Collatz conjecture.
This ladder is deliberately restricted to ordinary natural density. Tao's logarithmic-density theorem and concurrent natural-density preprints use different threshold or quantifier classes; the article discusses them separately rather than imposing a single total ranking.
The dependency spine
The argument first understands one logarithmic block, then turns that local information into a transport estimate, and only afterward iterates endpoints. Read the six nodes from left to right.
The key design choice: the consumer is an orbit minimum, so the recursion transports endpoint events. It does not ask for a uniform envelope on every iterate inside every block.
Guided proof lab
Open a stage to inspect its input, mathematical burden, and output. The output of each panel is the input consumed by the next one.
Input: a dyadic shell→Output: an explicit endpoint map on parity words
A dyadic shell contains exactly one representative of every parity word of the matching length. The affine iterate formula then writes the endpoint of one logarithmic block explicitly in terms of that word, converting the dynamical question into finite arithmetic on a complete Boolean cube.
Input: a parity word→Output: a fixed-total composition and a congruence
Fixing the number of odd steps separates the main multiplicative factor from the affine correction. The remaining parity data become a positive composition of a fixed total, and equality of two block endpoints becomes a congruence condition modulo the corresponding power of \(3\).
Input: endpoint fibers→Output: a Rényi-moment bound on crowding
Starts sharing an endpoint form a fiber. Integer-lift injectivity and a quotient-order estimate translate crowding in one congruence class into spending near the end of the associated composition. A fixed-total Rényi estimate controls the resulting \((1+\theta)\)-moment near the mean part count.
Input: target density plus fiber moments→Output: one-block density transport
Endpoint fibers are split into ordinary and heavy classes using an exponential multiplicity threshold. The target's density estimate bounds the ordinary contribution, while the Rényi moment bounds the heavy one. Balancing their decay rates yields the asymptotically linear transport slope \(\Lambda(\theta)\).
Input: one-block transport and contraction→Output: a recursive endpoint descent
A binomial-tail estimate supplies a fixed dense set on which one logarithmic block contracts \(n\) to at most \(3n^r\) for any fixed \(r>a_0\). The recursion pulls back this endpoint event only; it does not impose a stronger pathwise envelope inside each block.
Input: the endpoint recursion→Output: \(\delta_0\), the rate, and the clock
Taking \(R\asymp\log\log n\) blocks makes the endpoint scale \(n^{r^R}\). Summability of the propagated exceptional sets imposes two strict scalar bounds. Finally, letting \(r\downarrow a_0\) and \(\theta\uparrow1\) produces the nonattained endpoint \(\delta_0\), together with the exceptional rate and clock.
Endpoint control is deliberate: the public theorem concerns an orbit minimum, so it does not need a uniform bound on every intermediate iterate inside each logarithmic block.
Graduate study lab
The theorem has an order: first fix an interior descent exponent \(\delta\), then choose an admissible exceptional-set exponent \(\sigma\), and only then let the counting cutoff \(X\) grow. Move the controls to see which conclusions travel together and where the strict endpoint enters.
Model a very large input as \(n=10^D\). The slider controls \(\log_{10}D\), so each step changes the input length by an order of magnitude.
Boundary discipline. The controls stop below \(\delta_0=0.251245530155874\ldots\), because equality is not claimed. The paper proves existence of an effective constant and a sufficiently-large onset; this calculator does not invent numerical values for either one.
The literature ladder above isolates the fixed-power progression: Korec reached exponents above \(\log_4 3\), and Inselmann later reached every fixed positive exponent. Each application still chooses a horizontal power \(n^\varepsilon\) before \(n\) grows. The public theorem instead prescribes a single scale whose effective exponent tends to zero. That is the relevant comparison: not a new constant-power exponent, but a quantified rate at which the exponent itself decays. The article also tracks the counting-cutoff error; these are separate axes, not a claim that it dominates every recent Collatz result.
Counting digits makes the gap concrete. The theorem certifies an orbit value with at most \(1+(\log n)^{1-\delta}/\log 10\) decimal digits, while \(n\) itself has \(\asymp \log n\) digits — so the certified digit ratio tends to zero. A fixed-power bound \(n^{\alpha}\) only ever shrinks the digit count by the constant factor \(\alpha\).
The cleanest way to see it is to write the threshold as a power of \(n\). Since \(\exp\!\left((\log n)^{1-\delta}\right)=n^{\varepsilon(n)}\) with
\[ \varepsilon(n)=(\log n)^{-\delta}\;\longrightarrow\;0, \]the threshold is a power of \(n\) whose exponent decays. A fixed power is a horizontal line, and the decaying exponent eventually passes under every one of them — which is precisely the claim.
The preset black curve is the actual shortcut orbit of \(n=1{,}234{,}567\); the dashed line is the geometric trend suggested by a typical balance of odd and even steps, and the green line is the stretched-logarithmic target. Change \(n\) or \(\delta\) below, then compare the first target crossing with the theorem's displayed clock. A single orbit only illustrates the definitions: the theorem is an asymptotic statement about a density-one population and does not assert a pointwise envelope for each starting value.
n = 1,234,567 · δ = 0.15 · witness k* = 29 · clock bound ≈ 97.5
Theorem 1.1, part 2, gives a witness before \(6.953\log n\) steps on a density-one set of sufficiently large \(n\). Sampling 2,000 odd starting values across the dyadic shell \([2^{26},2^{27})\), — land inside the clock, with a median witness at — of the bound.
There is no tension between the theorem and a small value that misses the displayed clock. Its quantifiers say that, after fixing \(\delta\), there is a density-one set \(A_\delta\) whose sufficiently large members have a witness; they do not say that every integer, or every small integer, belongs to that set. A record-holder may therefore lie outside \(A_\delta\) or before the unspecified onset. Conversely, the high hit rate in this finite shell does not verify the asymptotic theorem. The table is a calibration of the literal map, target, and clock, not evidence for the limiting density claim.
Reproduce it. The preset data in this table and all four
figures are produced by
scripts/make_figure_data.py, which iterates the map
directly. A custom orbit entered above is computed locally in the
browser using the same shortcut map.
A set \(A\) of positive integers has natural density one when the fraction \(\#(A\cap[1,X])/X\) tends to \(1\), or equivalently when the fraction of exceptions tends to zero. Thus “most integers” is a limit of ordinary finite counts, not a probability assigned to an individual orbit. The definition allows infinitely many exceptions, even with irregular clustering, provided their relative frequency vanishes. The traces below offer a finite visual analogy: individual running minima remain ragged, while the theorem concerns the population as the counting scale tends to infinity. The sample itself proves no density statement.
Theorem 1.1 gives more than density zero, which by itself says only that the exceptional fraction is \(o(1)\) and supplies no rate. A power-law saving in \(X\) would decay exponentially in \(\log X\). The proved fraction \(\exp(-c(\log X)^\sigma)\) sits strictly between those scales: it is faster than every fixed negative power of \(\log X\), but slower than every fixed negative power of \(X\). The constant \(c_{\delta,\sigma}\) is an effective but unoptimized proof constant, not an empirical fit. The normalized curve below shows only the shape of the stated rate, not its actual onset or vertical placement.
The public Lean artifact verifies the principal theorem chain, not merely a companion result. Three referee-facing declarations match the descent statement, the optimized exceptional-count estimate, and the logarithmic-time witness in the public article. At the one-block seed, the formal proof uses a stronger all-prefix estimate than the terminal consequence used in the written proof; the final public conclusions are the same. This is not a line-by-line certification of the article's English exposition, literature discussion, or motivation. It is a kernel check that the encoded conclusions follow from the encoded definitions and formal lemmas, with a declaration-level dependency report exposing that chain.
The development is pinned to Lean v4.15.0 and a fixed
Mathlib revision. Its paper-facing axiom audit reports only
propext, Classical.choice, and
Quot.sound, with no sorry or project-local
axioms. These checks supplement the self-contained manuscript proof;
the manuscript does not use the build as a missing proof step.
Cite the concept DOI 10.5281/zenodo.21825993 to always
resolve to the newest version, or the version DOI below to pin v2.0.2.
@misc{shaik2026collatz,
author = {Shaik, Idris Ali},
title = {Quantitative {C}ollatz Descent to Stretched-Logarithmic
Scale in Natural Density, with a {L}ean 4 Formalization},
year = {2026},
publisher = {Zenodo},
version = {2.0.2},
doi = {10.5281/zenodo.21851173},
url = {https://doi.org/10.5281/zenodo.21851173}
}