Tao's proof via conditional Riesz products and a two-dimensional renewal process
The argument
Pairing adjacent geometric valuations and conditioning on the pair sums makes the summands of the Syracuse random variable independent, so its characteristic function becomes an average, over a two-dimensional renewal process, of products of factors of modulus at most one, each at most exp(-ε^3) at a "white" lattice point where the relevant phase is not near an integer. Because the "black" points form well-separated triangles and the renewal process, by a monotone induction with the large triangles handled by a separation estimate, meets enough white points, the average is O_A(n^{-A}) uniformly in n and in the frequency; the announced machine-checked formalization of the whole paper follows this same route and corroborates that the inference goes through.
Does it work?
Not yet evaluated.
Premises
- UnassessedNo current assessment. Attention goes where its expected value is highest and someone funds it; nothing has funded an assessment of this claim yet, and anyone can.constitution →Tao's theorem that almost all Collatz orbits attain almost bounded values has a complete, axiom-clean Lean 4 formalization.
Where it is made
Passages where sources make, criticize or mention this argument. They record where it appears, not how strong it is, and none has precedence over another.
No source is recorded as making it.
Earlier ratings
- Sep 17, 2026
The inference goes through: the conditional factorisation, the cosine bound at white points, the triangle structure of the black set, and the three-case monotonicity induction were each followed in the published text and fit together without gaps, and the argument has been refereed and adapted by other authors to generalised Collatz maps. It rests on no named external result beyond standard local limit and Chernoff bounds for random walks, so it does not stand or fall with any other claim in the graph. The announced machine-checked formalization of the paper would, if confirmed, raise this from an accepted to a kernel-checked proof; its current unassessed standing neither adds to nor subtracts from the argument's validity.