ProofAtlas

Number theory · dynamical systems · formal theorem

Tao’s Almost-Bounded Collatz Orbits

For every real-valued threshold function f on ℕ that tends to infinity, the positive starting values N whose standard Collatz orbit minimum is strictly below f(N) have logarithmic density one.

Scope: For every real-valued threshold function f on ℕ that tends to infinity, the positive starting values N whose standard Collatz orbit minimum is strictly below f(N) have logarithmic density one.

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Almost-bounded-orbits statement mapEvery real threshold function tending to infinity is eventually beaten by the orbit minimum for a logarithmic-density-one set of positive starting values.
Exact scope: For every real-valued threshold function f on ℕ that tends to infinity, the positive starting values N whose standard Collatz orbit minimum is strictly below f(N) have logarithmic density one.

Exact formal proposition

Hypotheses and conclusion

This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.

def TaoAlmostBoundedColMinStatement : Prop :=
  ∀ f : ℕ → ℝ,
    GrowsToInfinity f →
      HasLogDensity {N : ℕ | 0 < N ∧ (collatzOrbitMin N : ℝ) < f N} 1
Definitions used in this proposition

GrowsToInfinity

def GrowsToInfinity (f : ℕ → ℝ) : Prop :=
  Tendsto f atTop atTop

HasLogDensity

def HasLogDensity (s : Set ℕ) (d : ℝ) : Prop :=
  Tendsto (fun N : ℕ => logCountingRatio s N) atTop (nhds d)

collatzOrbitMin

noncomputable def collatzOrbitMin (N : ℕ) : ℕ :=
  sInf (collatzOrbitValues N)
Lean wrapper declaration

The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.

theorem taoAlmostBoundedColMin_checked : TaoAlmostBoundedColMinStatement
Open main Lean file

Proof route

From odd Syracuse dynamics to Tao's almost-bounded theorem

9 proof stages

The checked proof passes through nine distinct movements: it fixes the logarithmic-density endpoint, compresses standard Collatz dynamics to the odd Syracuse map, controls valuation laws, obtains primitive Fourier decay and fine-scale mixing, stabilizes first-passage distributions, shrinks the odd bad set across many scales, lifts the estimate back to every positive start, and finally lets fixed thresholds follow an arbitrary diverging function.

