pith. sign in

arxiv: 2606.21583 · v1 · pith:GERSXFFOnew · submitted 2026-06-19 · 🧮 math.CO · math.GR

Short Second Proof of the Odd-Modulus Directed Torus Hamilton Decomposition Theorem

SangHyun Park This is my paper

Pith reviewed 2026-06-26 13:35 UTC · model grok-4.3

classification 🧮 math.CO math.GR
keywords Hamilton decompositiondirected torusCayley graphodd modulusvoltage liftselection theoremformal verification
0
0 comments X

The pith

The directed Cayley graph D_d(m) on (Z/mZ)^d decomposes into d directed Hamilton cycles for every d≥2 and odd m≥3.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves that the directed torus graph D_d(m), defined as the Cayley graph on (Z/mZ)^d with positive unit generators, admits a decomposition into exactly d directed Hamilton cycles whenever the modulus m is odd and at least 3. The argument proceeds by induction on dimension: a base directed m-cycle with parallel copies is successively split using a fixed-row-sum selection theorem on replicated supports. This theorem guarantees voltage assignments that make each lifted factor traverse the fibres in a single m-cycle, preserving the necessary block structure for the next iteration. A reader cares because such decompositions give an explicit, symmetric organization of all arcs in these vertex-transitive digraphs.

Core claim

D_d(m) decomposes into d directed Hamilton cycles for every d≥2 and every odd m≥3. The combinatorial core is a fixed-row-sum selection theorem for replicated supports: when each indexed support A is repeated in m identical rows, one can select floor(|A|/2) entries from each row so that every column total is a unit modulo m. Applied to the Hamilton factors using a chosen coordinate direction, these selections prescribe the voltages in a cyclic lift that splits the direction into two. In fibre coordinates, the lifted successor is ĥ_j(x,z)=(h_j(x),z+1_{j∈M(x)}). After one traversal of the base Hamilton cycle, the fibre return is translation by the total carry. Since this carry is a unit modulo

What carries the argument

The fixed-row-sum selection theorem for replicated supports, which selects floor(|A|/2) entries per row so every column sum is a unit modulo m, controlling the carry in each cyclic lift.

If this is right

  • Each application of the selection theorem produces a valid Hamilton factor whose fibres remain direction-constant blocks.
  • Starting from d parallel copies of a directed m-cycle and iterating the lift d-1 times produces the full decomposition.
  • The same selection mechanism works uniformly for every coordinate direction chosen at each splitting step.
  • The resulting factors are edge-disjoint and cover every arc exactly once.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same selection theorem might allow decompositions when m is even if the unit condition is relaxed to coprime carries.
  • The block-preservation property could extend the method to other Cayley graphs on abelian groups with similar generating sets.
  • Formal verification in Lean 4 confirms that the combinatorial steps contain no hidden case distinctions for the given parameter ranges.

Load-bearing premise

The fixed-row-sum selection theorem holds when each support is replicated across m identical rows.

What would settle it

An explicit counterexample to the selection theorem for some support size and odd m, or a pair (d,m) with odd m≥3 where D_d(m) admits no decomposition into d directed Hamilton cycles.

read the original abstract

Let $D_d(m)=\operatorname{Cay}((\mathbb Z/m\mathbb Z)^d,\{e_1,\ldots,e_d\})$, with all generators oriented positively. We give a second proof that $D_d(m)$ decomposes into $d$ directed Hamilton cycles for every $d\ge 2$ and every odd $m\ge 3$. The combinatorial core is a fixed-row-sum selection theorem for replicated supports: when each indexed support $A$ is repeated in $m$ identical rows, one can select $\lfloor |A|/2\rfloor$ entries from each row so that every column total is a unit modulo $m$. Applied to the Hamilton factors using a chosen coordinate direction, these selections prescribe the voltages in a cyclic lift that splits the direction into two. In fibre coordinates, the lifted successor is $\widehat h_j(x,z)=(h_j(x),z+\mathbf 1_{\{j\in M(x)\}})$. After one traversal of the base Hamilton cycle, the fibre return is translation by the total carry. Since this carry is a unit modulo $m$, the return is a single $m$-cycle and the lifted factor is Hamilton. The new fibres also preserve the direction-constant block structure required for the next split. Iterating from a directed $m$-cycle with $d$ parallel copies of each arc yields the desired decomposition. The proof strategy was proposed with the assistance of OpenAI GPT-5.5 Pro and formally verified in Lean 4.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The paper gives a second proof that the directed Cayley graph D_d(m) = Cay((Z/mZ)^d, {e1,...,ed}) with all generators oriented positively decomposes into d directed Hamilton cycles whenever d≥2 and m≥3 is odd. The argument proceeds by iterative cyclic lifting: a fixed-row-sum selection theorem for m replicated copies of each support A is used to choose voltages so that each lifted factor remains Hamilton (the fibre return is a single m-cycle because the total carry is a unit mod m), while preserving the block structure needed for the next split. The base case begins with d parallel copies of a directed m-cycle; the entire construction, including the selection theorem, is formally verified in Lean 4.

Significance. If correct, the result supplies an alternative combinatorial proof of the odd-modulus directed torus Hamilton decomposition. The explicit machine-checked verification in Lean 4 of the selection theorem and the lifting steps constitutes independent, reproducible support for the central combinatorial core and is a notable strength of the manuscript.

