Lean evidence record
Tao’s Almost-Bounded Collatz Orbits: Lean evidence
This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.
Exact formal proposition
Hypotheses and conclusion
This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.
def TaoAlmostBoundedColMinStatement : Prop :=
∀ f : ℕ → ℝ,
GrowsToInfinity f →
HasLogDensity {N : ℕ | 0 < N ∧ (collatzOrbitMin N : ℝ) < f N} 1Definitions used in this proposition
GrowsToInfinity
def GrowsToInfinity (f : ℕ → ℝ) : Prop :=
Tendsto f atTop atTopHasLogDensity
def HasLogDensity (s : Set ℕ) (d : ℝ) : Prop :=
Tendsto (fun N : ℕ => logCountingRatio s N) atTop (nhds d)collatzOrbitMin
noncomputable def collatzOrbitMin (N : ℕ) : ℕ :=
sInf (collatzOrbitValues N)Lean wrapper declaration
The checked endpoint names the expanded proposition above. Both come from the same commit-pinned source.
theorem taoAlmostBoundedColMin_checked : TaoAlmostBoundedColMinStatementLine 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.
Technical evidence record
Source identity, checker results, and assumptions
- Main Lean declaration
taoAlmostBoundedColMin_checked- Source commit
d53c8de00056
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.known-tao-almost-bounded-orbits.colmin.v001- Accepted-result title
- Accepted Result: Tao's Almost-Bounded Collatz Orbits
- Accepted-result status
- Accepted formalization of a known theorem
- Accepted-result boundary
- This target records Tao's strict orbit-minimum formulation: for every real-valued function f on the natural numbers that tends to infinity, the positive starting values N whose standard Collatz orbit minimum is strictly below f(N) have logarithmic density one. Non-claim: This does not prove the full Collatz conjecture or that every orbit reaches 1. Non-claim: This is not a natural-density result and supplies no uniform density-convergence rate in f. Non-claim: It does not formalize every printed intermediate line of Tao's paper or claim that ProofAtlas originated the theorem. Non-claim: This accepted-result record does not by itself authorize public export or deployment.
- Declarations covered by recorded evidence
Erdos1135.Tao.taoAlmostBoundedColMin_checkedErdos1135.Tao.taoAlmostBounded_checked- Lean build
- passed
- Recorded build time
- 4.5 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
d53c8de00056fb05999e44589f2399d7efa026e4- Source SHA-256
sha256:ca16df30d1c105812c238360a63fa27d3ef1933631713aa4f6cced71b9f9267d- 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
Files and machine-readable evidence
Reproduce or inspect the recorded check
Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.
Review results
Publication reviews accepted
All four required publication-review gates are accepted for the reviewed presentation of this exact theorem. The review results are separate from the Lean build and do not broaden the formal statement.
Read the publication-review details