Models for cubic-graph $P_3$ -factors and the C02 family

Definition

cubic_p3_partition_models

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

combinatoricscubic-graphsgraph-theoryp3-factor

This module fixes the finite-simple-graph model used by the mission. It defines vertex degree, cubicity, 3-vertex-connectivity by deletion of at most two vertices, noninduced $P_3$ -factors, specified $P_3$ paths and their deletion, Kelmans's claims $(z1)$ and $(z8)$ , spanning 2-factors, perfect matchings, relative matching complements, and component-order divisibility.

It also defines the explicit graph family $H_q$ on $18+12q$ vertices from candidate C02 by a complete adjacency predicate. The first nine labels carry the fixed Petersen-minus-one-vertex brick, and the remaining labels and three joining edges are encoded arithmetically.

The bijection in P3Factor enforces both vertex coverage and disjointness. Only the two selected consecutive edges are required, so an ambient chord is allowed and the represented paths are not required to be induced.

Formalization Note The module is a shared, sorry-free interface. It does not assert that the open problem or the C02 candidate claims are proved.

Definition code

import Mathlib

namespace CubicP3Partition

universe u

variable {V : Type u} [Fintype V]

/-- The number of neighbors of a vertex. -/
noncomputable def degree (G : SimpleGraph V) (v : V) : Nat :=
  Nat.card {w : V // G.Adj v w}

/-- Every vertex has degree three. -/
def Cubic (G : SimpleGraph V) : Prop :=
  ∀ v, degree G v = 3

/-- Deleting any set of at most two vertices leaves a connected graph.
The order condition excludes the degenerate graphs with fewer than four vertices. -/
def ThreeVertexConnected (G : SimpleGraph V) : Prop :=
  4 ≤ Fintype.card V ∧
    ∀ S : Finset V, S.card ≤ 2 →
      (G.induce {v : V | v ∉ S}).Connected

/-- A partition of the vertices into ordered triples whose first--second and
second--third pairs are edges. No condition is imposed on the ambient edge
between the first and third vertices, so these paths need not be induced. -/
structure P3Factor (G : SimpleGraph V) where
  blockCount : Nat
  place : (Fin blockCount × Fin 3) ≃ V
  edge01 : ∀ i : Fin blockCount, G.Adj (place (i, 0)) (place (i, 1))
  edge12 : ∀ i : Fin blockCount, G.Adj (place (i, 1)) (place (i, 2))

/-- A specified three-vertex path in the ambient graph. -/
structure P3Path (G : SimpleGraph V) where
  left : V
  center : V
  right : V
  left_ne_center : left ≠ center
  center_ne_right : center ≠ right
  left_ne_right : left ≠ right
  edge_left : G.Adj left center
  edge_right : G.Adj center right

/-- Delete the three vertices of a specified path and take the induced graph. -/
def eraseP3 (G : SimpleGraph V) (L : P3Path G) :
    SimpleGraph {v : V // v ≠ L.left ∧ v ≠ L.center ∧ v ≠ L.right} :=
  G.induce {v : V | v ≠ L.left ∧ v ≠ L.center ∧ v ≠ L.right}

/-- Claim (z1) in Kelmans's Theorem 3.1, restricted to ordinary small types. -/
def ClaimZ1 : Prop :=
  ∀ (W : Type) [Fintype W], ∀ G : SimpleGraph W,
    Cubic G → ThreeVertexConnected G → Fintype.card W % 6 = 0 →
      Nonempty (P3Factor G)

/-- Claim (z8) in Kelmans's Theorem 3.1, restricted to ordinary small types. -/
def ClaimZ8 : Prop :=
  ∀ (W : Type) [Fintype W], ∀ G : SimpleGraph W,
    Cubic G → ThreeVertexConnected G → Fintype.card W % 6 = 0 →
      ∀ L : P3Path G, Nonempty (P3Factor (eraseP3 G L))

/-- A spanning 2-regular subgraph. -/
def TwoFactor (G F : SimpleGraph V) : Prop :=
  F ≤ G ∧ ∀ v, degree F v = 2

/-- Number of vertices in the connected component of `v` in `F`. -/
noncomputable def componentOrder (F : SimpleGraph V) (v : V) : Nat :=
  Nat.card {w : V // F.Reachable v w}

/-- A spanning 2-factor all of whose connected components have order divisible by three. -/
def DivisibleTwoFactor (G F : SimpleGraph V) : Prop :=
  TwoFactor G F ∧ ∀ v, 3 ∣ componentOrder F v

/-- The graph has a divisible 2-factor. -/
def HasDivisibleTwoFactor (G : SimpleGraph V) : Prop :=
  ∃ F : SimpleGraph V, DivisibleTwoFactor G F

/-- A spanning 1-regular subgraph. -/
def PerfectMatching (G M : SimpleGraph V) : Prop :=
  M ≤ G ∧ ∀ v, degree M v = 1

/-- The relative edge complement of `M` inside `G`, on the same vertex type. -/
def matchingComplement (G M : SimpleGraph V) : SimpleGraph V :=
  G ⊓ Mᶜ

/-- The strengthened route: some perfect matching has a divisible 2-factor as its complement. -/
def HasDivisibleComplement (G : SimpleGraph V) : Prop :=
  ∃ M : SimpleGraph V,
    PerfectMatching G M ∧ DivisibleTwoFactor G (matchingComplement G M)

/-- The twelve internal edges of the fixed Petersen-minus-one-vertex brick. -/
def brickEdges : List (Nat × Nat) :=
  [(0, 1), (0, 5), (1, 2), (1, 6), (2, 3), (2, 7),
   (3, 8), (4, 6), (4, 7), (5, 7), (5, 8), (6, 8)]

/-- A directed presentation of the edges used to define the C02 family. -/
def forwardEdge (q u v : Nat) : Prop :=
  (u, v) ∈ brickEdges ∨
  (9 ≤ u ∧ (v = u + 1 ∨ v = u + (6 * q + 5))) ∨
  (u = 0 ∧ v = 9) ∨
  (u = 3 ∧ v = 17 + 12 * q) ∨
  (u = 4 ∧ v = 13 + 6 * q)

/-- The explicit C02 graph family, of order `18 + 12*q`. -/
def H (q : Nat) : SimpleGraph (Fin (18 + 12 * q)) where
  Adj u v := u ≠ v ∧
    (forwardEdge q u.val v.val ∨ forwardEdge q v.val u.val)
  symm := ⟨by
    intro u v h
    exact ⟨Ne.symm h.1, h.2.symm⟩⟩
  loopless := ⟨by
    intro v h
    exact h.1 rfl⟩

end CubicP3Partition

Source

UnsolvedMath OPG-46613, https://www.unsolvedmath.com/problems/OPG-46613; A. Kelmans, arXiv:0910.2766v2, Problem 1.10 (p. 3), Section 2 and Theorem 3.1 (pp. 7–8), https://arxiv.org/abs/0910.2766v2; C01 and C02 at fixed revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a, https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/tree/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates

Read-back

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

degree：在宇宙 $u$ 中的有限类型 $V$ （带有 Fintype V 实例）上，对任意简单图 $G$ 和顶点 $v∈V$ ，degree G v 定义为满足 $G$ 在 $v$ 与 $w$ 之间有边的顶点 $w$ 所组成的 subtype 的自然数基数，即 $Nat.card(\{w : V ∣ G.Adj v w\})$ 。

Cubic：对上述有限类型 $V$ 上的简单图 $G$ ，Cubic G 是命题：对每个顶点 $v∈V$ ，满足 $G.Adj v w$ 的 $w∈V$ 的数量恰好等于 $3$ ，也就是 $∀v∈V,0;Nat.card(\{w : V ∣ G.Adj v w\})=3$ 。

ThreeVertexConnected：对有限类型 $V$ 上的简单图 $G$ ，ThreeVertexConnected G 当且仅当同时满足 $4≤Fintype.card V$ ，以及对每个有限子集 $S⊆V$ ，若 $S.card≤2$ ，则图 $G.induce \{v∈V ∣ v∉S\}$ 连通；这里被诱导图的顶点是带有 $v∉S$ 证明的 $V$ 的 subtype，边关系继承自 $G$ 。 $S$ 可以是空集，也可以有一个或两个顶点；定义中没有其他条件。

P3Factor：对有限类型 $V$ 上的简单图 $G$ ，一个 P3Factor G 对象是一个结构，包含一个自然数 $b$ （字段 blockCount）、一个从 $Fin\,b×Fin\,3$ 到 $V$ 的双射 $place$ ，以及对每个 $i∈Fin\,b$ 的两条边条件： $place(i,0)$ 与 $place(i,1)$ 在 $G$ 中相邻，且 $place(i,1)$ 与 $place(i,2)$ 在 $G$ 中相邻。双射覆盖所有 $V$ ，而 $b$ 没有单独的正性约束；除这两类边条件外，没有声明 $place(i,0)$ 与 $place(i,2)$ 必须相邻。

P3Path：对有限类型 $V$ 上的简单图 $G$ ，一个 P3Path G 对象包含三个顶点 left、center、right∈V，并包含 $left≠center$ 、 $center≠right$ 、 $left≠right$ 三个两两不等条件，以及 $G.Adj\;left\;center$ 和 $G.Adj\;center\;right$ 两个邻接条件；没有声明 $left$ 与 $right$ 之间必须有边。

eraseP3：给有限类型 $V$ 上的简单图 $G$ 和一个 P3Path G 对象 $L$ ，eraseP3 G L 是定义在 subtype $\{v∈V ∣ v≠L.left ∧ v≠L.center ∧ v≠L.right\}$ 上的简单图；其边关系是 $G$ 在这些剩余顶点上的诱导边关系。该定义只按三个不等条件筛除顶点。

ClaimZ1：ClaimZ1 是一个全称命题：对每个小类型 $W$ （即 Type 中的类型）及其 Fintype W 实例、每个定义在 $W$ 上的简单图 $G$ ，如果每个顶点的 $G$ 邻居数为 $3$ ，且 $4≤Fintype.card W$ 并且删除任意满足 $S.card≤2$ 的有限子集 $S⊆W$ 后所得诱导图连通，且 $Fintype.card W$ 除以 $6$ 的自然数余数为 $0$ ，那么存在某个自然数 $b$ 、一个双射 $place:Fin\,b×Fin\,3≃W$ ，使得对每个 $i∈Fin\,b$ ， $place(i,0)$ 与 $place(i,1)$ 相邻且 $place(i,1)$ 与 $place(i,2)$ 相邻。这里邻居数就是满足 $G.Adj v w$ 的 $w$ 的 subtype 的自然数基数；所有 $W$ 、其有限性实例和 $G$ 都在全称量化范围内。

ClaimZ8：ClaimZ8 先对每个小类型 $W$ 及其 Fintype W 实例、每个简单图 $G$ 作与 ClaimZ1 相同的三个前提：每个顶点有恰好 $3$ 个邻居， $4≤Fintype.card W$ 且对所有 $S⊆W$ 的有限子集只要 $S.card≤2$ 就有相应诱导图连通，并且 $Fintype.card W$ 除以 $6$ 的余数为 $0$ ；在这些前提下，它还要求对每个指定的三元路径 $L$ ——即三个两两不同的顶点 left、center、right，其中 left 与 center 相邻且 center 与 right 相邻——都存在某个自然数 $b$ 和双射 $Fin\,b×Fin\,3≃\{v∈W ∣ v≠L.left ∧ v≠L.center ∧ v≠L.right\}$ ，并且每个块的前两对位置分别在从 $G$ 诱导出的剩余顶点图中相邻。若没有这样的 $L$ ，这个内层全称条件为空真。

TwoFactor：对同一有限顶点类型 $V$ 上的两个简单图 $G$ 、 $F$ ，TwoFactor G F 是命题：对所有 $x,y∈V$ ，若 $F$ 在 $x,y$ 之间有边则 $G$ 也有边，并且对每个 $v∈V$ ，满足 $F.Adj v w$ 的 $w$ 的数量恰好为 $2$ 。定义没有额外的连通性条件；“spanning”只由 $F$ 与 $G$ 使用同一个顶点类型体现。

componentOrder：对有限类型 $V$ 上的简单图 $F$ 和顶点 $v∈V$ ，componentOrder F v 是所有能从 $v$ 在 $F$ 中到达的顶点 $w∈V$ 所组成的 subtype 的自然数基数，即 $Nat.card(\{w : V ∣ F.Reachable v w\})$ ；可达关系包含从 $v$ 到自身的零长度路径。

DivisibleTwoFactor：对同一有限顶点类型 $V$ 上的简单图 $G$ 、 $F$ ，DivisibleTwoFactor G F 要求同时满足：对所有 $x,y$ ， $F$ 的边都是 $G$ 的边；对每个 $v$ ， $F$ 恰有两个邻居；并且对每个 $v$ ，在 $F$ 中从 $v$ 可达的顶点数量是 $3$ 的倍数，即存在自然数 $k$ 使该数量等于 $3·k$ 。没有额外的非空或连通性条件；若 $V$ 为空，所有顶点量化的条件为空真。

HasDivisibleTwoFactor：对有限类型 $V$ 上的简单图 $G$ ，HasDivisibleTwoFactor G 表示存在某个定义在同一顶点类型 $V$ 上的简单图 $F$ ，使得每条 $F$ 边也是 $G$ 的边、每个顶点在 $F$ 中有恰好两个邻居，并且每个顶点在 $F$ 中的可达分支大小都是 $3$ 的倍数。存在性不要求该 $F$ 唯一，也没有单独的非空条件。

PerfectMatching：对有限类型 $V$ 上的简单图 $G$ 、 $M$ ，PerfectMatching G M 表示每条 $M$ 边也是 $G$ 的边，并且对每个 $v∈V$ ，满足 $M.Adj v w$ 的 $w$ 的数量恰好为 $1$ 。它没有额外的唯一性、连通性或非空顶点条件；当顶点类型为空时，顶点量化条件为空真。

matchingComplement：对同一有限顶点类型 $V$ 上的简单图 $G$ 、 $M$ ，matchingComplement G M 是图 $C=G⊓Mᶜ$ ；对任意 $x,y∈V$ ， $C$ 在 $x,y$ 之间有边当且仅当 $G$ 在 $x,y$ 之间有边且 $M$ 在 $x,y$ 之间没有边。这里取的是 $M$ 的补图与 $G$ 的边交集；该定义本身没有把 $M≤G$ 作为前提。

HasDivisibleComplement：对有限类型 $V$ 上的简单图 $G$ ，HasDivisibleComplement G 表示存在某个简单图 $M$ 定义在 $V$ 上，使得每条 $M$ 边都是 $G$ 的边、每个顶点恰有一个 $M$ 邻居，并且令 $C$ 为满足 $x∼_C y$ 当且仅当 $x∼_G y$ 且不满足 $x∼_M y$ 的图后， $C$ 的每条边也是 $G$ 的边、每个顶点在 $C$ 中恰有两个邻居，而且对每个顶点 $v$ ，在 $C$ 中从 $v$ 可达的顶点数量是 $3$ 的倍数。这里的 $C≤G$ 条件属于 DivisibleTwoFactor 的展开内容， $M$ 只要求存在而不要求唯一。

brickEdges：brickEdges 是一个由自然数有序对组成的列表，且其完整顺序为 $(0,1),(0,5),(1,2),(1,6),(2,3),(2,7),(3,8),(4,6),(4,7),(5,7),(5,8),(6,8)$ 。

forwardEdge：对任意 $q,u,v∈ℕ$ ，forwardEdge q u v 当且仅当以下五个条件至少一个成立： $(u,v)$ 属于上述十二个有序对的列表；或者 $9≤u$ 且 $v=u+1$ 或 $v=u+(6q+5)$ ；或者 $u=0$ 且 $v=9$ ；或者 $u=3$ 且 $v=17+12q$ ；或者 $u=4$ 且 $v=13+6q$ 。该谓词自身没有 $u≠v$ 条件，也没有要求 $u$ 、 $v$ 落在任何有限范围内。

H：对每个 $q∈ℕ$ ，H q 是顶点类型为 $Fin(18+12q)$ 的简单图。令 $D_q(a,b)$ 表示对自然数 $a,b$ 成立的 forwardEdge q a b 条件，并将其完全展开为

(a,b)∈[(0,1),(0,5),(1,2),(1,6),(2,3),(2,7),(3,8),(4,6),(4,7),(5,7),(5,8),(6,8)] ∨ (9≤a ∧ (b=a+1 ∨ b=a+(6q+5))) ∨ (a=0 ∧ b=9) ∨ (a=3 ∧ b=17+12q) ∨ (a=4 ∧ b=13+6q)。

对任意 $u,v∈Fin(18+12q)$ ， $u$ 与 $v$ 相邻当且仅当 $u≠v$ 且 $D_q(u.val,v.val)∨D_q(v.val,u.val)$ 。因此，算术条件只作用于这两个顶点的自然数值，除显示的条件外没有额外范围检查； $q=0$ 也在量化范围内。

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

Models for cubic-graph P3P_3P3​-factors and the C02 family

Models for cubic-graph $P_3$ -factors and the C02 family