Odd-Prime Perfect One-Factorization

Abstract

Kotzig’s construction gives a perfect one-factorization of the complete graph on one point adjoining the residues modulo an odd prime.

Definition 1.1 (Kotzig vertex type).

$$\begin{gathered} \forall p\in \mathbb{N}, \\ \mathrm{Vertex}(p):=\mathrm{Option}(\mathrm{ZMod}(p)). \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.Vertex (✓ std3).

Source. Repository-derived.

Commentary.

This repository formulation uses the classical Kotzig family as context. For a natural modulus p, the vertex type is exactly Option (ZMod p); the none vertex denotes the distinguished point at infinity.

Definition 1.2 (Partner map in one factor).

$$\begin{gathered} \forall p\in \mathbb{N},a\in \mathrm{ZMod}(p),x\in \mathrm{ZMod}(p), \\ (\mathrm{partner}(a,none)=\mathrm{some}(a))\wedge (\mathrm{partner}(a,\mathrm{some}(x))=\mathrm{ite}(x=a,none,\mathrm{some}((2:\mathrm{ZMod}(p))\cdot a-x))). \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.partner (✓ std3).

Source. Repository-derived.

Commentary.

This repository definition formulates the partner map in the classical Kotzig family. The factor indexed by a pairs infinity with a. Every other finite vertex x is paired with 2a-x, while the finite vertex a is paired back with infinity. The displayed ite is the exact branch structure of the Lean definition.

Definition 1.3 (Factor graph from the partner relation).

$$\begin{gathered} \forall p\in \mathbb{N},a\in \mathrm{ZMod}(p), \\ \mathrm{factor}(a):=\mathrm{SimpleGraph}.\mathrm{fromRel}((u,v:\mathrm{Vertex}(p)\mapsto v=\mathrm{partner}(a,u))). \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.factor (✓ std3).

Source. Repository-derived.

Commentary.

This repository definition formulates the classical Kotzig factor graph as exactly SimpleGraph.fromRel applied to the relation v = partner(a,u). The orientation shown here matches the Lean defining expression; fromRel supplies symmetry and removes loops.

Definition 1.4 (Union of two factors).

$$\begin{gathered} \forall p\in \mathbb{N},a\in \mathrm{ZMod}(p),b\in \mathrm{ZMod}(p), \\ \mathrm{pairGraph}(a,b):=\sup (\mathrm{factor}(a),\mathrm{factor}(b)). \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.pairGraph (✓ std3).

Source. Repository-derived.

Commentary.

This repository definition uses the classical Kotzig family as context. The pair graph is the lattice supremum, equivalently the edge union, of the factors indexed by a and b.

Definition 1.5 (Alternating-reflection translation step).

$$\begin{gathered} \forall p\in \mathbb{N},a\in \mathrm{ZMod}(p),b\in \mathrm{ZMod}(p), \\ \mathrm{translationStep}(a,b):=(2:\mathrm{ZMod}(p))\cdot (b-a). \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.translationStep (✓ std3).

Source. Repository-derived.

Commentary.

This repository definition records the translation used in its proof of the classical Kotzig family. Composing the two affine reflections gives displacement 2(b-a); in the partner graph that displacement is reached in one or two edges (the exceptional vertices are handled by a single edge).

Theorem 1.6 (Owner of an edge incident to infinity).

$$\begin{gathered} \forall p\in \mathbb{N}, \\ [\mathrm{Fact}(\mathrm{Prime}(p))], \\ \forall a\in \mathrm{ZMod}(p),x\in \mathrm{ZMod}(p), \\ (p\ne 2)\Rightarrow (\mathrm{Adj}(\mathrm{factor}(a),none,\mathrm{some}(x))⟺a=x). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.edge_owner_infinity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The edge from none to some x is in factor a exactly when a equals x.

Theorem 1.7 (Owner of a finite edge).

$$\begin{gathered} \forall p\in \mathbb{N}, \\ [\mathrm{Fact}(\mathrm{Prime}(p))], \\ \forall a\in \mathrm{ZMod}(p),x\in \mathrm{ZMod}(p),y\in \mathrm{ZMod}(p), \\ (p\ne 2\wedge x\ne y)\Rightarrow (\mathrm{Adj}(\mathrm{factor}(a),\mathrm{some}(x),\mathrm{some}(y))⟺a=\frac{(x+y)}{(2:\mathrm{ZMod}(p))}). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.edge_owner_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

For distinct finite vertices x and y, the owner is their midpoint. The displayed fraction is field division in ZMod p, with denominator two coerced into that field; it is not natural-number division.

Theorem 1.8 (Distinct factors have two neighbors at every vertex).

$$\begin{gathered} \forall p\in \mathbb{N}, \\ [\mathrm{Fact}(\mathrm{Prime}(p))], \\ \forall a\in \mathrm{ZMod}(p),b\in \mathrm{ZMod}(p), \\ (p\ne 2\wedge a\ne b)\Rightarrow (\forall v\in \mathrm{Vertex}(p), \\ \mathrm{ncard}(\mathrm{neighborSet}(\mathrm{pairGraph}(a,b),v))=2). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.pairGraph_two_regular (✓ std3). ∎

