ClaudesCycles.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

12 declarations, 3 contain sorry, 0 declared as axioms

Claude's Cycles

Reference: Claude's Cycles by Donald E. Knuth (2026)

Fix m ≥ 2. Consider the directed graph with vertex set (ZMod m)³, where from each vertex (i, j, k) there are directed arcs to (i+1, j, k), (i, j+1, k), and (i, j, k+1) (arithmetic mod m). The goal is to partition all 3m³ directed arcs into three edge-disjoint directed Hamiltonian cycles (each of length m³).

Knuth describes an explicit construction, found by Claude (Anthropic), that achieves this decomposition for all odd m ≥ 3. The case m = 2 is known to be impossible [Aub82]. The even case m > 2 is also settled. Knuth's paper says so in its final section, added in the 14 April 2026 revision: "Breaking news: The problem for even values of m is no longer in doubt!" Ho Boon Suan's algorithm [Ho26] is proved correct for even m ≥ 8 in [GPT26], and Aquino-Michaels [AM26] gives a decomposition for the even case that is simpler. The statement below starts at m = 4, which is below the range [GPT26] covers, so it also rests on the explicit solutions in [Kn26], whose header gives even m ≥ 4.

References

[Knu26] D. E. Knuth, "Claude's Cycles" (2026).
[Aub82] J. Aubert, B. Schneider, "Graphes orientés indécomposables en circuits hamiltoniens", J. Combin. Theory Ser. B 32 (1982), 347–349.
[Ho26] Ho Boon Suan, closed-form construction for even m, https://cs.stanford.edu/~knuth/even_closed_form.c
[GPT26] A proof that [Ho26] yields three m³-cycles for every even m ≥ 8, 14 pages, https://cs.stanford.edu/~knuth/even_closed_form_proof_final.pdf
[AM26] K. Aquino-Michaels, "Completing Claude's cycles: Multi-agent structured exploration on an open combinatorial problem", https://github.com/no-way-labs/residue
[Kn26] Explicit even solutions for even m ≥ 4, recorded with [Knu26], https://cs.stanford.edu/~knuth/even_solution.py
[KM26] K. Morrison, a Lean formalisation of the odd case, https://github.com/kim-em/KnuthClaudeLean

Imports (1)

FormalConjecturesUtil

abbrev ClaudesCycles.Vertex The vertex type: vectors in (ZMod m)³ line 62 source
Source documentation
The vertex type: vectors in (ZMod m)³.

no axioms what this means
Statement uses: Nat
Proof uses: Fin, OfNat.ofNat, ZMod
1 instances, coercions and auxiliary constants left out.
```
abbrev Vertex (m : ℕ) := Fin 3 → ZMod m
```
def ClaudesCycles.bumpAt Bump coordinate b of vertex v: add 1 to the b-th component line 65 source
Source documentation
Bump coordinate b of vertex v: add 1 to the b-th component.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, OfNat.ofNat, ClaudesCycles.Vertex
Proof uses: Function.update, ZMod, HAdd.hAdd
18 instances, coercions and auxiliary constants left out.
```
def bumpAt {m : ℕ} [NeZero m] (b : Fin 3) (v : Vertex m) : Vertex m :=
…
```
Mentions: ClaudesCycles.Vertex
def ClaudesCycles.cubeAdj Adjacency in the cube digraph: u is adjacent to v if v is obtained from u by bumping one coordinate line 70 source
Source documentation
Adjacency in the cube digraph: u is adjacent to v if v is obtained from u by bumping one coordinate.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, ClaudesCycles.Vertex
Proof uses: Exists, Fin, OfNat.ofNat, Eq, ClaudesCycles.bumpAt
5 instances, coercions and auxiliary constants left out.
```
def cubeAdj {m : ℕ} [NeZero m] (u v : Vertex m) : Prop :=
…
```
Mentions: ClaudesCycles.Vertex
def ClaudesCycles.IsDirectedHamiltonianCycle Documented declaration: IsDirectedHamiltonianCycle line 75 source
Source documentation
A permutation σ on vertices is a directed Hamiltonian cycle of a digraph with adjacency adj if every arc (v, σ v) is an edge, σ is a single cycle, and σ moves every vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Equiv.Perm
Proof uses: And, Equiv.Perm.IsCycle, Eq, Finset, Equiv.Perm.support, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
def IsDirectedHamiltonianCycle {V : Type*} [Fintype V] [DecidableEq V]
    (adj : V → V → Prop) (σ : Equiv.Perm V) : Prop :=
