← All papers
First page of Hamilton decompositions of the directed 7-torus at odd modulus via root-flat certificates and a prefix-count construction

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
A Lean 4 formalization verifies the directed 7-torus Hamilton decomposition with symbolic and boundary certificates.
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.

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.

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.

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.