Kelmans Theorem 3.1 via 3.16: $(t2) \Rightarrow (z7)$

Proved

CubicP3Partition.kelmans_t2_implies_z7

by WillR · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricscubic-graphsgraph-theoryp3-factor

If deleting the endpoints of any edge of a cubic 3-connected graph of order $2 \bmod 6$ leaves a graph with a $P_3$ -factor, then deleting any two distinct edges of a cubic 3-connected graph of order divisible by six leaves a graph with a $P_3$ -factor. This is the $(t2) \Rightarrow (z7)$ step of Kelmans Theorem 3.1, proved in Section 3.16 by subdividing both edges and joining the new vertices: the subdivided graph has order $2 \bmod 6$ , and removing the new edge's endpoints recovers the double edge-deletion.

Preamble

import Definitions.Def_cubic_p3_partition_models
import Definitions.Def_kelmans_aux_claims

Formal statement

namespace CubicP3Partition

theorem kelmans_t2_implies_z7 : ClaimT2 -> ClaimZ7 := by sorry

end CubicP3Partition

Source

A. Kelmans, Packing 3-vertex Paths In Cubic 3-connected Graphs, https://arxiv.org/abs/0910.2766v2, Theorem 3.1 and 3.16, claims (t2) and (z7).

View graph

Kelmans Theorem 3.1 via 3.16: (t2)⇒(z7)(t2) \Rightarrow (z7)(t2)⇒(z7)

Kelmans Theorem 3.1 via 3.16: $(t2) \Rightarrow (z7)$