1 Program overview

This is a blueprint for a full Lean 4 formalization of Terence Tao’s 2019 theorem (arXiv:1909.03562v5) that almost all Collatz orbits attain almost bounded values. The summit is Theorem 1.3: for every \(f:\mathbb {N}\to \mathbb {R}\) with \(f(N)\to \infty \), one has \(\mathrm{Colmin}(N) {\lt} f(N)\) for almost all \(N\) in the sense of logarithmic density, where \(\mathrm{Colmin}(N)\) is the minimum of the Collatz orbit of \(N\). As of this writing the theorem is formalized in no proof assistant, by any route; a Lean proof is a first.

1.1 The spine

The whole argument is a chain of reductions. Read right-to-left, each arrow is “is proved from”:

\[ \underbrace{\text{Thm 1.3}}_{\text{main}} \Longleftarrow \text{Thm 1.6} \Longleftarrow \underbrace{\text{Thm 3.1}}_{\text{quantitative}} \Longleftarrow \underbrace{\text{Prop 1.11}}_{\text{stabilization}} \Longleftarrow \big[\, \text{Prop 1.9} + \text{Prop 1.14}\, \big] \Longleftarrow \underbrace{\text{Prop 1.17}}_{\text{character decay}} \Longleftarrow \text{Prop 7.1} \Longleftarrow \text{Prop 7.3} \Longleftarrow \text{Prop 7.8}. \]

The passage from the analytic main theorem to a purely arithmetic statement about the Syracuse map (the odd-to-odd accelerated Collatz map) happens at Thm 1.6/Thm 3.1 (node 5.1), and drives everything down to a single Fourier-analytic input, the character-sum decay Prop 1.17 (node 7.11). Prop 1.17 is proved in §7 by a renewal-process argument played against the geometry of the “black” set of the phase functions — the deepest part of the paper.

1.2 The three risk kernels

Almost all of the completion risk concentrates in three clusters; everything outside them is standard treadmill fare (counting, harmonic sums, \(\mathbb {Z}/3^n\mathbb {Z}\) arithmetic, PMF calculus).

S3 — the local 2-D bound (Lemma 2.2, node 2.3): Gaussian-type local limit upper bounds for sums of the lattice distributions. Classical analysis; long but self-contained via explicit formulas and exponential tilting (D5).
X3 — the triangle structure (Lemma 7.4, node 7.3): the black set of the phase function is a disjoint union of well-separated triangles. Finite, elementary, delicate case analysis.
X8/X10 — renewal versus triangles (Case 2 and Lemma 7.10, nodes 7.8, 7.10): the paper’s pinnacle. The design decision D6 finitizes the infinite renewal process into an explicit downward recursion \(Q\), turning the stopping-time measure theory into strong inductions over that recursion.

The critical path is \(\text{S3}\to \text{X6}\to \{ \text{X8},\text{X10}\} \to \text{X11}\to \text{C10}\to \text{C9} \to \text{C6}\).

1.3 Global modelling decisions

The Lean development departs from the paper’s presentation in eight deliberate ways (full rationale in BLUEPRINT.md §0); the ones that shape the statements below are:

Probability is discrete. Every random variable is a PMF on a countable type; expectations are tsums and total variation is \(d_{\mathrm{TV}}(p,q)=\sum _a |p(a)-q(a)|\). No measure theory (node 2.1).
\(\mathbb {Z}[1/2]\) is eliminated. The paper’s offset map is replaced by its integer multiple \(\texttt{fnat}\, n\, a = \sum _{m{\lt}n} 3^{n-1-m} 2^{\, a_{[1,m]}}\), so the iteration identity (1.7)\(\times 2^{|a|}\) lives entirely in \(\mathbb {N}\) (node 3.2).
Asymptotics are reified. \(X\ll Y\) becomes \(\exists C{\gt}0,\ X\le C\, Y\); \(\ll _A\) becomes \(\forall A{\gt}0,\exists C{\gt}0\). No IsBigO/filters in load-bearing statements (uniformity in \(n,\xi \) is exactly what filter-\(O\) would hide). This constrains statements only, and does not by itself make a constant effective: a proof may still obtain its witness from a rate-free limit and satisfy D3 while defeating its purpose. Where a constant is meant to be effective the witness must be an explicit term; since Exists is a Prop, an inexplicit one cannot be recovered downstream. See notes/effective-constants.md.
The small constant is a numeral. \(\varepsilon := 10^{-4}\) (candidate; validated per-site).
The infinite renewal process is finitized by the downward recursion \(Q\) (node 7.4) — the single most important de-risking decision.

Throughout, tuples are \(0\)-indexed (\(a:\mathrm{Fin}\, n\to \mathbb {N}\); paper index \(i\) is Lean index \(i-1\)), and \(a_{[1,m]}\) denotes the prefix sum \(\sum _{i{\lt}m} a_i\).