Formal-evidence review
- Coverage
- 1 exact subject binding
- Reviewer
- Claude Fable 5
- Independence
- Independence not asserted
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.
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_coll · log N, and m ≤ 436 · log N.
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.
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 : ℝ)}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.
Result boundary
What this theorem 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_coll · 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.
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.
Technical evidence, source identity, and assumptions
- Main Lean declaration
ndRhinRawCollatzSqrtLogTimeBracket- Source commit
ca3dd0d63920
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.known-nd-rhin-log-time.raw-sqrt-bracket.v002- Accepted-result title
- Accepted Result: Square-Root Descent Has a Logarithmic Raw-Time Window
- 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.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
Publication review
Review record
Publication 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
Contributors and roles
Authorship and other contributions are recorded separately for this version.
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.
Download exact review bindings
Public-wording review
- Coverage
- 1 exact subject binding
- Reviewer
- Claude Fable 5
- Independence
- Independence not asserted
Result-boundary review
- Coverage
- 2 exact subject bindings
- Reviewer
- Claude Fable 5
- Independence
- Independence not asserted
Statement-alignment review
- Coverage
- 1 exact subject binding
- Reviewer
- Claude Fable 5
- Independence
- Independence not asserted
Citation
Cite this release
Use the version-specific citation so the authorship, scope, and public record remain attached.
Release history
Versions and public record
- Release
- Accepted result
- Version
- version 2
- Published
- Canonical page
- Open canonical page
Release chronology
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.