Kelmans Theorem 3.1 via 3.8: $(z1) \Rightarrow (z4)$

Proved

CubicP3Partition.kelmans_z1_implies_z4

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

combinatoricscubic-graphsgraph-theoryp3-factor

If every cubic 3-connected graph of order divisible by six has a $P_3$ -factor, then for every such graph and every vertex $x$ there is a 3-vertex path centered at $x$ whose deletion leaves a graph with a $P_3$ -factor. This is the $(z1) \Rightarrow (z4)$ step of Kelmans Theorem 3.1, proved in Section 3.8 via a $K_{3,3}$ blow-up: a counterexample vertex that is an endpoint in every factor lifts to a cubic 3-connected graph with no factor at all.

Preamble

import Definitions.Def_cubic_p3_partition_models
import Definitions.Def_kelmans_aux_claims

Formal statement

namespace CubicP3Partition

theorem kelmans_z1_implies_z4 : ClaimZ1 -> ClaimZ4 := 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.8, claims (z1) and (z4).

View graph

Kelmans Theorem 3.1 via 3.8: (z1)⇒(z4)(z1) \Rightarrow (z4)(z1)⇒(z4)

Kelmans Theorem 3.1 via 3.8: $(z1) \Rightarrow (z4)$