Hamilton decompositions of the directed 5-torus for odd modulus
SangHyun Park
math.CO
Apr 29, 2026 · v1
TL;DR
A companion Lean 4 formalization independently verifies the Cayley statement and finite certificates.
Abstract
We prove that the directed five-dimensional torus $D_5(m) = \operatorname{Cay}((\mathbb{Z}_m)^5, \{e_0, e_1, e_2, e_3, e_4\})$ has a Hamilton decomposition for every odd integer $m \geq 3$. This is the first higher-dimensional case in which the return-map method requires a genuine zero-set selector rather than an odometer-type correction. The construction assigns the five outgoing generators by a cyclic layer schedule with one non-constant layer determined by a zero-set Latin table; an explicit finite exact-cover certificate proves that this layer is a matching. By cyclic symmetry, Hamiltonicity of all color classes reduces to a single normalized return map. For $m \geq 5$, an explicit first-return calculation on the section $p = 2$ gives one induced cycle whose excursion lengths sum to $m^4$. The remaining modulus $m = 3$ is settled by a printed finite cycle certificate. A companion Lean 4 formalization provides an independent machine verification of the Cayley statement and the finite certificates; source, audit scripts, and ancillary search code are available at
https://github.com/aria1th/Torus-Hamilton-Decomposition-Program.
Problem
Hamilton decompositions of directed tori (Cartesian products of directed cycles) have been studied in dimensions 2 and 3, but dimension 5 remained open. The return-map method used for dimension 3 requires a genuinely new technique (a zero-set selector) in higher dimensions.
Approach
The proof constructs a cyclic arc-coloring of D_5(m) with one non-constant layer determined by a zero-set Latin table. An explicit finite exact-cover certificate proves this layer is a matching. By cyclic symmetry, Hamiltonicity of all five color classes reduces to a single normalized return map. For m >= 5, an explicit first-return calculation on a section gives one induced cycle whose excursion lengths sum to m^4. The case m = 3 is settled by a finite cycle certificate. A companion Lean 4 formalization provides independent machine verification of the Cayley statement and finite certificates.
Results
The directed five-dimensional torus D_5(m) has a Hamilton decomposition for every odd integer m >= 3. This is the first higher-dimensional case requiring a genuine zero-set selector rather than an odometer-type correction in the return-map method.
