Hamilton decompositions of all directed tori at odd modulus
SangHyun Park
math.CO
May 6, 2026 · v1
TL;DR
Accompanying Lean 4 formalization verifies the main directed-tori Hamilton decomposition theorem and finite certificate predicates.
Abstract
Let $D_d(m) = \mathrm{Cay}((\mathbb{Z}/m\mathbb{Z})^d, {e_0, \ldots, e_{d-1}})$ denote the directed Cayley graph on the positive coordinate basis, equivalently the Cartesian product of $d$ directed cycles of length $m$. The equal side directed Hamilton decomposition problem asks when the arc set of $D_d(m)$ partitions into $d$ directed Hamilton cycles. We prove that such a decomposition exists for every $d \geq 2$ and every odd $m \geq 3$, settling the equal side directed Hamilton decomposition problem at all odd moduli. The proof combines root flat certificate theorem, a prefix count primitivity criterion, and a modular trade lifting theorem with two closure principles: the Cartesian product and the successor step $b \mapsto 2b+1$. Together these propagate the small base dimensions $d \in {2, 3, 5, 7}$ to all $d \geq 2$. The boundary cases $D_7(3)$ and $D_7(5)$, where the prefix-count family saturates its zero symbol budget, are handled by explicit non prefix zero set root flat certificates whose zero set compiler. An accompanying Lean 4 formalization verifies the main theorem and the finite certificate predicates.
Problem
The equal-side directed Hamilton decomposition problem asks when the arc set of the directed Cayley graph on (Z/mZ)^d with the positive coordinate basis partitions into d directed Hamilton cycles. This remained open for odd moduli despite decades of partial results on related Hamiltonicity questions.
Approach
The proof combines a root flat certificate theorem, a prefix count primitivity criterion, and a modular trade lifting theorem with two closure principles: the Cartesian product and the successor step b -> 2b+1. These propagate small base dimensions d in {2,3,5,7} to all d >= 2. Boundary cases D_7(3) and D_7(5) are handled by explicit non-prefix zero-set root-flat certificates. An accompanying Lean 4 formalization verifies the main theorem and the finite certificate predicates.
Results
The paper settles the equal-side directed Hamilton decomposition problem for all d >= 2 and every odd m >= 3, completely resolving the odd-moduli case. The Lean 4 formalization provides machine-checked verification of both the main theorem and the finite certificate predicates used in the proof.