Hamilton decompositions of the directed 7-torus at odd modulus via root-flat certificates and a prefix-count construction
SangHyun Park
math.CO
May 1, 2026 · v1
TL;DR
A Lean 4 formalization verifies the directed 7-torus Hamilton decomposition with symbolic and boundary certificates.
Abstract
We prove that the directed seven-dimensional equal-side torus D_7(m) = Cay((Z/mZ)^7, {e_0, e_1, ..., e_6}) admits a directed Hamilton decomposition for every odd integer m >= 3. The proof has two main contributions. First, we introduce the root-flat certificate: a named verification framework in which a Hamilton decomposition of D_n(m) follows from three local conditions on a single root flat -- row Latinness, layer bijectivity, and primitive return maps. This abstraction was used informally in the earlier odd D_5(m) construction; here it appears as a definition and a theorem, providing a common verification interface for prime-dimensional base cases. Second, for every odd m >= 7, we give a uniform prefix-coordinate construction: one-layer prefix maps, a symbol-count criterion, and explicit 7x7 count matrices produce all seven Hamilton factors without a finite search. The remaining moduli m = 3 and m = 5 are exactly the boundary where the prefix-count method provably cannot work; they are handled by finite root-flat certificates whose validity is checked in Lean 4. A Lean 4 formalization verifies the Cayley statement, with the symbolic branch and the finite boundary certificates checked in the same development.
Problem
Whether the directed seven-dimensional equal-side torus D_7(m) admits a directed Hamilton decomposition for every odd m >= 3 was an open question in the study of Hamiltonicity of Cartesian products of directed cycles.
Approach
The proof introduces the root-flat certificate framework, where a Hamilton decomposition follows from three local conditions on a single root flat (row Latinness, layer bijectivity, primitive return maps). For odd m >= 7, a uniform prefix-coordinate construction using one-layer prefix maps, a symbol-count criterion, and explicit 7x7 count matrices produces all seven Hamilton factors without finite search. Boundary moduli m=3 and m=5 are handled by finite root-flat certificates whose validity is checked in Lean 4.
Results
The directed 7-torus D_7(m) admits a directed Hamilton decomposition for every odd integer m >= 3. The Lean 4 formalization verifies both the symbolic branch (the uniform construction for m >= 7) and the finite boundary certificates (m = 3, 5) in a single development.