Natural-Density Almost-Bounded Collatz Orbits in Logarithmic Time (AI, Lean)
A new formal proof in Lean establishes that for almost all positive integers, the Collatz process reaches a value below any growing threshold in logarithmic time, with explicit constants 145 (Syracuse) and 436 (Collatz). The result does not prove the full conjecture but represents a significant density result.
The theorem at a glance
Two logarithmic-time density conclusions at a glance
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 exact theorem and checked proofMain theorem · expanded proposition · proof walkthrough · Lean evidence→
Enlarge
Theorem schematic
Two density domains within two logarithmic clocks
EnlargeThe 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.
The theorem at a glance
Square-root logarithmic time window at a glance
The natural-density theorem supplies the upper clock for the square-root threshold. A deterministic halving argument supplies the strict lower clock, and the checked corollary retains one witness satisfying both inequalities.
Enlarge
Theorem schematic
A square-root hit inside a logarithmic window
EnlargeFor natural-density-one many starts, a raw Collatz hit below √N occurs inside a genuine logarithmic time window.
log N/(2 log 2) < m ≤ C_coll log N < 436 log N and Collatz^m(N) < √N
The same witness time is strictly greater than log N divided by 2 log 2 and no greater than the checked raw Collatz clock, which is below 436 · log N. The lower bound is special to the square-root target.
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.
Open PDF ↗
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.
Collatz results landscape
How these results relate
depends onstrengthenscomparison only
The atlas keeps proof dependencies separate from stronger sibling results and useful comparisons. The two lanes below are disconnected: neither predecessor-count family is an input to the density-and-time family.
Predecessor-count bounds
Three exact 0.90 theorem variants
Real cutoffx0.90Natural cutoffN0.90Positive scalectx0.901
Density and logarithmic time
Rhin feeds the quantitative rate engine
Rhin phase gap→Quantitative rate engine→
Natural-density theoremSquare-root time window
separate companion · not a dependencyTerras finite power-saving bound
Exact relationship evidence
Reviewed dependency path: Rhin phase gap → ND31 main → ND31 bounds → same-exponent rate → fixed rate → the two sibling density-family endpoints. Six retained depends_on edges support this contracted path.
Comparison only: the Terras result is explicitly recorded as a separate companion, not an input to the natural-density proof.
No inferred edge: shared source files, a common subject, or historical background do not create a theorem dependency.
Scope limits
What this formalization does not claim
This does not prove the Collatz conjecture, convergence for every start, or arrival at 1; a density-zero exceptional set may remain.
The threshold must tend to infinity but need not be monotone, and the hit below it is strict.
The odd-relative Syracuse conclusion and ordinary-density raw Collatz conclusion have different domains and must not be collapsed into one claim about all positive starts.
The 145 bound counts odd-to-odd Syracuse steps, while the 436 bound counts raw Collatz steps including halvings.
The square-root lower clock belongs only to the companion square-root corollary, not to the general growing-threshold theorem.
The separate Terras power-saving finite-stopping theorem is a companion comparison, not an input to this proof.
The exact formal theorems
Open the checked proofs
Each theorem page includes its expanded exact proposition, visual explanation, complete checked source, and checker evidence. Longer proof routes also include a step-by-step walkthrough.
Lean proof
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 check passedNo unfinished proof stepsAccepted formal result
Open theorem and proofDownload main Lean file
Lean proof
Square-Root Descent Has a Logarithmic Raw-Time Window
For natural-density-one many positive starts N, a raw Collatz iterate falls strictly below √N after more than log N / (2 log 2) steps and by at most 436 · log N steps.
Lean check passedNo unfinished proof stepsAccepted formal result
Open theorem and proofDownload main Lean file
Continue the mathematics
Build from the checked theorem
Use the checked natural-density theorem to study stronger time constants, explicit density-convergence rates for restricted threshold classes, or other dynamical systems where arithmetic phase gaps feed quantitative mixing and descent.
Each 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 ZIPDownload graph and proof-architecture handoff (JSON)Browse the checked source onlineDownload main Lean file: Paper.lean
Formalization at a glance
What is checked—and how much source supports it
Browse the counted source
Declarations covered by evidence2
First-party Lean files599
Lean source lines182,625
Main recorded file224 lines
Explanatory proof route8 curated stages
How counting works: Line counts exclude blank lines; comments and documentation count. The total is the deduplicated, commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded. Declaration count means names covered by the artifact's recorded evidence; it is not a count of every declaration in the source. Source footprint is not a difficulty or proof-quality score.
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.