pith. machine review for the scientific record. sign in

arxiv: 2605.04734 · v2 · submitted 2026-05-06 · 🧮 math.CO · cs.DM· cs.LO

Recognition: 1 theorem link

· Lean Theorem

Hamilton decompositions of all directed tori at odd modulus

Sanghyun Park
Authors on Pith no claims yet

Pith reviewed 2026-05-12 01:59 UTC · model grok-4.3

classification 🧮 math.CO cs.DMcs.LO
keywords directed Hamilton decompositionCayley graphtorusHamilton cycleodd modulusCartesian productgroup ring
0
0 comments X

The pith

The arc set of every directed d-torus with odd cycle length m partitions into d directed Hamilton cycles.

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

This paper establishes a complete solution to the equal-side directed Hamilton decomposition problem for all odd moduli. It shows that the directed Cartesian product of d cycles of length m, for any d at least 2 and odd m at least 3, can have its arcs partitioned into exactly d directed Hamilton cycles. The proof relies on root flat certificates for small dimensions and lifting theorems that use Cartesian products and a successor operation to reach arbitrary dimensions. An accompanying formalization in Lean verifies the key steps and base cases. If correct, this means all such directed toroidal networks admit perfect cycle covers by Hamilton paths in equal number to the dimension.

Core claim

We prove that the directed Cayley graph D_d(m) on (Z/mZ)^d with generators the standard basis vectors admits a decomposition of its arcs into d directed Hamilton cycles whenever m is odd and d ≥ 2. The result follows from combining the root flat certificate theorem with a prefix count primitivity criterion and a modular trade lifting theorem, using closure under Cartesian products and the map b to 2b+1 to extend from base dimensions 2, 3, 5, 7 to all d. The critical boundary cases D_7(3) and D_7(5) are settled by explicit non-prefix root flat certificates.

What carries the argument

The modular trade lifting theorem together with closure under Cartesian product and the successor step, which propagate Hamilton decompositions from low dimensions using root flat certificates.

Load-bearing premise

The explicit root flat certificates constructed for D_7(3) and D_7(5) are correct, and the prefix-count primitivity criterion accurately identifies the needed primitive elements.

What would settle it

An explicit check that the arc set of D_7(3) cannot be partitioned into 7 directed Hamilton cycles, or a failure of the primitivity criterion in one of the lifted constructions for some larger d.

Figures

Figures reproduced from arXiv: 2605.04734 by Sanghyun Park.

