Number theory · dynamical systems · formal theorem
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.
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
Square-root logarithmic time window at a glance
Accessible transcript
log N/(2 log 2) < m ≤ C_coll log N < 436 log N and Collatz^m(N) < √N
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.
Read the complete poster transcript
COLLATZ DYNAMICS · NATURAL DENSITY · RAW TIME
SQUARE-ROOT DESCENT HAS A LOGARITHMIC TIME WINDOW
FOR NATURAL-DENSITY-ONE MANY POSITIVE STARTS N
∃ m : ℕ,
log N / (2 log 2) < m
m ≤ C_coll · log N < 436 · log N
Collatz^m(N) < √N
WHY THE WINDOW HAS TWO SIDES
1 · UPPER CLOCK
The natural-density theorem supplies a hit below √N by logarithmic raw time.
2 · LOWER CLOCK
Before log N / (2 log 2), repeated halvings cannot take N below √N.
3 · EXACT BRACKET
The same witness satisfies both inequalities.
EXACT SCOPE
Natural density one, not every start. Raw Collatz steps. Strictly below √N, not arrival at 1. The lower clock is special to this square-root target and is not asserted for every diverging threshold.
Theorem schematic
A square-root hit inside a logarithmic 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.
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 ndRhinRawCollatzSqrtLogTimeBracket : Terras.HasNatDensity rawCollatzSqrtLogTimeBracketSet 1Definitions used in this proposition
rawCollatzSqrtLogTimeBracketSet
def rawCollatzSqrtLogTimeBracketSet : Set ℕ :=
{N : ℕ | 0 < N ∧ ∃ m : ℕ,
Real.log (N : ℝ) / (2 * Real.log 2) < (m : ℝ) ∧
(m : ℝ) ≤ ndCollatzLogTimeConstant * Real.log (N : ℝ) ∧
(m : ℝ) ≤ 436 * Real.log (N : ℝ) ∧
((collatzStep^[m]) N : ℝ) < Real.sqrt (N : ℝ)}Result boundary
What this page does—and does not—establish
The checked corollary says that a natural-density-one set of positive starts N has a raw Collatz iterate strictly below √N at some time m with log N / (2 log 2) < m, m ≤ Cₒₒₗₗ · log N, and m ≤ 436 · log N.
- This does not prove the Collatz conjecture, convergence for every start, or arrival at 1; a density-zero exceptional set may remain.
- The clock counts raw Collatz steps including halvings, and the descent below √N is strict.
- The lower clock is specific to the square-root target; the general growing-threshold theorem does not assert it.
- Natural density one is an asymptotic statement and does not provide a finite cutoff after which every start satisfies the 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.
Technical evidence, source identity, and assumptions
- Main Lean declaration
ndRhinRawCollatzSqrtLogTimeBracket- 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.raw-sqrt-bracket.v002- Declarations covered by recorded evidence
Erdos1135.ND.ndRhinRawCollatzSqrtLogTimeBracket- Lean build
- passed
- Recorded build time
- 2.0 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.choiceQuot.soundpropext
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.