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.
Scope: 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.
Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
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.
From a Diophantine phase gap to natural-density logarithmic-time descent
8 proof 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 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.
The Syracuse endpoint uses odd-relative density among odd starts; the raw Collatz endpoint uses ordinary density among positive starts.
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
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
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
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
For every target N₀ ≥ 2 and cutoff x ≥ 2, the bad-start count divided by x is bounded by C · (log N₀)^(-d).
05
Bound the fixed-target exceptional ratio
oddSyracuseLogTimeBadRatio(N₀, x) ≤ C · (log N₀)^(-d)
The bad starts are positive odd inputs that do not reach N₀ within the fixed logarithmic Syracuse-time budget. One nonnegative constant C bounds their count divided by x uniformly in the cutoff. The bound decreases when the target grows; it does not assert density-one descent for each fixed target.
Lean lemmas for this step
ND31LogTimeBounds
ndRhinND31LogTimeBounds_sameD
ndRhinLogTimeRate_sameD
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
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
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.
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
The theorem at a glance
Two logarithmic-time density conclusions at a glance
One checked package gives an odd-relative Syracuse theorem and a separate ordinary-density raw Collatz theorem with explicit logarithmic clocks.
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
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.
Result boundary
What this theorem 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.
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.
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.
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 2, 21 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.
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.
Accepted Result: Natural-Density Almost-Bounded Collatz Orbits in Logarithmic Time
Accepted-result status
Accepted formal theorem
Accepted-result boundary
This target records the exact paper-facing conjunction in Erdos1135.ND.ndRhinLogTimePaperPackage and the dependent square-root raw-time bracket. The main endpoint gives natural-density-one logarithmic-time Syracuse and raw Collatz descent for every diverging threshold, with explicit clock bounds and a fixed quantitative engine. Non-claim: It does not prove the Collatz conjecture, convergence for every start, or arrival at 1. Non-claim: Natural density one allows a density-zero exceptional set. Non-claim: The arbitrary threshold must tend to infinity but need not be monotone; the hit inequality is strict. Non-claim: The 145 bound counts odd-to-odd Syracuse steps, while 436 counts raw Collatz steps including halvings. Non-claim: No density-convergence rate uniform in arbitrary threshold functions, optimal time constant, or priority claim is asserted. Non-claim: The square-root lower clock belongs only to the dependent square-root corollary, not the general growing-threshold theorem. Non-claim: The Terras power-saving finite-stopping theorem is a separate companion and is not an input to this proof.
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
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.
Authorship and other contributions are recorded separately for this version.
Authorship
Paper author
Lech Mazur
Contributions
Direct contributionProofAtlas AI-agent collaboration
Unnamed ProofAtlas AI agents contributed route proposals, proof-route narrowing, finite probes, stress tests, and read-only audits.
Computation
Gap or error discovery
Proof strategy
Research direction
Direct contributionLech Mazur
Lech Mazur is the named author of the version-2 paper.
Exposition
Selected reviews
Review record
Each entry names the review question, exact subject coverage, and reviewer provenance recorded for this release. A selected review concerns only its named question and is not by itself proof or acceptance of a broader claim. These bindings alone do not establish that proof or computation checks were rerun.
This version is part of the release history. No independent external timestamp is claimed.
Scope of this release
AI development credit remains aggregate because stable historical model and run identities were not retained.
Lech Mazur is credited here as paper author; the inspected pre-authorization evidence did not support exclusive or fine-grained authorship of every proof, Lean, computation, or visual component.
No independent external priority anchor is recorded.