…
```
theorem ClaudesCycles.bumpAt_apply_self line 80 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, OfNat.ofNat, ClaudesCycles.Vertex, Eq, ZMod, ClaudesCycles.bumpAt, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Function.update_self, eq_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem ClaudesCycles.bumpAt_apply_of_ne line 85 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, Fin, OfNat.ofNat, Ne, ClaudesCycles.Vertex, Eq, ZMod, ClaudesCycles.bumpAt
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Function.update_of_ne, Ne.symm, HAdd.hAdd, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem ClaudesCycles.bumpAt_injective The three arcs leaving a vertex are distinct, which is what makes the ∃! in HasHamiltonianArcDecomposition a condition about arcs rather than about heads that might coincide line 93 source
Source documentation
The three arcs leaving a vertex are distinct, which is what makes the ∃! in HasHamiltonianArcDecomposition a condition about arcs rather than about heads that might coincide. It needs 1 < m.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, LT.lt, OfNat.ofNat, ClaudesCycles.Vertex, Function.Injective, Fin, ClaudesCycles.bumpAt
Proof uses: Fact, Fact.mk, Eq, Decidable.byContradiction, Not, ZMod, congrFun, False.elim, False, Eq.mp, HAdd.hAdd, Eq.trans, congrArg, ClaudesCycles.bumpAt_apply_of_ne, Ne.symm, ClaudesCycles.bumpAt_apply_self
36 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem bumpAt_injective {m : ℕ} [NeZero m] (hm : 1 < m) (v : Vertex m) :
    Function.Injective fun b => bumpAt b v := by
…
```
Mentions: ClaudesCycles.Vertex, ClaudesCycles.bumpAt
def ClaudesCycles.HasHamiltonianArcDecomposition Documented declaration: HasHamiltonianArcDecomposition line 105 source
Source documentation
The arcs of the cube digraph on (ZMod m)³ can be decomposed into three directed Hamiltonian cycles: there exist three permutations, each forming a directed Hamiltonian cycle, such that every arc (v, bumpAt b v) belongs to exactly one cycle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NeZero
Proof uses: Exists, Fin, OfNat.ofNat, Equiv.Perm, ClaudesCycles.Vertex, And, ClaudesCycles.IsDirectedHamiltonianCycle, ZMod, ClaudesCycles.cubeAdj, ExistsUnique, Eq, ClaudesCycles.bumpAt
14 instances, coercions and auxiliary constants left out.
```
def HasHamiltonianArcDecomposition (m : ℕ) [NeZero m] : Prop :=
…
```
theorem ClaudesCycles.not_hasHamiltonianArcDecomposition_one The hypothesis 1 < m on cube_hamiltonian_arc_decomposition is load-bearing line 114 source
Source documentation
The hypothesis 1 < m on cube_hamiltonian_arc_decomposition is load-bearing. At m = 1 the vertex type has one element, so the only permutation of it is the identity, which is not a cycle. Note that Odd 1 holds, so without 1 < m the odd statement would be false.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, ClaudesCycles.HasHamiltonianArcDecomposition, OfNat.ofNat, Nat
Proof uses: Fin, Equiv.Perm, ClaudesCycles.Vertex, And, ClaudesCycles.IsDirectedHamiltonianCycle, ZMod, ClaudesCycles.cubeAdj, ExistsUnique, Eq, ClaudesCycles.bumpAt, False, Equiv.Perm.IsCycle.ne_one, And.left, Equiv.Perm.IsCycle, Finset, Equiv.Perm.support, Finset.univ, And.right, Subsingleton.elim
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem not_hasHamiltonianArcDecomposition_one : ¬ HasHamiltonianArcDecomposition 1 := by
…
```
Mentions: ClaudesCycles.HasHamiltonianArcDecomposition
theorem ClaudesCycles.cube_hamiltonian_arc_decomposition For odd m > 1, the cube digraph on (ZMod m)³ has a Hamiltonian arc decomposition into three directed cycles [Knu26] sorry line 121 source
Source documentation
For odd m > 1, the cube digraph on (ZMod m)³ has a Hamiltonian arc decomposition into three directed cycles [Knu26].

depends on sorry what this means
Statement uses: Nat, NeZero, Odd, LT.lt, OfNat.ofNat, ClaudesCycles.HasHamiltonianArcDecomposition
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cube_hamiltonian_arc_decomposition {m : ℕ} [NeZero m] (hm : Odd m) (hm' : 1 < m) :
    HasHamiltonianArcDecomposition m := by
…
```
Mentions: ClaudesCycles.HasHamiltonianArcDecomposition
theorem ClaudesCycles.cube_hamiltonian_arc_decomposition_impossible_m2 The case m = 2 is impossible: the cube digraph on (ZMod 2)³ does not have a Hamiltonian arc decomposition [Aub82] sorry line 128 source
Source documentation
The case m = 2 is impossible: the cube digraph on (ZMod 2)³ does not have a Hamiltonian arc decomposition [Aub82].

depends on sorry what this means
Statement uses: Not, ClaudesCycles.HasHamiltonianArcDecomposition, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cube_hamiltonian_arc_decomposition_impossible_m2 :
    ¬ HasHamiltonianArcDecomposition 2 := by
…
```
Mentions: ClaudesCycles.HasHamiltonianArcDecomposition
theorem ClaudesCycles.cube_hamiltonian_arc_decomposition_even For even m > 2, the cube digraph on (ZMod m)³ has a Hamiltonian arc decomposition sorry line 136 source
Source documentation
For even m > 2, the cube digraph on (ZMod m)³ has a Hamiltonian arc decomposition. Knuth records this as settled in the final section of [Knu26], by [Ho26] with the proof in [GPT26] for even m ≥ 8, and by [AM26] for the even case generally.

depends on sorry what this means
Statement uses: Iff, True, Nat, NeZero, Even, LT.lt, OfNat.ofNat, ClaudesCycles.HasHamiltonianArcDecomposition
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cube_hamiltonian_arc_decomposition_even :
    answer(True) ↔ ∀ᵉ (m : ℕ) (_ : NeZero m) (_ : Even m) (_ : 2 < m),
      HasHamiltonianArcDecomposition m := by
…
```
Mentions: ClaudesCycles.HasHamiltonianArcDecomposition