The Collatz Covering Claim as an Explicit Hypothesis: A Machine-Checked Lean 4 Specification

A Lean 4 specification of the Collatz map, its iterates, and the covering claim that every positive integer reaches 1. Proved: the covering claim, taken as an explicit hypothesis, implies that every positive integer lies in the reverse tree of 1. Not proved: the Collatz conjecture itself; the result is conditional and makes no unconditional statement about it. #print axioms reports no axioms. The Lean development builds in CI (green on the commit archived here) with no sorry and no user-declared axioms. Source: https://github.com/BenFrohman/collatz-covering-claim at commit a678ee992137883780da79d81f6b3ea0a25e1f03.