minor comments (1)
  1. The abstract states that the proof strategy was proposed with assistance from OpenAI GPT-5.5 Pro; while not affecting correctness, a brief clarification in the introduction on the precise division of labor between the AI suggestion and the subsequent Lean formalization would improve transparency.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, recognition of the significance of the combinatorial argument and Lean 4 verification, and recommendation to accept the manuscript.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The manuscript supplies an explicit combinatorial argument whose core is the fixed-row-sum selection theorem, together with an iterative voltage-lifting construction whose correctness is asserted to have been machine-checked in Lean 4. Machine-checked proofs count as independent external support under the evaluation rules; the derivation therefore does not reduce to any fitted parameter, self-definitional equation, or load-bearing self-citation chain. No instance of the six enumerated circularity patterns appears in the provided text.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The argument rests on the validity of the fixed-row-sum selection theorem as a domain assumption in combinatorial number theory; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Fixed-row-sum selection theorem for replicated supports holds
    Invoked as the combinatorial core that guarantees column totals are units modulo m, enabling the lift to produce Hamilton cycles.

pith-pipeline@v0.9.1-grok · 5796 in / 1067 out tokens · 35736 ms · 2026-06-26T13:35:17.495126+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

19 extracted references · 6 canonical work pages · 3 internal anchors

  1. [1]

    Z. R. Bogdanowicz, On decomposition of the Cartesian product of directed cycles into cycles of equal lengths,Discrete Appl. Math.229 (2017), 148–150

    2017

  2. [2]

    Z. R. Bogdanowicz, Identifying Hamilton cycles in the Cartesian product of directed cycles,AKCE Int. J. Graphs Comb.17 (2020), no. 1, 534–538

    2020

  3. [3]

    S. J. Curran and J. A. Gallian, Hamiltonian cycles and paths in Cayley graphs and digraphs—a survey,Discrete Math.156 (1996), 1–18

    1996

  4. [4]

    S. J. Curran and D. Witte, Hamilton paths in Cartesian products of directed cycles, inCycles in Graphs, Ann. Discrete Math. 27, North-Holland, 1985, 35–74

    1985

  5. [5]

    Darijani, B

    I. Darijani, B. Miraftab, and D. Witte Morris, Arc-disjoint Hamiltonian paths in Cartesian products of directed cycles, arXiv:2203.11017v2, 2022; doi:10.48550/arXiv.2203.11017

    work page doi:10.48550/arxiv.2203.11017 2022

  6. [6]

    J. L. Gross and T. W. Tucker,Topological Graph Theory, Wiley, New York, 1987

    1987

  7. [7]

    Hasanvand, Modulo factors with bounded degrees, arXiv:2205.09012 (2022), doi:10.48550/arXiv.2205.09012

    M. Hasanvand, Modulo factors with bounded degrees, arXiv:2205.09012 (2022), doi:10.48550/arXiv.2205.09012

    work page doi:10.48550/arxiv.2205.09012 2022

  8. [8]

    Keating, Multiple-ply Hamiltonian graphs and digraphs, inCycles in Graphs, Ann

    K. Keating, Multiple-ply Hamiltonian graphs and digraphs, inCycles in Graphs, Ann. Discrete Math. 27, North-Holland, 1985, 81–88

    1985

  9. [9]

    G. H. J. Lanel, H. K. Pallage, J. K. Ratnayake, S. Thevasha, and B. A. K. Welihinda, A survey on Hamiltonicity in Cayley graphs and digraphs on different groups,Discrete Math. Algorithms Appl.11 (2019), no. 5, 1930002

    2019

  10. [10]

    de Moura and S

    L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, inAutomated Deduction—CADE 28, Lecture Notes in Computer Science 12699, Springer, 2021, 625–635

    2021

  11. [11]

    The mathlib Community, The Lean mathematical library, inProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020, 367–381

    2020

  12. [12]

    Meng and Q

    J. Meng and Q. Huang, Hamiltonian cycles and decompositions of Cayley digraphs of finite abelian groups,Appl. Math. J. Chinese Univ.12 (1997), 259–266

    1997

  13. [13]

    S. H. Park, Hamilton decompositions of the directed3-torus: a return-map and odometer view, arXiv:2603.24708, 2026

    work page arXiv 2026

  14. [14]

    S. H. Park, Hamilton decompositions of the directed5-torus for odd modulus, arXiv:2604.27140, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  15. [15]

    S. H. Park, Hamilton decompositions of the directed7-torus at odd modulus via root-flat certificates and a prefix-count construction, arXiv:2605.00660, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  16. [16]

    S. H. Park, Hamilton decompositions of all directed tori at odd modulus, arXiv:2605.04734v2, 2026; doi:10.48550/arXiv.2605.04734

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2605.04734 2026

  17. [17]

    S. H. Park, Torus Hamilton Decomposition Program, Lean 4 source repository, 2026; source snapshot at commit7e96c0e1. 10

    2026

  18. [18]

    W. T. Trotter, Jr., and P. Erdős, When the Cartesian product of directed cycles is Hamiltonian,J. Graph Theory2 (1978), no. 2, 137–142

    1978

  19. [19]

    Witte and J

    D. Witte and J. A. Gallian, A survey: Hamiltonian cycles in Cayley graphs,Discrete Math.51 (1984), no. 3, 293–304. 11

    1984