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

TL;DR

This paper proves the existence of directed Hamilton decompositions in seven-dimensional torus graphs for all odd moduli m >= 3, introducing root-flat certificates and a prefix-count construction for verification.

Contribution

It introduces the root-flat certificate framework and a prefix-count construction, providing a unified verification method for Hamilton decompositions in high-dimensional tori.

Findings

Proves Hamilton decompositions for all odd m >= 3 in D_7(m).

Introduces root-flat certificates as a verification framework.

Provides a prefix-count construction for m >= 7, verified in Lean 4.

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.