Hamilton decompositions of the directed 5-torus for odd modulus

TL;DR

This paper proves that the directed five-dimensional torus has a Hamilton decomposition for all odd moduli, introducing a novel zero-set selector method and providing explicit certificates and formal verification.

Contribution

It establishes the first higher-dimensional Hamilton decomposition result using a zero-set selector, with explicit certificates and formal proof verification.

Findings

Proves Hamilton decompositions exist for all odd m ≥ 3 in D_5(m).

Introduces a zero-set Latin table method for layer assignment.

Provides explicit finite certificates and formal verification via Lean 4.

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.