ProofAtlas

Number theory · dynamical systems · formal theorem

Natural-Density Almost-Bounded Collatz Orbits in Logarithmic Time

For thresholds tending to infinity along odd inputs, odd-relative-density-one many odd starts descend within 145 · log N Syracuse steps; for thresholds tending to infinity on all positive inputs, ordinary-natural-density-one many positive starts descend within 436 · log N raw Collatz steps.

Lean proofpassed
Unfinished proof stepsNone
Formal resultAccepted

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

Two logarithmic-time density conclusions at a glance

Ivory editorial poster separating an odd-relative-density Syracuse result for odd starts from an ordinary-natural-density raw Collatz result for positive starts, with exact clocks and four proof movements.
One checked package gives an odd-relative Syracuse theorem and a separate ordinary-density raw Collatz theorem with explicit logarithmic clocks.

Accessible transcript

C_syr = 501501/(5000 log 2) < 145; C_coll = 1509503/(5000 log 2) < 436; d = 6993/200000 < 5/143

The proof uses a global power-law phase gap and fixed quantitative rate, turns fixed-target control into an odd-relative Syracuse conclusion, then uses the two-adic lift to obtain the ordinary-density raw Collatz conclusion.

Read the complete poster transcript

NUMBER THEORY · NATURAL DENSITY · COLLATZ DYNAMICS

COLLATZ DESCENT IN LOGARITHMIC TIME

TWO CLOCKS · TWO PRECISE DENSITY DOMAINS

ODD SYRACUSE RESULT

FOR EVERY f GROWING ALONG ODD INPUTS

ODD-RELATIVE NATURAL DENSITY 1

N ODD

∃ m ≤ C_syr · log N

Syracuse^m(N) < f(N)

C_syr = 501501/(5000 log 2) < 145

odd-to-odd steps

RAW COLLATZ RESULT

FOR EVERY f GROWING ON ALL POSITIVE INPUTS

ORDINARY NATURAL DENSITY 1

N > 0

∃ m ≤ C_coll · log N

Collatz^m(N) < f(N)

C_coll = 1509503/(5000 log 2) < 436

individual Collatz steps

ODD CORE ROUTE

WRITE N = 2^a M WITH M ODD, a ≥ 0

RAW COLLATZ ROUTE

Factoring out powers of two lifts the odd-core descent to a raw Collatz descent.

HOW THE PROOF MOVES

1 · RHIN PHASE GAP

A global power-law gap separates arithmetic phases.

2 · QUANTITATIVE RATE

Scheduled passages retain one fixed exponent.

3 · GROWING THRESHOLD

A diverging threshold absorbs a fixed target.

4 · TWO-ADIC LIFT

Odd cores and powers of two produce the raw result.

d = 6993/200000 = 0.034965 < 5/143

EXACT SCOPE

Odd-relative density for the Syracuse clause; ordinary natural density for the raw Collatz clause. A density-zero exceptional set may remain. Not every orbit. Not arrival at 1. f need not be monotone. No uniform convergence rate in f.

Theorem schematic

Two density domains within two logarithmic clocks

Many green deterministic trajectories cross below a gently oscillating cobalt threshold at varied gold hit rings beneath nested clock arcs; adjacent text distinguishes the odd-relative Syracuse population from the ordinary-density raw Collatz population.
The Syracuse endpoint uses odd-relative density among odd starts; the raw Collatz endpoint uses ordinary density among positive starts.

odd-relative density(Syracuse hit) = 1 with C_syr < 145; ordinary density(raw Collatz hit) = 1 with C_coll < 436

For thresholds growing along odd inputs, odd-relative-density-one many odd starts have a Syracuse hit before 145 · log N odd-to-odd steps. For thresholds growing on all positive inputs, ordinary-natural-density-one many positive starts have a raw Collatz hit before 436 · log N individual steps.

Proof architecture

From a Diophantine phase gap to natural-density logarithmic-time descent

8 curated stages

The checked route has eight movements: it fixes the distinct odd-relative and ordinary natural-density endpoints, obtains a global Rhin phase gap, uses that gap to control scheduled passages, telescopes the local estimates at one fixed exponent, proves fixed-target odd-start descent, lets a diverging threshold absorb a target chosen for any density tolerance, lifts the result through powers of two to raw Collatz time, and assembles the exact public constants.

