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.

Lean proofpassed
Unfinished proof stepsNone
Formal resultAccepted
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.

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.

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

On a deep forest-green field, many deterministic Collatz traces descend from distinct starts. A gently undulating cobalt threshold rises across the scene; most antique-gold minimum nodes lie strictly below it, while widening gold contours evoke logarithmic weighting and a sparse muted set remains above.
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.

Proof architecture

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

9 curated 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 source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.

  1. Many forest-green Collatz trajectories descend to distinct antique-gold minimum beads beneath a broad, gently oscillating cobalt threshold ribbon; widening harmonic contours suggest logarithmic weighting, while a sparse vermilion set remains exceptional.
    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. Forest-green standard Collatz paths approach a central cobalt valuation spine, where antique-gold odd cores emerge and continue as shorter cobalt Syracuse paths; faint powers-of-two geometry remains behind the unbranched trajectories.
    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. An ordered residue lattice feeds cobalt step-height sequences through a narrow comparison screen and into nearly aligned antique-gold distributions, with a small vermilion spill indicating controlled approximation error rather than exact equality.
    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. A forest-green renewal tree and repeated return arches feed cobalt character phases arranged on large circular frequency geometry; the oscillations cancel into a narrow stream ending at one antique-gold residual bead.
    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. A circular family of forest-green frequency spokes narrows into layered cobalt oscillations passing through translucent residue-fiber planes, then emerges as evenly spaced antique-gold horizontal fibers with only faint remaining variation.
    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. Repeated green valuation staircases feed a descending cobalt first-passage trajectory toward a gold threshold ring, while two broad green and cobalt source-window distributions narrow through matched gold checkpoints into closely aligned passage profiles.
    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. A descending chain of progressively smaller circular source scales carries braided cobalt and forest-green traces toward a deep-green threshold basin; an antique-gold decay envelope at the lower left shrinks as the multiscale chain advances.
    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. Cobalt towers of powers-of-two layers collapse through an antique-gold odd-part spine, then expand into many forest-green standard Collatz trajectories; a translucent gold accounting band crosses the family while only sparse vermilion strands remain bad.
    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. Many forest-green orbit traces fan from a shared scale construction toward distinct antique-gold minimum beads, while a thick cobalt threshold ribbon oscillates but rises across the top and sparse vermilion exception traces fade between successive finite thresholds.
    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

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

Result boundary

What this page 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.

Continue the mathematics

Start from the complete checked source

The pinned theorem and its complete local import closure let internal and external agents inspect the proof, compare an alternate route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks every proposed extension against its exact formal statement.

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

Checked source + agent continuation package · 397 Lean files · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Formal-result publication and review details

Independent publication review

The formal theorem's publication gates are accepted

Lean checks the proof. Independent AI review separately accepted evidence completeness, statement alignment, result boundary, and the retained theorem wording. Those gates apply to the formal result; generated media is reviewed and promoted separately. Neither review replaces Lean's proof check or broadens the theorem.

01

Formal evidence

Independent 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

Independent 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 in a new tab