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.

翻译：我们证明，对于每个奇数整数 m ≥ 3，有向七维等边环面 D_7(m) = Cay((Z/mZ)^7, {e_0, e_1, ..., e_6}) 存在有向哈密顿分解。该证明有两项主要贡献。首先，我们引入根平证书：一种命名验证框架，其中 D_n(m) 的哈密顿分解可从单个根平的三个局部条件——行拉丁性、层双射性和原始返回映射——推导得出。该抽象在早期的奇数 D_5(m) 构造中已被非正式使用；在此它作为定义和定理出现，为素数维基本情形提供了通用验证接口。其次，对于每个奇数 m ≥ 7，我们给出统一的前缀坐标构造：一层前缀映射、符号计数准则和显式 7×7 计数矩阵可在无需有限搜索的情况下生成全部七个哈密顿因子。其余模数 m = 3 和 m = 5 恰好是前缀计数方法必然失效的边界情形；它们通过有限根平证书处理，其有效性已在 Lean 4 中验证。Lean 4 形式化验证了该 Cayley 陈述，符号分支和有限边界证书在同一开发中得到校验。