Coverage in Heraclitus walks: interval filling and residue connectivity

This paper proves two sufficient conditions for a greedy Heraclitus walk starting at zero to visit every integer exactly once. The walk always chooses an unvisited integer at an allowed distance, preferring the destination closest to zero and the positive destination in a tie. Coverage is proved when the allowed distances either contain 1 and 2 and are unbounded, or contain all sufficiently large integers in specified residue classes whose residues, together with the modulus, have greatest common divisor 1. Further results include exact interval checkpoints, an explicit first-visit bound for the odd-tail case, and examples showing both coverage beyond the two main criteria and limitations of particular proof methods. The accompanying reproducible package contains the PDF and LaTeX manuscript, Lean 4.35.0 formal proofs, verification scripts and a guide connecting the paper’s statements to their formal counterparts. Versioned source package: https://github.com/gujord/heraclitus-coverage/tree/v1.0.0 Roger Gujord is the sole author and is responsible for the paper. Mathematical exploration, proof drafts, exposition and formalization were AI-assisted. Machine verification does not constitute independent human mathematical review. Such review remains outstanding, and historical originality and priority remain unconfirmed. Prose and data are licensed under CC BY 4.0; code is licensed under MIT. This is a separate work from the earlier base-seven paper: https://doi.org/10.5281/zenodo.23912682