Hamilton decompositions of the directed 3-torus: a return-map and odometer view
This solves a specific combinatorial graph theory problem about Hamiltonian decompositions in directed torus graphs.
The paper proves that the directed 3-torus D_3(m) can be decomposed into three arc-disjoint directed Hamilton cycles for all integers m ≥ 3, with the proof formalized in Lean 4.
We prove that the directed 3-torus D_3(m), or equivalently the Cartesian product of three directed m-cycles, admits a decomposition into three arc-disjoint directed Hamilton cycles for every integer m >= 3. The proof reduces Hamiltonicity to the m-step return maps on the layer section S=i+j+k=0. For odd m, five Kempe swaps of the canonical coloring produce return maps that are explicitly affine-conjugate to the standard 2-dimensional odometer. For even m, a sign-product invariant rules out Kempe-from-canonical constructions, and a different low-layer witness reduces after one further first-return map to a finite-defect clock-and-carry system. The remaining closure is a finite splice analysis, and the case m=4 is handled separately by a finite witness. A Lean 4 formalization accompanies the construction.