ProofAtlas

First-party checked source

Source for Natural-Density Collatz Descent in Logarithmic Time

This pinned Lean source formalizes the following mathematical result: 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. Download the complete checked closure, open the endpoint, or browse its supporting modules to study the proof or develop an extension.

Immutable source commit: ca3dd0d63920411213403092aecc6946619eb082

Checked source + agent continuation package · 599 Lean files · 2 evidence records · Download ZIP

Each ZIP contains the checked first-party local Lean import closure, exact statements and boundaries, license, notice, evidence, a source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled; this is not a portable whole-repository release.

Formalization at a glance

What is checked—and how much source supports it

Browse the counted source
Declarations covered by evidence
2
First-party Lean files
599
Lean source lines
182,625
Main recorded file
224 lines

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.

Exact theorem evidence

Natural-Density Almost-Bounded Collatz Orbits in Logarithmic Time

Erdos1135.ND.ndRhinLogTimePaperPackage

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit
ca3dd0d63920411213403092aecc6946619eb082
Main Lean file
Erdos1135/ND/LogTime/Paper.lean
Main-file footprint
224 lines
File SHA-256
sha256:040eae84c87d52a042c53574a44533091e453b3d0f409d81dd5e951ba294012a
Complete Lean closure
599 files · 182,625 lines
Toolchain
leanprover/lean4:v4.30.0-rc2
Open main Lean file Download main Lean fileDownload checker evidence (JSON)Download Apache-2.0 licenseDownload Advameg, Inc. notice

Exact theorem evidence

Square-Root Descent Has a Logarithmic Raw-Time Window

Erdos1135.ND.ndRhinRawCollatzSqrtLogTimeBracket

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit
ca3dd0d63920411213403092aecc6946619eb082
Main Lean file
Erdos1135/ND/LogTime/Paper.lean
Main-file footprint
224 lines
File SHA-256
sha256:040eae84c87d52a042c53574a44533091e453b3d0f409d81dd5e951ba294012a
Complete Lean closure
599 files · 182,625 lines
Toolchain
leanprover/lean4:v4.30.0-rc2
Open main Lean file Download main Lean fileDownload checker evidence (JSON)Download Apache-2.0 licenseDownload Advameg, Inc. notice

Deduplicated checked source

Complete Lean import closure

These exact bytes are shared by 2 theorem evidence records above, so the file browser is shown once.

Complete checked Lean closure

599 Lean files are available here

Start with the principal theorem and proof-architecture files below, or search the complete commit-pinned closure.

599Lean files
Search and browse all 599 checked Lean files

Every listed file is read from the same pinned Git commit. File links open raw source in a new tab; use the ZIP download for the complete package. External Mathlib modules are dependency-locked but are not copied into this first-party source tree.

Showing all 599 files

Erdos11358 files · 276 lines
Erdos1135/ND5 files · 400 lines
Erdos1135/ND/Band72 files · 22,193 lines
Erdos1135/ND/Density4 files · 538 lines
Erdos1135/ND/Discrepancy39 files · 12,953 lines
Erdos1135/ND/Fourier44 files · 12,067 lines
Erdos1135/ND/LogTime12 files · 2,351 lines
Erdos1135/ND/Probability5 files · 1,098 lines
Erdos1135/NumberTheory/Rhin14 files · 5,960 lines
Erdos1135/Tao4 files · 1,086 lines
Erdos1135/Tao/Density5 files · 1,205 lines
Erdos1135/Tao/Fourier32 files · 9,968 lines
Erdos1135/Tao/Probability37 files · 8,159 lines
Erdos1135/Tao/Renewal167 files · 75,780 lines
Erdos1135/Tao/Section314 files · 3,300 lines
Erdos1135/Tao/Section555 files · 10,580 lines
Erdos1135/Tao/Section639 files · 7,300 lines
Erdos1135/Tao/Syracuse37 files · 6,409 lines
Erdos1135/Terras/Core1 file · 58 lines
Erdos1135/Terras/Density1 file · 358 lines
Erdos1135/Terras/Parity2 files · 503 lines
FormalConjectures/Util1 file · 37 lines
FormalConjectures/Wikipedia1 file · 46 lines
Source hashMatches checked record
Lean buildPassed in recorded evidence
LicenseApache-2.0 · Advameg, Inc.

Provenance and reproducibility

Exact checked source, with reuse terms

The endpoint and every listed local import come from the exact recorded Git commit, and the endpoint matches the stored source hash byte for byte. The locally authored package material is licensed under Apache-2.0 by Advameg, Inc.; Mathlib and cited third-party material remain under their own terms. Machine-readable checker evidence is included.