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

Proved

CubicP3Partition.kelmans_z1_iff_z8

by hao jia · 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, the following two universal claims are equivalent:

every such graph has a $P_3$ -factor;
after deleting the vertices of any specified three-vertex path from any such graph, the remaining induced graph has a $P_3$ -factor.

(z1)\quad\Longleftrightarrow\quad(z8).

This is the $(z1)$ – $(z8)$ equivalence contained in Kelmans's larger list of equivalent claims.

Formalization Note Both sides quantify over ordinary small finite vertex types and use the mission's explicit noninduced path-factor and vertex-deletion models.

Preamble

import Definitions.Def_cubic_p3_partition_models

Formal statement

namespace CubicP3Partition

/-- The equivalence between claims (z1) and (z8) from Kelmans's Theorem 3.1. -/
theorem kelmans_z1_iff_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).

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

令 $A(W,G)$ 表示以下完整前提： $W$ 是 Type 中的一个小类型并带有 Fintype W 实例， $G$ 是定义在 $W$ 上的简单图，每个 $v∈W$ 的 $G$ 邻居数恰为 $3$ ， $4≤Fintype.card W$ ，对每个有限子集 $S⊆W$ 若 $S.card≤2$ 则从满足 $v∉S$ 的 subtype 上诱导出的 $G$ 图连通，并且 $Fintype.card W$ 除以 $6$ 的自然数余数为 $0$ ；令 $P(W,G)$ 表示存在自然数 $b$ 和双射 $Fin\,b×Fin\,3≃W$ ，且对每个 $i∈Fin\,b$ ，位置 $0$ — $1$ 和位置 $1$ — $2$ 的两条边都在 $G$ 中；令 $Q(W,G,L)$ 表示对一个指定的三元路径 $L$ （三个顶点两两不同，且 left—center、center—right 两条边在 $G$ 中），存在自然数 $b$ 和双射 $Fin\,b×Fin\,3≃\{v∈W ∣ v≠L.left ∧ v≠L.center ∧ v≠L.right\}$ ，并且这些位置的两类相邻对在 $G$ 的该剩余顶点诱导图中相邻。定理声明以下两个全称命题等价：对每个这样的 $W$ 、其有限性实例和每个 $G$ ， $A(W,G)$ 蕴含 $P(W,G)$ ；当且仅当对每个这样的 $W$ 、其有限性实例和每个 $G$ ， $A(W,G)$ 蕴含对每个指定的 $L:P3Path\,G$ 都有 $Q(W,G,L)$ 。右侧的内层全称在不存在指定三元路径时为空真；两个外层命题的量化范围都包括所有符合条件的小类型、有限性实例和简单图。

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Kelmans Theorem 3.1: (z1)⇔(z8)(z1) \Leftrightarrow (z8)(z1)⇔(z8)

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