Hamilton decompositions of equal-side directed tori
SangHyun Park
math.CO
May 6, 2026 · v3
cs.DM cs.LO
TL;DR
The all-dimensions Hamilton decomposition theorem and its case-split structure are formalized in Lean 4 with Mathlib, with a released artifact and pinned versions.
Abstract
Let $D_d(m)$ be the Cartesian product of $d$ positively oriented directed cycles of length $m$. We prove that $D_d(m)$ decomposes into $d$ directed Hamilton cycles for every $m\ge3$ and $d\ge2$. The construction proceeds by splitting coordinate directions in directed multitori. An integer selection theorem supplies unit voltages compatible with the prescribed arc multiplicities; at even modulus, the decisive condition is the parity of each incidence component. For even $m$ and odd $d\ge7$, we satisfy this condition with a factorization having one additional cycle. A relative lifting theorem preserves the first-return data of a three-colour recolouring through successive coordinate splits, after which the recolouring removes the additional cycle on a set whose size is independent of the dimension. Explicit constructions complete the low-dimensional cases. The theorem yields Hamilton decompositions of Cartesian products of equal-order, equal-degree Hamilton-decomposable digraphs, of abelian Cayley digraphs whose generators partition into module bases, and of a family of height-stretched directed tori.
Problem
Determine whether the Cartesian product D_d(m) of d directed cycles of length m decomposes into d arc-disjoint directed Hamilton cycles for every m≥3 and d≥2.
Approach
Hamilton decompositions are encoded as root-flat certificates and reduced to prefix-admissible count matrices with gcd primitivity conditions. A high-modulus count branch handles m≥d. Base-tail certificates with skew-product lifts handle smaller moduli. Product and successor closure rules, plus parity arguments and recolouring for even m, cover all dimensions. A Lean 4 formalization (with Mathlib) records the full result and its branch structure.
Results
D_d(m) admits a directed Hamilton decomposition for all m≥3 and d≥2. Corollaries cover Cartesian products of Hamilton-decomposable digraphs, certain abelian Cayley digraphs, and height-stretched tori. The Lean development is released as a reproducibility artifact.