First-party checked source

Source for Power-Saving Bound for Logarithmic-Time Collatz Descent

This pinned Lean source formalizes the following mathematical result: For every N ≥ 15,552, the proportion of natural numbers n < N that do not fall below their starting value within k ≤ log n accelerated Collatz steps is at most 10,000,000 · N⁻¹ᐟ¹⁰⁰. Download the complete checked closure, open the endpoint, or browse its supporting modules to study the proof or develop an extension.

Immutable source commit: 379cf63bbe657fd0cb5d824e7785d747fd0fc946

Checked source + agent continuation package · 20 Lean files · 1 evidence record · 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: 1
First-party Lean files: 20
Lean source lines: 2,511
Main recorded file: 201 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

Power-Saving Bound for Logarithmic-Time Collatz Descent

Erdos1135.Terras.natCountingRatio_finiteStoppingTime_log_failure_le_power

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: 379cf63bbe657fd0cb5d824e7785d747fd0fc946
Main Lean file: Erdos1135/Terras/EffectiveLogTimePower.lean
Main-file footprint: 201 lines
File SHA-256: sha256:a04c7c2b145512429a07591dc56f0fc04a77472a7630e5e4f63959fcaf3d7cce
Complete Lean closure: 20 files · 2,511 lines
Toolchain: leanprover/lean4:v4.30.0-rc2

Open main Lean file Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license Download Advameg, Inc. notice

Deduplicated checked source

Complete Lean import closure

This closure supports the theorem evidence record above.

Browse complete checked source · 20 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.

Erdos1135/Terras/EffectiveLogTimePower.lean201 lines
Erdos1135/Basic.lean19 lines
Erdos1135/CollatzStep.lean21 lines
Erdos1135/Division.lean25 lines
Erdos1135/Parity.lean49 lines
Erdos1135/Residues.lean62 lines
Erdos1135/Terras/Core/Defs.lean58 lines
Erdos1135/Terras/Density/NaturalDensity.lean358 lines
Erdos1135/Terras/EffectiveLogTimeStopping.lean338 lines
Erdos1135/Terras/FiniteStoppingTime.lean79 lines
Erdos1135/Terras/LogTimeStopping.lean67 lines
Erdos1135/Terras/Parity/Contraction.lean77 lines
Erdos1135/Terras/Parity/Residue.lean269 lines
Erdos1135/Terras/Parity/Word.lean234 lines
Erdos1135/Terras/Probability/Asymptotic.lean213 lines
Erdos1135/Terras/Probability/BinomialTail.lean210 lines
Erdos1135/Terras/Probability/Bitstrings.lean116 lines
Erdos1135/TwoAdic.lean32 lines
FormalConjectures/Util/ProblemImports.lean37 lines
FormalConjectures/Wikipedia/CollatzConjecture.lean46 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.