These source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.

  1. A population of starts sends green trajectories below an oscillating cobalt threshold at varied gold hit rings, with shorter odd and longer raw logarithmic clock arcs above.
    The Syracuse endpoint uses odd-relative density among odd starts; the raw Collatz endpoint uses ordinary density among positive starts.
    01

    Fix the exact density-one endpoint

    odd-relative density(Syracuse hit) = 1; ordinary density(raw Collatz hit) = 1

    Both endpoints require a strict hit below a threshold that may oscillate while tending to infinity, but they retain different threshold-growth hypotheses, populations, density notions, and clocks.

    Lean lemmas for this step
    • ND16LogTimeStatement
    • ND13LogTimeStatement
    • ndRhinLogTimePaperPackage
  2. Cobalt irrational-rotation samples avoid gold neighborhoods of an integer lattice; a finite inner band joins a large-height outer band while protected widths shrink with scale.
    One positive constant gives a power-law lower bound for the nearest-integer distance of every positive multiple of log₂ 3.
    02

    Rhin's estimate yields a global phase gap

    ∃ c > 0, ∀ q ≥ 1, c · q^(-133/10) ≤ ‖q log₂ 3‖

    Rhin's literal large-height estimate controls all sufficiently large multiples. Finite absorption supplies a positive normalized minimum for the remaining finitely many multiples, yielding one existential global witness.

    Lean lemmas for this step
    • literalRhinLargeHeightBound
    • existsGlobalPhaseBound_of_largeHeightBound
    • existsPhaseGapRhin
  3. Phase-circle samples enter separated resonance gates along a cobalt logarithmic clock while ordered green passage strands traverse the windows and a narrow exceptional stream remains.
    Power-law separation of arithmetic phases prevents near-resonances from accumulating across the logarithmic passage schedule.
    03

    The phase gap controls scheduled passages

    PhaseGap c (143/10) supplies the scheduled-passage separation used by the ND31 rate engine

    The fixed phase-gap witness is converted into deterministic spacing across scheduled windows. That spacing controls the bad passage contribution; it is an arithmetic estimate, not an independence or random-walk assumption.

    Lean lemmas for this step
    • PhaseGap
    • NDM2Bounds
    • ndRhinND31LogTimeBounds_sameD
  4. Overlapping cobalt passage windows transfer green mass along a logarithmic arc while thin errors collect beneath one stable gold envelope that remains strictly below a cap.
    The local passage bounds telescope while preserving the fixed exponent d = 6993/200000, strictly below the phase-gap cap 5/143.
    04

    Telescope passages at one fixed exponent

    d = 6993/200000 = 0.034965 < 5/143

    The proof pays each local error into one quantitative envelope instead of weakening the rate at every stage. The strict cap matters: the checked exponent has reserve and the endpoint is not attained.

    Lean lemmas for this step
    • ndRhinLogTimeRate_sameD
    • ndRhinLogTimeRate_sameD_6993_200000
  5. Equal-width blocks of gold odd starts feed compressed cobalt Syracuse trajectories into one fixed green target basin before a clock ends, leaving a shrinking vermilion slice.
    For each fixed target scale, the quantitative odd-start bad ratio yields odd-relative-density-one logarithmic-time descent among odd starts.
    05

    Obtain fixed-target density-one descent

    oddSyracuseLogTimeBadRatio(N₀, x) ≤ C · (log N₀)^(-d)

    The fixed-target theorem is the rate-bearing bridge from passage estimates to density. It controls the proportion relative to odd starts and keeps the target fixed while the population cutoff grows.

    Lean lemmas for this step
    • ND31LogTimeBounds
    • ndRhinND31LogTimeBounds_sameD
    • ndRhinLogTimeRate_sameD
  6. An ornate target-and-compass dial at left feeds a fan of trajectories into a vertical split; red paths spread above a red boundary while gray paths and sparse gold points continue below a blue horizontal marker.
    For each density tolerance, choose one fixed target with a sufficiently small bad ratio; a diverging threshold eventually lies above that target.
    06

    Let a diverging threshold absorb a fixed target

    ∀ ε > 0, choose B; eventually B < f(N), so fixedTargetGood(B) ⊆ hitBelow(f)

    The target choice may depend on the requested tolerance, while the threshold function is arbitrary apart from tending to infinity. Eventual set inclusion then transfers the fixed-target density estimate without claiming a convergence rate uniform in the threshold.

    Lean lemmas for this step
    • ND16LogTimeStatement
    • nd16LogTimeStatement_of_nd31
    • GrowsToInfinity
  7. Two blue clock faces mark a horizontal timeline. Above it one green trajectory crosses a gold threshold at a ringed hit; below it a fan of green trajectories records many ringed hits between dotted time markers.
    Factoring positive starts into powers of two times odd cores transfers the odd-relative Syracuse theorem to an ordinary-density theorem for all positive starts and converts its clock to raw steps.
    07

    Lift odd hits to raw Collatz time

    N = 2^a M with M odd; Syracuse hits from M lift to raw Collatz hits from N

    The two-adic lift is deterministic. Initial halvings expose the odd core, each Syracuse movement expands into raw Collatz steps, and a finite density identity carries the odd result to the full positive population.

    Lean lemmas for this step
    • ND13LogTimeStatement
    • collatzLogTimeConstant
    • ndCollatzLogTimeConstant
    • nd13LogTimeStatement
  8. Symmetric columns of green nodes descend through a row of gold nodes; blue arcs converge on a central spiral while green trajectories fan outward above a large compass dial.
    The final package records the fixed quantitative engine, the odd-relative Syracuse and ordinary-density raw Collatz statements, explicit clocks below 145 and 436, and the untimed consequence.
    08

    Assemble the paper constants and endpoint

    C_syr = 501501/(5000 log 2) < 145; C_coll = 1509503/(5000 log 2) < 436

    The paper-facing theorem is a conjunction of separately meaningful checked components. It preserves the distinct density domains, the odd and raw clocks, the strict exponent reserve, the arbitrary diverging thresholds, and the older untimed natural-density chain.

    Lean lemmas for this step
    • ndSyracuseLogTimeConstant_eq_501501_div
    • ndCollatzLogTimeConstant_eq_1509503_div
    • ndSyracuseLogTimeConstant_lt_145
    • ndCollatzLogTimeConstant_lt_436
    • ndRhinLogTimePaperPackage
