ProofAtlas

Lean evidence record

Power-Saving Bound for Logarithmic-Time Collatz Descent: Lean evidence

This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.

Read theorem page
Lean buildpassed
Unfinished proof stepsNone
Publication reviewsAccepted

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.

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 natCountingRatio_finiteStoppingTime_log_failure_le_power {N : ℕ} (hN : 15552 ≤ N) : natCountingRatio {n : ℕ | ¬ ∃ k : ℕ, (k : ℝ) ≤ Real.log (n : ℝ) ∧ accelerated^[k] n < n} N ≤ 10000000 * (N : ℝ) ^ (-(1 / 100 : ℝ))
Definitions used in this proposition

accelerated

def accelerated (n : ℕ) : ℕ :=
  if Even n then n / 2 else (3 * n + 1) / 2

natCountingRatio

noncomputable def natCountingRatio (s : Set ℕ) (N : ℕ) : ℝ :=
  (natCount s N : ℝ) / (N : ℝ)
Open main Lean file

Technical evidence record

Source identity, checker results, and assumptions

Main Lean declaration
natCountingRatio_finiteStoppingTime_log_failure_le_power
Source commit
379cf63bbe65

Mechanical evidence

How Lean checked the proof

These fields support the exact Lean declaration, not a broader informal claim.

Artifact ID
artifact.known-terras-log-time-power.bound.v001
Declarations covered by recorded evidence
Erdos1135.Terras.natCountingRatio_finiteStoppingTime_log_failure_le_power
Lean build
passed
Recorded build time
1.2 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
379cf63bbe657fd0cb5d824e7785d747fd0fc946
Source SHA-256
sha256:a04c7c2b145512429a07591dc56f0fc04a77472a7630e5e4f63959fcaf3d7cce
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.choice
  • Quot.sound
  • propext

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.

Checked source + agent continuation package · 20 Lean files · 1 evidence record · Download ZIPBrowse counted source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license

Review bindings

Publication reviews accepted

All four required publication-review gates are accepted for the retained presentation of this exact theorem. The review bindings are recorded separately from the Lean build and do not broaden the formal statement.

Read the publication-review details