Number theory · dynamical systems · formal theorem
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.
Scope: 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.
Exact formal proposition
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 1rawCollatzSqrtLogTimeBracketSet 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 : ℝ)}The theorem 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.
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
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.
Result boundary
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.
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
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.
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.
ndRhinRawCollatzSqrtLogTimeBracketca3dd0d63920Mechanical evidence
These fields support the exact Lean declaration, not a broader informal claim.
artifact.known-nd-rhin-log-time.raw-sqrt-bracket.v002Erdos1135.ND.ndRhinRawCollatzSqrtLogTimeBracketleanprover/lean4:v4.30.0-rc2ca3dd0d63920411213403092aecc6946619eb082sha256:040eae84c87d52a042c53574a44533091e453b3d0f409d81dd5e951ba294012aLean foundations
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.soundpropextIndependent review
Independent review is accepted for this exact theorem. The visuals passed a separate review and remain explanations, not proof evidence. See review details on the formalization overview.
Credit for this release
Authorship and other contributions are recorded separately for this version.
Unnamed ProofAtlas AI agents contributed route proposals, proof-route narrowing, finite probes, stress tests, and read-only audits.
Lech Mazur is the named author of the version-2 paper.
Selected reviews
Each entry names the question reviewed, its exact scope, and the reviewer provenance recorded for this release.
Download exact review bindings
Citation
Use the version-specific citation so the authorship, scope, and public record remain attached.
Release history
This version is part of the release history. No independent external timestamp is claimed.