Formalization
Theorem → Lean map
Eleven public theorems, kernel-checked against Mathlib, with the exact boundary between what Lean certifies and what the manuscript assembles.
The pin
The development is frozen at commit
ef3410843bf58d69f771f5ba2c0571d54b54da59 and archived under
DOI 10.5281/zenodo.21930432.
The article is self-contained; this formalization checks the principal
theorem chain independently of the English proof.
What the axiom report says
PaperAudit.lean and TimeoutEndpointAudit.lean
run #print axioms over the public roots and the canonical
timeout chain. Every declaration reports only propext,
Classical.choice, and Quot.sound — Lean's
three standard axioms. There is no sorry, no
admit, no native_decide, no
ofReduceBool, and no project-local axiom.
Replay it yourself
From the lean/ directory of the tagged checkout:
lake build
lake build FirstPassageLinearTransportAlternates
lake build FirstPassageLinearTransportLegacy
The first command is the fail-loudly canonical gate and includes the
named audit roots. The other two independently reconstruct the
optional all-prefix cross-check and the historical two-regime library;
neither is part of the default target, and neither is imported by
Main.
The map
All eleven declarations below live in
Main.lean, namespace
FirstPassageLinearTransport.QuantitativeCollatzMain. Their
types display the literal shortcut and raw Collatz maps and the
package's explicit natural-density and exceptional-count definitions,
not an abstract surrogate. The authoritative machine-generated map is
PaperDependencyAudit.lean; the release record is
lean/FORMALIZATION.md.
| Result | Lean declaration |
|---|---|
| Headline | |
| Moving polylogarithmic endpoint canonical theorem; shell-dependent exponent |
collatz_first_passage_moving_polylogarithmic_natural_density_descent |
| Timeout compatibility name exact alias, identical proposition |
collatz_first_passage_timeout_moving_polylogarithmic_natural_density_descent |
| Fixed-exponent specialization every fixed \(A>A_{\rm FP}\), with orbit ceiling |
collatz_first_passage_fixed_polylogarithmic_natural_density_descent |
| Stretched-logarithmic companions | |
| Timed landing explicit \(6.953\log n\) shortcut clock |
collatz_first_passage_stretched_log_natural_density_descent |
| Unclocked consequence projection of the timed theorem |
collatz_first_passage_stretched_log_natural_density_descent_unclocked |
| Same-witness orbit ceiling clock, landing, and \(n^{1+\beta}\) at one witness |
collatz_first_passage_stretched_log_descent_with_orbit_ceiling |
| Raw Collatz clock unaccelerated map, \(10.44\log n\) |
collatz_first_passage_raw_stretched_log_natural_density_descent |
| Quantitative counts and fixed powers | |
| Stretched exceptional count every strict subendpoint power |
collatz_first_passage_quantitative_stretched_exceptional_count |
| Fixed-power exceptional count every fixed \(\alpha>0\) |
collatz_first_passage_quantitative_fixed_power_exceptional_count |
| Timed fixed-power descent natural-density consequence |
collatz_first_passage_fixed_power_natural_density_descent |
| Graded fixed-power clock time–descent tradeoff companion |
collatz_first_passage_graded_power_natural_density_descent |
Where the formal claim stops
This is a declaration-level coverage boundary, not an admitted obligation. Nothing in the development is left unproved. But some combined quantitative statements in the manuscript are assembled from separately checked components rather than exported as single wrapper theorems.
Specifically: the exact endpoint and combined forms of the quantitative stretched-logarithmic theorem, the moving raw specialization of the raw-clock corollary, and the literal capstone form of the fixed-barrier failure bound are manuscript derivations over formalized structural components. Lean separately checks the explicit \(6.953\log n\) witness, every strict subendpoint exceptional power, and the raw \(10.44\log n\) landing.
Likewise, the log-log, triple-log, and arbitrary-divergent profiles use the formal generic producer but have no literal public specialization of their own.
Principal checked chain
Beneath the public surface, the dependency audit maps the manuscript's load-bearing steps to checked declarations, including:
- the parity-vector bijection and exact affine iterate;
- maximal and adjustable barrier counts with deterministic orbit envelopes;
- first-passage reversal, tagged-fiber bounds, and loss-filtered transport;
- decreasing-rank direct-passage collapse and rank-scaled reverse-loss telescoping;
- the timeout tail and its endpoint-rate density estimate;
- the cumulative-time corridor and square-root feasible-time support;
- support-sensitive first-bad aggregation;
- logarithmic shortcut and raw clocks, and same-witness orbit ceilings;
- dyadic-shell exceptional estimates and natural-density assembly.
The optional all-prefix library proves the same moving theorem type by a
different low-rank producer, as an independent cross-check. It is built
separately and is never imported by Main.