Immutable source snapshot
Explicit Positive-Density Collatz Convergence in Logarithmic Time source at 830b9d3f38f2
This permanent route identifies the exact Git snapshot used by the recorded Lean theorem. The complete checked import closure, source footprint, downloads, and checker evidence are available on the source page.
Git commit830b9d3f38f2a8da8cd921bf6a9310dd69336fd0
Recorded theorem endpoint
CollatzPositiveDensity.densityConstant_pos · CollatzPositiveDensity.cutoff_pos · CollatzPositiveDensity.positive_density · CollatzPositiveDensity.positive_density_ten48
A fixed explicit positive fraction of the integers below every sufficiently large cutoff reaches 1 within 10.46 ln n ordinary Collatz steps. The full Collatz conjecture remains open.