Kelmans Theorem 3.1 via 3.15: $(z7) \Rightarrow (z8)$

Proved

CubicP3Partition.kelmans_z7_implies_z8

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

combinatoricscubic-graphsgraph-theoryp3-factor

If deleting any two distinct edges of a cubic 3-connected graph of order divisible by six leaves a graph with a $P_3$ -factor, then deleting any 3-vertex path leaves a graph with a $P_3$ -factor. This is the $(z7) \Rightarrow (z8)$ step of Kelmans Theorem 3.1, proved in Section 3.15 with a two-copy gadget joined by a bijection between the deleted path's neighborhoods.

Preamble

import Definitions.Def_cubic_p3_partition_models
import Definitions.Def_kelmans_aux_claims

Formal statement

namespace CubicP3Partition

theorem kelmans_z7_implies_z8 : ClaimZ7 -> ClaimZ8 := 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.15, claims (z7) and (z8).

View graph

Kelmans Theorem 3.1 via 3.15: (z7)⇒(z8)(z7) \Rightarrow (z8)(z7)⇒(z8)

Kelmans Theorem 3.1 via 3.15: $(z7) \Rightarrow (z8)$