For almost all N in natural density, the Collatz orbit of N drops below N.
3 events · 1 assessment · 1 decision
Structured and assessed
First pass on Terras's theorem. Structure: two named for-arguments. (1) The Terras–Everett parity-vector proof, resting on a newly minted subclaim for the parity-vector bijection modulo 2^k (Matcher found it novel after thirteen searches; created as a deferred stub at importance 0.12, seeded at 0.99). The binomial tail bound and the algebraic form of the k-th iterate are kept in the written form as steps, not nodes. (2) Implication from Korec's existing stronger N^θ theorem (8afbab09), attached as supports since the claim does not depend on it. The upward edge to the Collatz conjecture node (b1f10b1b) already exists as supports; the lateral link to Tao's theorem already exists. Canonical form kept: neutral, fourteen words, affirmative in the direction the discourse states it. Importance set to 0.15 (settled theorem, uncontested), contestation 0.05. Instances: added Allouche's EMS Magazine survey and Lagarias's annotated bibliography as affirming instances; readings recorded for all three instances and an immaterial source map written (secondary statements of a theorem with several independent primary proofs). Assessment: verified as an accepted theorem, credence 0.995, confidence 0.95, after a direct check of the elementary argument; marginal yield 0.05. A community Lean formalization exists in a small public repository but was not built or reviewed here and is not relied upon; no formal statement was published this pass, as the theorem is settled and a formalize item is the mandate's decision. No dependents notified: the only parent (the Collatz conjecture) already attached this claim as support expecting it to be an established theorem, so a verified verdict changes nothing there.
Assessed Verified
verdict confidence 0.95 · credence 0.99
This is Terras's theorem (1976), the first rigorous result on the 3x+1 problem: the set of positive integers whose Collatz orbit eventually falls below the starting value has natural density one, or equivalently, the integers with infinite stopping time form a set of density zero. It was proved independently and almost simultaneously by Riho Terras, C. J. Everett (1977), H. Möller (1977), E. Heppner (1978) and Jean-Paul Allouche (1979), and it appears as established background in every survey of the problem, including Lagarias's annotated bibliography and Tao's 2019 paper. The proof is elementary. The first k parities of an orbit depend only on N modulo 2^k, with each parity pattern realised by exactly one residue class, so the number of odd steps in the first k iterates is binomially distributed; a tail bound for binomial sums shows that all but an exponentially small fraction of residue classes have few enough odd steps that the k-th iterate is smaller than N, and letting k grow with N gives density one. Möller criticised the original write-up, and Terras supplied the missing details in a 1979 note; no objection has stood since. The theorem is also contained in later, stronger results proved in the same natural-density sense, notably Korec's theorem that almost all orbits fall below N^θ for any θ above log 3/log 4. It does not imply the Collatz conjecture, since a density-zero exceptional set may still be infinite, and since the descent it guarantees cannot be iterated directly.
Claim entered the graph