Original dark-green metadata cover for the paper Natural-Density Almost-Bounded Collatz Orbits in Logarithmic Time by Lech Mazur, with a phase-gap circle and descending logarithmic trajectories.

Companion research paper

Natural-Density Almost-Bounded Collatz Orbits in Logarithmic Time

Lech Mazur · 2026-07-16 · 27 pages

A mathematical paper developing the natural-density-one logarithmic-time Collatz descent theorem, its Rhin phase-gap input, the quantitative rate architecture, the Syracuse-to-raw-time bridge, and the square-root time-window corollary.

Read the paper (PDF) Download PDF
Paper, rights, and source relationship

Hosting authorized by the rightsholder. Original ProofAtlas metadata cover; not a reproduction of a paper page.

Lech Mazur, “Natural-Density Almost-Bounded Collatz Orbits in Logarithmic Time,” version 1, 16 July 2026.

  • The paper is mathematical exposition linked to the same theorem family; the exact checked Lean declarations and pinned source remain authoritative if wording differs.
  • The paper discusses a theorem that permits a density-zero exceptional set and does not claim the full Collatz conjecture or convergence of every orbit.

Exact formal proposition

Hypotheses and conclusion

This is the exact recorded theorem statement, followed by the source definitions that give its named predicates and quantities their full meaning.

theorem ndRhinLogTimePaperPackage : (NDM2Bounds (1 / 32000 : ℝ) (6993 / 200000 : ℝ) ∧ ND31LogTimeBounds (6993 / 200000 : ℝ) ndSyracuseLogTimeConstant ∧ ND16LogTimeStatement ndSyracuseLogTimeConstant ∧ ND13LogTimeStatement ndCollatzLogTimeConstant) ∧ ndSyracuseLogTimeConstant < 145 ∧ ndCollatzLogTimeConstant < 436 ∧ NDChainStatement
Definitions used in this proposition

NDM2Bounds