Source. Repository-derived.

Commentary.

This helper proof is repository work in the context of the classical Kotzig family. When a and b are distinct, the two partner vertices are distinct, so every neighbor set in pairGraph(a,b) has set cardinality two.

Theorem 1.9 (The translation step has full additive order).

$$\begin{gathered} \forall p\in \mathbb{N}, \\ [\mathrm{Fact}(\mathrm{Prime}(p))], \\ \forall a\in \mathrm{ZMod}(p),b\in \mathrm{ZMod}(p), \\ (p\ne 2\wedge a\ne b)\Rightarrow (\mathrm{addOrderOf}(\mathrm{translationStep}(a,b))=p). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.translationStep_addOrderOf (✓ std3). ∎

Source. Repository-derived.

Commentary.

This helper proof is repository work in the context of the classical Kotzig family. For distinct a and b and odd prime p, 2(b-a) is nonzero in ZMod p. Its additive order is therefore the prime p.

Theorem 1.10 (Kotzig’s odd-prime perfect one-factorization).

$$\begin{gathered} \forall p\in \mathbb{N}, \\ [\mathrm{Fact}(\mathrm{Prime}(p))], \\ (p\ne 2)\Rightarrow ((\forall a\in \mathrm{ZMod}(p),\mathrm{IsPerfectMatching}((\mathrm{Top}.\mathrm{top}:\mathrm{SimpleGraph}.\mathrm{Subgraph}(\mathrm{factor}(a)))))\wedge (\forall u\in \mathrm{Vertex}(p),v\in \mathrm{Vertex}(p), \\ (u\ne v)\Rightarrow (\exists !a\in \mathrm{ZMod}(p),\mathrm{Adj}(\mathrm{factor}(a),u,v)))\wedge (\forall a\in \mathrm{ZMod}(p),b\in \mathrm{ZMod}(p), \\ (a\ne b)\Rightarrow (\mathrm{IsHamiltonian}(\mathrm{pairGraph}(a,b))))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.odd_prime_perfect_one_factorization (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed reflection-factor family is the Kotzig GK construction, named in the scoped Library note only for p >= 11. Its three properties for every odd prime, including p = 3, 5, 7, are proved here. The note attests existence, not this explicit formulation.

For every odd prime p, every factor is a perfect matching on Option (ZMod p), and every pair of distinct vertices belongs to exactly one indexed factor.

For distinct indices a and b, alternating the two partner reflections reaches x+2(b-a) from x in one or two edges. Since this nonzero translation generates additive ZMod p, the two-regular pair graph is connected; Mathlib’s connected-cycle theorem then supplies a Hamiltonian cycle.

Theorem 1.11 (Existence of an odd-prime perfect one-factorization).

$$\begin{gathered} \forall p\in \mathbb{N}, \\ [\mathrm{Fact}(\mathrm{Prime}(p))], \\ (p\ne 2)\Rightarrow (\exists \mathrm{factors}:(\mathrm{ZMod}(p)\to \mathrm{SimpleGraph}(\mathrm{Vertex}(p))), \\ (\forall a\in \mathrm{ZMod}(p),\mathrm{IsPerfectMatching}((\mathrm{Top}.\mathrm{top}:\mathrm{SimpleGraph}.\mathrm{Subgraph}(\mathrm{factors}(a)))))\wedge (\forall u\in \mathrm{Vertex}(p),v\in \mathrm{Vertex}(p), \\ (u\ne v)\Rightarrow (\exists !a\in \mathrm{ZMod}(p),\mathrm{Adj}(\mathrm{factors}(a),u,v)))\wedge (\forall a\in \mathrm{ZMod}(p),b\in \mathrm{ZMod}(p), \\ (a\ne b)\Rightarrow (\mathrm{IsHamiltonian}(\sup (\mathrm{factors}(a),\mathrm{factors}(b)))))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.exists_odd_prime_perfect_one_factorization (✓ std3). ∎

Citation. Jack Allsop and Ian M. Wanless (2025). Perfect 1-factorisations of K_{11,11}. DOI: 10.48550/arXiv.2506.02455.

Commentary.

For every odd prime p, K_{p+1} admits a perfect one-factorization. The Library note attests this existence statement: Section 5 names Kotzig’s GK family for p >= 11, and Section 1 records existence at p = 3, 5, 7. Here the existential factors range over arbitrary graphs on Option (ZMod p); the proof instantiates them with the reflection factors of the preceding theorem.

References

• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.Vertex
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.edge_owner_infinity
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.edge_owner_pair
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.exists_odd_prime_perfect_one_factorization
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.factor
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.odd_prime_perfect_one_factorization
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.pairGraph
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.pairGraph_two_regular
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.partner
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.translationStep
• Truth anchor: D5/S3/ConceptDynamics/GraphColoring/OddPrimePerfectOneFactorization.translationStep_addOrderOf