Hamilton decompositions of the directed 7-torus at odd modulus via root-flat certificates and a prefix-count construction
This solves a case of a long-standing problem in graph theory (Hamilton decompositions of Cayley graphs) for dimension 7, extending previous results for dimensions 3 and 5.
The paper proves that the directed seven-dimensional torus D_7(m) admits a directed Hamilton decomposition for every odd m ≥ 3, using a new root-flat certificate framework and a prefix-count construction for m ≥ 7, with m=3,5 handled by finite certificates verified in Lean 4.
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.