We prove that the directed 3-torus D_3(m), or equivalently the Cartesian product of three directed m-cycles, admits a decomposition into three arc-disjoint directed Hamilton cycles for every integer m >= 3. The proof reduces Hamiltonicity to the m-step return maps on the layer section S=i+j+k=0. For odd m, five Kempe swaps of the canonical coloring produce return maps that are explicitly affine-conjugate to the standard 2-dimensional odometer. For even m, a sign-product invariant rules out Kempe-from-canonical constructions, and a different low-layer witness reduces after one further first-return map to a finite-defect clock-and-carry system. The remaining closure is a finite splice analysis, and the case m=4 is handled separately by a finite witness. A Lean 4 formalization accompanies the construction.

翻译：我们证明有向三维环 D_3(m)，即三个有向 m-环的笛卡尔积，对每个整数 m ≥ 3 均可分解为三个弧不交的有向哈密顿环。该证明将哈密顿性归结为层截面 S=i+j+k=0 上的 m 步回归映射。对于奇数 m，标准着色的五次 Kempe 交换产生的回归映射显式仿射共轭于标准二维里程计。对于偶数 m，符号乘积不变量排除了基于 Kempe 的标准构造，而一种不同的低层见证经一次进一步的首次回归映射后简化为有限缺陷的时钟进位系统。剩余闭合通过有限拼接分析完成，且 m=4 情形由有限见证独立处理。该构造附有 Lean 4 形式化证明。