These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.

  1. Scientific figure illustrating: For every real threshold f that tends to infinity, the positive starts with collatzOrbitMin N strictly below f(N) have logarithmic density one.
    For every real threshold f that tends to infinity, the positive starts with collatzOrbitMin N strictly below f(N) have logarithmic density one.
    01

    What Tao's theorem actually says

    ∀ f : ℕ → ℝ, GrowsToInfinity f → HasLogDensity {N : ℕ | 0 < N ∧ (collatzOrbitMin N : ℝ) < f N} 1

    The proof begins by fixing the exact endpoint: varied orbit minima lie below a diverging but not necessarily monotone threshold for logarithmic-density-one many positive starts. It neither sends every trajectory to one nor asserts universal convergence.

    Lean lemmas for this step
    • GrowsToInfinity
    • TaoAlmostBoundedStatement
    • collatzOrbitValues
    • collatzOrbitMin
    • TaoAlmostBoundedColMinStatement
    • TaoAlmostBoundedStatement_iff_colMin
  2. Scientific figure illustrating: Every positive start factors into a power of two times an odd core, and each Syracuse iterate of that core is reached along the original standard Collatz orbit.
    Every positive start factors into a power of two times an odd core, and each Syracuse iterate of that core is reached along the original standard Collatz orbit.
    02

    Strip powers of two and follow the odd dynamics

    N = 2^a · M with Odd M; every (syracuse^[k]) M is reached by the standard Collatz orbit of N

    The proof separates the deterministic standard dynamics from the compressed odd dynamics used by the analytic argument. Removing powers of two exposes odd cores, and one Syracuse movement represents a block of ordinary Collatz steps. No probability estimate has entered yet.

    Lean lemmas for this step
    • collatzStep
    • syracuse
    • reaches_powTwo_mul
    • reaches_syracuse_iterate
    • positiveCollatzBad_oddPart_cover
  3. Scientific figure illustrating: On the recorded logarithmic odd windows, the actual Syracuse valuation-list law is close in full L1 distance to independent positive Geom(2) increments, with an exponentially decaying checked error.
    On the recorded logarithmic odd windows, the actual Syracuse valuation-list law is close in full L1 distance to independent positive Geom(2) increments, with an exponentially decaying checked error.
    03

    Valuations approach an ideal geometric law

    taoProp19ValuationTV μ n ≤ C₁ · 2^(−c₁ n) under the recorded scale and source-residue hypotheses

    Residue decoding and strict truncation turn actual Syracuse step valuations into finite lists that can be compared with the ideal geometric product law. The small separated residual is essential: Proposition 1.9 proves quantitative approximation under its scale and source-law hypotheses, not exact independence.

    Lean lemmas for this step
    • truncateValuationList
    • taoCanonicalUniformOddResiduePMF
    • taoProp19SourceResidueLaw_map_decoder
    • taoProp19ValuationTV_le_sourceTV_add_two_overflow
    • taoProp19CanonicalApproximationWithConstants_checked
    • taoProp19ValuationApproximationStatement_checked
  4. Scientific figure illustrating: The checked Section 7 renewal and finite-Fourier route gives polynomial decay for every primitive frequency of the Syracuse distribution.
    The checked Section 7 renewal and finite-Fourier route gives polynomial decay for every primitive frequency of the Syracuse distribution.
    04

    Renewal structure forces character decay

    ∀ A : ℕ, 0 < A → ∃ C ≥ 0, ‖DFT(syracPMF n)(ξ)‖ ≤ C / n^A for primitive ξ modulo 3^n

    Renewal packets are paired and transported through the checked Section 7 assembly. Their oscillating character contributions cancel across primitive modes, leaving a polynomially small Fourier coefficient. This is the formal route retained in the checked source.

    Lean lemmas for this step
    • taoProp117PrimitivePolynomialDecay
    • TaoProp117PrimitivePolynomialDecayStatement
    • syracPMFPrimitiveDFTBound
    • syracPMFPrimitivePolynomialDecayAt
  5. Scientific figure illustrating: Primitive-frequency decay and the checked Section 6 fiber decomposition suppress fine-scale residue oscillation at each positive natural exponent; the downstream route specializes this at exponent one.
    Primitive-frequency decay and the checked Section 6 fiber decomposition suppress fine-scale residue oscillation at each positive natural exponent; the downstream route specializes this at exponent one.
    05

    Character decay yields fine-scale mixing

    ∀ A : ℕ, 0 < A → ∃ C ≥ 0, 1 ≤ m ≤ n → syracFineScaleOscillation m n ≤ C / m^A

    Section 7 controls the primitive modes, while the remaining lower-frequency modes recurse through the source-fiber decomposition. Together they give polynomial fine-scale mixing across every pair of scales permitted by the formalized hypotheses and pass the exponent-one case to the downstream route.

    Lean lemmas for this step
    • taoProp117PrimitivePolynomialDecay
    • taoProp114FineScaleMixing
    • syracFineScaleMixingAt
    • TaoProp114FineScaleMixingStatement
  6. Scientific figure illustrating: Valuation control, deterministic descent, and fine-scale mixing stabilize the no-hit and first-passage laws across Tao's paired source windows.
    Valuation control, deterministic descent, and fine-scale mixing stabilize the no-hit and first-passage laws across Tao's paired source windows.
    06

    Mixing stabilizes first-passage laws

    noHitErr(B) ≤ C · B^(−c) and passTVErr(B) ≤ C · (log B)^(−c) along the checked paired-window route

    The checked Section 5 route compares two logarithmic source windows. Actual valuation control and mixing make their first-passage distributions close, while deterministic descent identifies the threshold event. This is the rate-bearing first-passage endpoint, not yet the density theorem.

    Lean lemmas for this step
    • taoSection5CanonicalPairNoHitRateStatement_checked
    • taoSection5CanonicalPairPassTVRateStatement_checked
    • taoProp111ConcreteFirstPassageStabilizationRate_checked
    • taoProp111RealFirstPassageStabilizationRate_checked
  7. Scientific figure illustrating: A bounded trace and geometric error budget combine across descending scales to give a polynomially small logarithmic mass for odd starts that miss a fixed Syracuse threshold.
    A bounded trace and geometric error budget combine across descending scales to give a polynomially small logarithmic mass for odd starts that miss a fixed Syracuse threshold.
    07

    Iterate scales to shrink the odd bad set

    logCount {N | Odd N ∧ ¬ syracuseHitsAtMost N B} X ≤ D · (log B)^(−c) · logCount {N | Odd N} X

    Each active source scale supplies a controlled first-passage contribution. The checked Section 3 construction arranges those windows into a finite cover and pays for their errors with a geometric budget, yielding a uniform all-prefix bound for the odd bad set.

    Lean lemmas for this step
    • taoProp111RealFirstPassageStabilizationRate_checked
    • exists_taoSection3AmbientBoundedTrace_checked
    • exists_taoSection3AmbientGeometricBudget_checked
    • exists_taoSection3UniformOddBadMass_checked
  8. Scientific figure illustrating: The exact two-adic decomposition transfers the odd Syracuse bad-set estimate to all positive standard Collatz starts without losing the logarithmic-mass rate.
    The exact two-adic decomposition transfers the odd Syracuse bad-set estimate to all positive standard Collatz starts without losing the logarithmic-mass rate.
    08

    Lift the bound back to standard Collatz

    logCount (positiveCollatzBad B) X ≤ D · (log B)^(−c) · logMass X

    Every positive start is written as a power of two times an odd factor. A Syracuse threshold hit from that odd factor is reached along the original standard Collatz orbit, and the finite two-adic mass identity controls the union of all lifted layers.

    Lean lemmas for this step
    • collatzHitsAtMost_powTwo_mul_of_syracuseHitsAtMost
    • positiveCollatzBad_oddPart_cover
    • logCount_le_logMass_of_oddPart_cover
    • exists_taoSection3UniformStandardBadMass_checked
  9. Scientific figure illustrating: Vanishing fixed-threshold errors and the eventual growth of any diverging f yield the strict orbit-minimum statement in logarithmic density.
    Vanishing fixed-threshold errors and the eventual growth of any diverging f yield the strict orbit-minimum statement in logarithmic density.
    09

    Let finite thresholds follow any diverging function

    ∀ f : ℕ → ℝ, GrowsToInfinity f → HasLogDensity {N : ℕ | 0 < N ∧ (collatzOrbitMin N : ℝ) < f N} 1

    The standard bad-set estimate is complemented to obtain good-set lower bounds for fixed thresholds. Thresholds are then chosen with errors tending to zero; because f tends to infinity, the corresponding good sets eventually lie inside the hit-below-f set, which is exactly the strict orbit-minimum event.

    Lean lemmas for this step
    • logCount_positiveCollatzBad_eq_sub
    • thresholdLowerBoundHypothesis_of_allPrefix_positiveBad
    • exists_taoThresholdLowerBound_checked
    • taoAlmostBounded_of_thresholdLowerBound
    • taoAlmostBounded_checked
    • collatzHitsBelowReal_iff_collatzOrbitMin_lt
    • TaoAlmostBoundedStatement_iff_colMin
    • taoAlmostBoundedColMin_checked

