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

Proved

CubicP3Partition.kelmans_z8_implies_z1

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 deleting the vertices of any specified three-vertex path from any such graph leaves an induced graph with a $P_3$ -factor (claim $(z8)$ ), then every such graph has a $P_3$ -factor (claim $(z1)$ ). This is the reverse 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_z8_implies_z1 : ClaimZ8 -> ClaimZ1 := 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: (z8)⇒(z1)(z8) \Rightarrow (z1)(z8)⇒(z1)

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