Quantitative Collatz Descent

Formalization

Theorem → Lean map

Each conclusion of Theorem 1.1 in the public v2.0.2 article is linked to its exact Lean 4 declaration in the immutable v2.0.1 tag.

Browse CET v2.0.1 Archived artifact

The pin

v2.0.1CET release tag
4.15.0Lean toolchain
9837ca9Mathlib commit
3axioms, all standard

The development is pinned to commit db84058497f8be629c8a2460033e20fe303bd673 and archived under DOI 10.5281/zenodo.21797535. The public article is self-contained. Its supplementary formalization checks the principal theorem chain independently of the English proof.

What the axiom report says

PaperAudit.lean runs #print axioms over every declaration in the public chain. Each one reports only propext, Classical.choice, and Quot.sound — the three standard Lean axioms. There is no sorry, no native_decide, no ofReduceBool, and no project-local axiom.

Replay it yourself

From the lean directory of the tagged checkout:

lake build

lake env lean -DautoImplicit=false -DrelaxedAutoImplicit=false \
  -DmaxHeartbeats=20000000 \
  CollatzEndpointTransport/Linear/PaperDependencyAudit.lean

lake env lean -DautoImplicit=false -DrelaxedAutoImplicit=false \
  -DmaxHeartbeats=20000000 \
  CollatzEndpointTransport/Linear/PaperAudit.lean

These three commands answer three different questions. lake build is the source-reconstruction gate for the library. The dependency audit reports a transitive compiled-declaration closure plus a separate source-reference closure from Lean's .ilean metadata. The axiom audit is a logical-trust check and is not evidence of declaration reachability.

The map

Article labels below follow public Zenodo v2.0.2. Module paths are relative to lean/CollatzEndpointTransport/. The software tag also retains companion results from the preceding manuscript edition; they are not relabeled as theorem products of the streamlined public article.

Paper resultLean declarationModule
Public article v2.0.2
Theorem 1.1, part 1
natural-density descent		 QuantitativeCollatzMain.collatz_central_renyi_endpoint_natural_density_descent Linear/Main.lean
Theorem 1.1, part 1
optimized exceptional count		 QuantitativeCollatzMain.collatz_central_renyi_endpoint_exceptional_count_at_exponent Linear/Main.lean
Theorem 1.1, part 2
logarithmic-time witness		 QuantitativeCollatzMain.collatz_central_renyi_endpoint_natural_density_descent_timed Linear/Main.lean
Endpoint identity
exact nonattained value of \(\delta_0\)		 QuantitativeCollatzMain.centralRenyiEndpointAdmissibleExponent_eq_paper Linear/Main.lean
Principal mechanism
Article §4
central fixed-total Rényi core		 FixedTotal.fixedRenyiMoment_central_le Linear/CentralRenyiReverse.lean
Article §4
central endpoint aggregate		 FixedTotal.centralEndpointInformation_le Linear/CentralRenyiShell.lean
Article §5
quantitative density pullback		 FixedTotal.collatzPullback_dense_centralRenyi Linear/CentralRenyiPullback.lean
Article §§6–7
endpoint bootstrap socket		 OptimizedLinearPullback.centralRenyiEndpointOnlyTheorem_of_transport Linear/CentralRenyiEndpointOnly.lean

Package layout

  • Linear/Main.lean — referee-facing theorem API, with the exact nonattained endpoint log (1 / a0) / log (2 / a0).
  • Linear/CentralRenyi*.lean — the fixed-total endpoint estimate and quantitative pullback mechanism used by the article.
  • Linear/PaperDependencyAudit.lean — transitive compiled-declaration graph, .ilean source-reference graph, and the frozen release's manuscript-to-source roots.
  • Linear/PaperAudit.lean — the public #print axioms report.
  • Common/ — route-independent Collatz definitions, parity infrastructure, the stronger all-prefix one-block seed used by the formal proof, and dyadic summation.
  • QuadraticAppendix/ — the independently verified optional quadratic baseline, outside the principal article chain.

Scope of the formalization. The Lean development verifies the principal theorem chain: the descent conclusion, optimized exceptional-count estimate, and logarithmic-time witness. Its one-block seed is stronger than the terminal consequence used in the written proof. The article remains self-contained and does not use Lean to discharge a missing English step; conversely, Lean does not certify the literature discussion or every sentence of exposition. The dependency and axiom audits state the exact formal boundary.