The theorem at a glance

Tao's almost-bounded orbits at a glance

Ivory editorial poster for Tao's almost-bounded Collatz theorem, with a large logarithmic-density-one statement, the exact orbit-minimum set, an engraved field of descending Collatz traces beneath a rising threshold, four proof-architecture steps, and a red exact-scope footer.
Tao's theorem says that, for every diverging f, the starts whose Collatz orbit minimum falls strictly below f(N) have logarithmic density one.

Accessible transcript

{N > 0 | (collatzOrbitMin N : ℝ) < f(N)} has logarithmic density 1

The checked route passes from standard Collatz dynamics to odd Syracuse dynamics, establishes quantitative distribution and mixing estimates, controls fixed-threshold bad sets across scales, and transfers the result back to standard starts. It proves logarithmic-density-one strict orbit minima below every diverging threshold, not natural density, a uniform rate, ReachesOne, or the full Collatz conjecture.

Read the complete poster transcript

DYNAMICAL SYSTEMS · LOGARITHMIC DENSITY

TAO’S ALMOST-BOUNDED COLLATZ ORBITS

f(N) → +∞

ALMOST EVERY ORBIT FALLS BELOW ITS OWN DIVERGING THRESHOLD

FOR EVERY f : ℕ → ℝ WITH f(N) → +∞

LOGARITHMIC DENSITY 1

{N > 0 | (collatzOrbitMin N : ℝ) < f(N)}

Logarithmic density weights N by 1/N before taking the limiting proportion.

HOW THE PROOF MOVES

1 · CONTROL SYRACUSE BAD SETS

A polynomial logarithmic-mass bound shrinks with the threshold.

2 · RETURN TO STANDARD COLLATZ

Odd parts and powers of two transfer the bound to every positive start.

3 · ASSEMBLE FIXED THRESHOLDS

Vanishing errors give density one for each growing threshold family.

4 · PASS TO THE ORBIT MINIMUM

A hit below f(N) is equivalent to collatzOrbitMin N < f(N).

EXACT SCOPE

Logarithmic density and strict < for every diverging f. Not natural density.

Not a uniform rate in f. Not ReachesOne. Not the full Collatz conjecture.

Theorem schematic

Orbit minima below a diverging threshold

Scientific figure illustrating: For every diverging threshold f, logarithmically almost every positive N has collatzOrbitMin N < f(N).
For every diverging threshold f, logarithmically almost every positive N has collatzOrbitMin N < f(N).

For every f : ℕ → ℝ tending to +∞, {N > 0 | (collatzOrbitMin N : ℝ) < f(N)} has logarithmic density 1

For every real-valued f that tends to infinity, the positive starts N whose standard Collatz orbit has some value strictly below f(N) form a set of logarithmic density one. The threshold need not be monotone, and the conclusion neither gives natural density one nor says every orbit reaches a common endpoint.

Result boundary

What this theorem does—and does not—establish

For every real-valued threshold function f on ℕ that tends to infinity, the positive starting values N whose standard Collatz orbit minimum is strictly below f(N) have logarithmic density one.

About these visual explanations

These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

Continue the mathematics

Open questions and extensions

The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.

What the source ZIP contains

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.

Complete checked Lean source · 397 Lean files · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Publication review

Review record

Publication reviews accepted

Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.

01

Formal evidence

The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.

02

Statement alignment

The formal declaration was accepted against the named theorem and its exact variant.

03

Result boundary

The accepted boundary keeps nearby stronger or commonly confused claims out of scope.

04

Public wording

The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.

05

Canonical source

The first-party source link is pinned to the checked package commit and exact Lean file.

06

Accepted result

A validated accepted-result record binds the four reviews to the checked formalization.

Expanded visual

Open original image