Figure 1
Figure 1. Figure 1: Proof architecture. The count branch covers odd view at source ↗
Figure 1
Figure 1. Figure 1: Structure of the proof. The initial dimensions are established within the paper; the [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Root-flat slicing. A Cayley step ei moves from one layer to the next; after re-centering to the root flat, it appears as the root-flat step qi . Definition 2.1 (Root-flat certificate). A root-flat certificate consists of maps dt(w, κ) ∈ {0, . . . , d − 1} for t ∈ Z/mZ, w ∈ Ad,m and colors κ ∈ {0, . . . , d − 1}, satisfying: (RF1) for each fixed (t, w), the map κ 7→ dt(w, κ) is a permutation of {0, . . . , … view at source ↗
Figure 2
Figure 2. Figure 2: Root-flat slicing. A Cayley step ei moves between consecutive layers and, after re￾centering to the root flat, appears as the root-flat step qi . Definition 3.1 (Root-flat certificate). A root-flat certificate is a family of maps dt(w, κ) ∈ {0, . . . , d − 1} (t ∈ Z/mZ, w ∈ Ad,m, κ ∈ {0, . . . , d − 1}) satisfying: (RF1) for every (t, w), the map κ 7→ dt(w, κ) is a permutation of {0, . . . , d − 1}; (RF2) … view at source ↗
Figure 3
Figure 3. Figure 3: Triangular prefix coordinates. Root-flat moves become prefix decrements, so the view at source ↗
Figure 3
Figure 3. Figure 3: Triangular prefix coordinates. Root-flat steps become prefix decrements, and the [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: One-layer factorization at a fixed threshold. The symbol ∆ supplies the missing label view at source ↗
Figure 4
Figure 4. Figure 4: One-layer factorisation at a fixed threshold. The label ∆ supplies the displacement [PITH_FULL_IMAGE:figures/full_fig_p018_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The q = 1 matching correction. The construction starts from a {±1}-matrix. The matching raises one entry in each P row; one compensating lowering in the distinguished row keeps the special column balanced and respects the q = 1 nonnegativity restriction. Proof. Nonnegativity has already been checked. The row sums are m because, for a non-final row, ai + (1 + εi) +X k (1 + εi + Σik) = ai + L(1 + εi) + r − a… view at source ↗
Figure 5
Figure 5. Figure 5: Boundary-certificate architecture for D7(3) and D7(5). Solid arrows are proof de￾pendencies: the zero-set compiler proves the local root-flat conditions (RF1)–(RF2), while the rank-coordinate model proves the global single-cycle condition (RF3). The dashed arrow records the executable verification script: it reconstructs the schedule from the zero-set certificate, checks the direct return cycles, and also … view at source ↗
Figure 6
Figure 6. Figure 6: Base-tail architecture. The base motion on view at source ↗
Figure 6
Figure 6. Figure 6: The q = 1 matching correction. Starting from a {±1}-matrix, the matching raises one entry per P-row; one compensating lowering at the distinguished row keeps the distinguished column balanced and respects the q = 1 nonnegativity restriction. The count matrix is now defined by Ni,0 = ai , Ni,∆ = 1 + εi , Ni,k = 1 + εi + Σik (1 ≤ i ≤ L), and Nd,0 = 1, Nd,∆ = 0, Nd,k = ck. Proposition 11.4 (Count matrix for q… view at source ↗
Figure 7
Figure 7. Figure 7: Cylinder decomposition. A phase partition splits one horizontal Hamilton direction view at source ↗
Figure 7
Figure 7. Figure 7: Lifting scheme from the base to the missing prefix coordinates. The base motion on [PITH_FULL_IMAGE:figures/full_fig_p036_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: A local active trade. A single vertex swap preserves the local Latin condition and view at source ↗
Figure 8
Figure 8. Figure 8: Cylinder decomposition. A phase partition splits one horizontal Hamilton direction [PITH_FULL_IMAGE:figures/full_fig_p038_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Dyadic-triadic interval hitting. The bounded ratio between consecutive elements of view at source ↗
Figure 9
Figure 9. Figure 9: A local active trade. A single vertex swap preserves the local Latin condition and [PITH_FULL_IMAGE:figures/full_fig_p040_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Formal dependency diagram for the release endpoint. The seed endpoints feed the view at source ↗
Figure 10
Figure 10. Figure 10: Selector-profile plot for the boundary zero-set compilers. The plot summarises the [PITH_FULL_IMAGE:figures/full_fig_p057_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Scale of the two boundary certificates and the direct check. The horizontal axis is [PITH_FULL_IMAGE:figures/full_fig_p060_11.png] view at source ↗
read the original abstract

Let $D_d(m) = \mathrm{Cay}((\mathbb{Z}/m\mathbb{Z})^d, {e_0, \ldots, e_{d-1}})$ denote the directed Cayley graph on the positive coordinate basis, equivalently the Cartesian product of $d$ directed cycles of length $m$. The equal side directed Hamilton decomposition problem asks when the arc set of $D_d(m)$ partitions into $d$ directed Hamilton cycles. We prove that such a decomposition exists for every $d \geq 2$ and every odd $m \geq 3$, settling the equal side directed Hamilton decomposition problem at all odd moduli. The proof combines root flat certificate theorem, a prefix count primitivity criterion, and a modular trade lifting theorem with two closure principles: the Cartesian product and the successor step $b \mapsto 2b+1$. Together these propagate the small base dimensions $d \in {2, 3, 5, 7}$ to all $d \geq 2$. The boundary cases $D_7(3)$ and $D_7(5)$, where the prefix-count family saturates its zero symbol budget, are handled by explicit non prefix zero set root flat certificates whose zero set compiler. An accompanying Lean 4 formalization verifies the main theorem and the finite certificate predicates.

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 / 2 minor

Summary. The paper proves that the directed Cayley graph D_d(m) = Cay((Z/mZ)^d, {e_0, …, e_{d-1}}) admits an arc decomposition into d directed Hamilton cycles for every d ≥ 2 and every odd m ≥ 3. The argument proceeds by establishing a root-flat-certificate theorem, a prefix-count primitivity criterion, and a modular-trade lifting theorem, then applying two closure principles (Cartesian product and the successor map b ↦ 2b+1) to reduce the problem to base dimensions d ∈ {2,3,5,7}; the remaining boundary cases D_7(3) and D_7(5) are discharged by explicit non-prefix zero-set certificates. All steps, including the finite certificate predicates, are verified by an accompanying Lean 4 formalization.

Significance. The result settles the equal-side directed Hamilton decomposition problem for all odd moduli, completing the classification for this infinite family of directed tori. The explicit machine-checked formalization of the main theorem, the lifting theorems, the primitivity criterion, and the two boundary certificates constitutes a substantial strength: it removes the usual manual-verification gap and supplies a fully auditable combinatorial existence proof.

minor comments (2)
  1. [Abstract] Abstract, final sentence: the clause “whose zero set compiler” is grammatically incomplete and should be rephrased to indicate that the zero-set predicates of the boundary certificates are themselves formalized.
  2. [Section 2] The notation for elements of the group ring Z[(Z/mZ)^d] is introduced only informally; a short displayed definition of the support and the zero-set of a certificate would improve readability when the prefix-count criterion is first stated.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and accurate summary of the manuscript, which correctly identifies the main theorem, the proof strategy via root-flat certificates, lifting theorems, and closure principles, as well as the role of the accompanying Lean 4 formalization. We are grateful for the recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained via machine-checked formalization

full rationale

The paper establishes the existence of Hamilton decompositions for all directed tori D_d(m) with d ≥ 2 and odd m ≥ 3 by combining the root flat certificate theorem, prefix count primitivity criterion, modular trade lifting theorem, and two closure principles (Cartesian product and successor step). These are propagated from verified base cases D_7(3) and D_7(5) using explicit certificates. An accompanying Lean 4 formalization verifies the main theorem, all supporting lemmas, and the finite certificate predicates, rendering the argument independent of any fitted parameters, self-definitional reductions, or load-bearing self-citations that encode the target result. No step reduces by construction to its inputs; the formal verification supplies external, machine-checked evidence.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The proof rests on standard axioms of group theory and graph theory together with three named combinatorial theorems (root flat certificate theorem, prefix count primitivity criterion, modular trade lifting theorem) whose statements are taken as given and then applied via two closure principles. No free parameters are fitted to data. No new entities are postulated.

axioms (3)
  • domain assumption Root flat certificate theorem
    Invoked to certify the base cases and boundary configurations for small d.
  • domain assumption Prefix count primitivity criterion
    Used to guarantee that certain elements generate the required cycles in the group ring.
  • domain assumption Modular trade lifting theorem
    Provides the inductive step that lifts solutions from modulus m to 2m+1.

pith-pipeline@v0.9.0 · 5535 in / 1431 out tokens · 40637 ms · 2026-05-12T01:59:48.299993+00:00 · methodology

Review history (2 revisions) →

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

32 extracted references · 32 canonical work pages · 2 internal anchors

  1. [1]

    Alspach, J.-C

    B. Alspach, J.-C. Bermond, and D. Sotteau, Decomposition into cycles I: Hamilton decom- positions, inCycles and Rays, NATO ASI Series C, vol. 301, Kluwer Academic Publishers, Dordrecht, 1990, pp. 9–18. 63

    work page 1990

  2. [2]

    Aquino-Michaels, Completing Claude’s cycles: multi-agent structured exploration on an open combinatorial problem, Version v1.0.0, Zenodo, 2026

    K. Aquino-Michaels, Completing Claude’s cycles: multi-agent structured exploration on an open combinatorial problem, Version v1.0.0, Zenodo, 2026. doi:10.5281/zenodo.19737970

    work page doi:10.5281/zenodo.19737970 2026

  3. [3]

    Aubert and B

    J. Aubert and B. Schneider, D´ ecomposition de la somme cart´ esienne d’un cycle et de l’union de deux cycles hamiltoniens en cycles hamiltoniens,Discrete Mathematics38 (1982), 7–16

    work page 1982

  4. [4]

    Baranyai and G

    Z. Baranyai and G. R. Sz´ asz, Hamiltonian decomposition of lexicographic product,Journal of Combinatorial Theory, Series B31 (1981), 253–261

    work page 1981

  5. [5]

    Bermond, O

    J.-C. Bermond, O. Favaron, and M. Mah´ eo, Hamiltonian decomposition of Cayley graphs of degree 4,Journal of Combinatorial Theory, Series B46 (1989), 142–153

    work page 1989

  6. [6]

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

    work page 2017

  7. [7]

    Z. R. Bogdanowicz, Identifying Hamilton cycles in the Cartesian product of directed cycles, AKCE International Journal of Graphs and Combinatorics17 (2020), no. 1, 534–538

    work page 2020

  8. [8]

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

    work page 1996

  9. [9]

    S. J. Curran and D. Witte, Hamilton paths in Cartesian products of directed cycles, inCycles in Graphs, Annals of Discrete Mathematics 27 (1985), 35–74

    work page 1985

  10. [10]

    Darijani, B

    I. Darijani, B. Miraftab, and D. Witte Morris, Arc-disjoint Hamiltonian paths in Cartesian products of directed cycles,Ars Mathematica Contemporanea25 (2025), no. 2, Paper P2.10

    work page 2025

  11. [11]

    M. F. Foregger, Hamiltonian decompositions of products of cycles,Discrete Mathematics24 (1978), 251–260

    work page 1978

  12. [12]

    Gale, A theorem on flows in networks,Pacific Journal of Mathematics7 (1957), 1073–1082

    D. Gale, A theorem on flows in networks,Pacific Journal of Mathematics7 (1957), 1073–1082

    work page 1957

  13. [13]

    Keating, Multiple-ply Hamiltonian graphs and digraphs,Cycles in Graphs, Annals of Discrete Mathematics 27 (1985), 81–88

    K. Keating, Multiple-ply Hamiltonian graphs and digraphs,Cycles in Graphs, Annals of Discrete Mathematics 27 (1985), 81–88

    work page 1985

  14. [14]

    D. E. Knuth, Claude’s cycles, Preprint, revised April 2026. https://www-cs-faculty. stanford.edu/~knuth/papers/claude-cycles.pdf

    work page 2026

  15. [15]

    Kotzig, Every Cartesian product of two circuits is decomposable into two Hamiltonian circuits, Centre de Recherches Math´ ematiques, Montr´ eal, Rapport 233, 1973

    A. Kotzig, Every Cartesian product of two circuits is decomposable into two Hamiltonian circuits, Centre de Recherches Math´ ematiques, Montr´ eal, Rapport 233, 1973

    work page 1973

  16. [16]

    Lacaze-Masmonteil, Hamiltonian decompositions of the wreath product of Hamiltonian decomposable digraphs,Discrete Mathematics349 (2026), no

    A. Lacaze-Masmonteil, Hamiltonian decompositions of the wreath product of Hamiltonian decomposable digraphs,Discrete Mathematics349 (2026), no. 6, Article 115012

    work page 2026

  17. [17]

    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 Mathematics, Algorithms and Applications11 (2019), no. 5, 1930002

    work page 2019

  18. [18]

    Liu, Hamiltonian decompositions of Cayley graphs on Abelian groups,Discrete Mathematics 131 (1994), 163–171

    J. Liu, Hamiltonian decompositions of Cayley graphs on Abelian groups,Discrete Mathematics 131 (1994), 163–171

    work page 1994

  19. [19]

    Liu, Hamiltonian decompositions of Cayley graphs on Abelian groups of odd order,Journal of Combinatorial Theory, Series B66 (1996), 75–86

    J. Liu, Hamiltonian decompositions of Cayley graphs on Abelian groups of odd order,Journal of Combinatorial Theory, Series B66 (1996), 75–86. 64

    work page 1996

  20. [20]

    Liu, Hamiltonian decompositions of Cayley graphs on abelian groups of even order,Journal of Combinatorial Theory, Series B88 (2003), 305–321

    J. Liu, Hamiltonian decompositions of Cayley graphs on abelian groups of even order,Journal of Combinatorial Theory, Series B88 (2003), 305–321

    work page 2003

  21. [21]

    Meng and Q

    J. Meng and Q. Huang, Hamiltonian cycles and decompositions of Cayley digraphs of finite abelian groups,Applied Mathematics–A Journal of Chinese Universities12 (1997), 259–266

    work page 1997

  22. [22]

    L. L. Ng, Hamiltonian decomposition of lexicographic products of digraphs,Journal of Combinatorial Theory, Series B73 (1998), 119–129

    work page 1998

  23. [23]

    SangHyun Park, Hamilton decompositions of the directed 3-torus: a return-map and odometer view, arXiv:2603.24708, 2026

    work page arXiv 2026

  24. [24]

    SangHyun Park, Hamilton decompositions of the directed 5-torus for odd modulus, arXiv:2604.27140v1, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  25. [25]

    SangHyun Park, Hamilton decompositions of the directed 7-torus at odd modulus via root-flat certificates and a prefix-count construction, arXiv:2605.00660v1, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  26. [26]

    SangHyun Park,Torus-Hamilton-Decomposition-Program, Lean 4 formalisation repository, release tag0.0.3.1-odd-anc, commit0a00a8a, 2026

    work page 2026

  27. [27]

    H. J. Ryser,Combinatorial Mathematics, Carus Mathematical Monographs 14, Mathematical Association of America, 1963

    work page 1963

  28. [28]

    Stong, Hamilton decompositions of Cartesian products of graphs,Discrete Mathematics 90 (1991), 169–190

    R. Stong, Hamilton decompositions of Cartesian products of graphs,Discrete Mathematics 90 (1991), 169–190

    work page 1991

  29. [29]

    Stong, Hamilton decompositions of directed cubes and products,Discrete Mathematics 306 (2006), no

    R. Stong, Hamilton decompositions of directed cubes and products,Discrete Mathematics 306 (2006), no. 18, 2186–2204

    work page 2006

  30. [30]

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

    work page 1978

  31. [31]

    E. E. Westlund, J. Liu, and D. L. Kreher, 6-regular Cayley graphs on abelian groups of odd order are Hamiltonian decomposable,Discrete Mathematics309 (2009), 5106–5110

    work page 2009

  32. [32]

    Witte and J

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

    work page 1984