Formalization source
Source for the Collatz predecessor lower bound
These files contain the definitions and proofs behind the three predecessor-count lower bounds with exponents 9/10 and 901/1000. Read the theorem pages to understand the claims; use the source to study the proof, reproduce the check, test objections, or develop an extension.
Theorem exponents: 9/10 = 0.90 and 901/1000 = 0.901Source release: v1.0.0
Formalization at a glance
Three exact statements, one checked source closure
- Recorded declarations
- 3
- First-party Lean files
- 58
- Lean source lines
- 10,237
- Main recorded file
- 39 lines
How counting works: Line counts exclude blank lines; comments and documentation count. The total is the deduplicated first-party Lean import closure of the three recorded theorem declarations at commit 5f76a170e74e; Mathlib and other third-party dependencies are excluded. This is source footprint, not a proof-quality or difficulty score.
Provenance and reproducibility
The source commit 5f76a170e74ea5b0c37c56683bd4c1e9d72e5e3f ties every theorem page to the same unchanging files, so people and agents can inspect, reproduce, challenge, and build from the exact snapshot that was checked. The fixed-snapshot route is an additional archive view of this same commit, not a separate or newer source version.