def NDM2Bounds (cHit cTr : ℝ) : Prop :=
  ∃ CHit CTr x0 : ℝ,
    0 ≤ CHit ∧ 0 ≤ CTr ∧ 2 ≤ x0 ∧
      ∀ (x : ℝ), x0 ≤ x →
        ∀ (hx : 1 ≤ x) (branch : Tao.TaoSection5SourceBranch),
          let y := transportSourceY x branch
          ∃ hwindow : (oddBlock y).Nonempty,
          ∃ hmass : 0 < Tao.logFinsetMass (oddBlock y),
            uniformNoHitProbability x y hwindow ≤
                CHit * Real.rpow x (-cHit) ∧
              passFullL1 x y hx hwindow hmass ≤
                CTr * Real.rpow (Real.log x) (-cTr)

ND31LogTimeBounds

def ND31LogTimeBounds (c Ctime : ℝ) : Prop :=
  ∃ C : ℝ, 0 ≤ C ∧
    ∀ (N0 : ℕ) (x : ℝ), 2 ≤ N0 → 2 ≤ x →
      oddSyracuseLogTimeBadRatio Ctime N0 x ≤
        C * Real.rpow (Real.log (N0 : ℝ)) (-c)

ND16LogTimeStatement

def ND16LogTimeStatement (Ctime : ℝ) : Prop :=
  ∀ f : ℕ → ℝ,
    Tao.GrowsOnOddsToInfinity f →
      HasOddRelativeNatDensityOne
        {N : ℕ | ∃ m : ℕ,
          (m : ℝ) ≤ Ctime * Real.log (N : ℝ) ∧
            ((Tao.syracuse^[m]) N : ℝ) < f N}

ND13LogTimeStatement

def ND13LogTimeStatement (Ctime : ℝ) : Prop :=
  ∀ f : ℕ → ℝ,
    Tao.GrowsToInfinity f →
      Terras.HasNatDensity
        {N : ℕ | 0 < N ∧ ∃ m : ℕ,
          (m : ℝ) ≤ Ctime * Real.log (N : ℝ) ∧
            ((collatzStep^[m]) N : ℝ) < f N} 1

NDChainStatement

def NDChainStatement : Prop :=
  ∃ cHit cTr : ℝ,
    0 < cHit ∧ 0 < cTr ∧
      NDM2Bounds cHit cTr ∧
      ND31Bounds cTr ∧
      ND16Statement ∧
      ND13Statement

ndSyracuseLogTimeConstant

noncomputable def ndSyracuseLogTimeConstant : ℝ :=
  Tao.taoAlpha * ndSyracuseAmbientTimeConstant

ndCollatzLogTimeConstant

noncomputable def ndCollatzLogTimeConstant : ℝ :=
  collatzLogTimeConstant ndSyracuseLogTimeConstant
Open main Lean file

Result boundary

What this page does—and does not—establish

The checked package gives two related logarithmic-time conclusions: odd-relative natural density one among odd starts for the Syracuse clause with f tending to infinity along odd inputs, and ordinary natural density one among positive starts for the raw Collatz clause with f tending to infinity on all positive inputs. It also records a dependent square-root raw-time bracket.

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 · 599 Lean files · 2 evidence records · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Technical evidence, source identity, and assumptions
Main Lean declaration
ndRhinLogTimePaperPackage
Source commit
ca3dd0d63920

Mechanical evidence

How Lean checked the proof

These fields support the exact Lean declaration, not a broader informal claim.

Artifact ID
artifact.known-nd-rhin-log-time.paper-package.v002
Declarations covered by recorded evidence
Erdos1135.ND.ndRhinLogTimePaperPackage
Lean build
passed
Recorded build time
2.3 s one machine-dependent evidence run, not a benchmark
Evidence collected
· clean-source provenance recorded
Unfinished proof check
passed
Lean toolchain
leanprover/lean4:v4.30.0-rc2
Recorded source commit
ca3dd0d63920411213403092aecc6946619eb082
Source SHA-256
sha256:040eae84c87d52a042c53574a44533091e453b3d0f409d81dd5e951ba294012a
Statement alignment
accepted

Lean foundations

Standard foundations used by the proof

Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.

  • Classical.choice
  • Quot.sound
  • propext

Independent review

Formal-result publication reviews accepted

The required formal-result publication reviews are accepted for this exact theorem. The displayed visuals passed their separate publication review and remain explanatory, not proof evidence. See review details on the formalization page.

Expanded visual

Open original image in a new tab