Kelmans Theorem 3.1: $(z1) \Rightarrow (z8)$

Proved

CubicP3Partition.kelmans_z1_implies_z8

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

combinatoricscubic-graphsgraph-theoryp3-factor

For finite simple cubic 3-connected graphs whose order is divisible by six, if every such graph has a $P_3$ -factor (claim $(z1)$ ), then deleting the vertices of any specified three-vertex path from any such graph leaves an induced graph that has a $P_3$ -factor (claim $(z8)$ ). This is the forward direction of the $(z1)$ - $(z8)$ equivalence in Kelmans's Theorem 3.1.

Preamble

import Definitions.Def_cubic_p3_partition_models

Formal statement

namespace CubicP3Partition

theorem kelmans_z1_implies_z8 : ClaimZ1 -> ClaimZ8 := by sorry

end CubicP3Partition

Source

A. Kelmans, Packing 3-vertex Paths In Cubic 3-connected Graphs, https://arxiv.org/abs/0910.2766v2, pp. 7-8, Theorem 3.1, claims (z1) and (z8).

View graph

Kelmans Theorem 3.1: (z1)⇒(z8)(z1) \Rightarrow (z8)(z1)⇒(z8)

Kelmans Theorem 3.1: $(z1) \Rightarrow (z8)$