Papers With

← All papers
First page of Hamilton decompositions of the directed 3-torus: a return-map and odometer view

Hamilton decompositions of the directed 3-torus: a return-map and odometer view

SangHyun Park

math.CO Mar 25, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
A Lean 4 formalization accompanies the Hamilton decomposition construction for the directed 3-torus.
Abstract
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.
Problem

Whether the directed 3-torus D_3(m) (the Cartesian product of three directed m-cycles) admits a decomposition into three arc-disjoint directed Hamilton cycles for every m >= 3 was open.

Approach

The proof reduces Hamiltonicity to the m-step return maps on a 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 step. Parts of the construction are verified in Lean.

Results

D_3(m) admits a decomposition into three arc-disjoint directed Hamilton cycles for every integer m >= 3. The odd-m case uses five explicit Kempe swaps; the even-m case uses a separate construction that circumvents the sign-product obstruction. The Lean verification covers parts of the combinatorial argument.