Divisible 2-factors yield $P_3$ -factors

Proved

CubicP3Partition.divisible_two_factor_implies_p3_factor

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

combinatoricscubic-graphsgraph-theoryp3-factor

Let $G$ be any finite simple graph. If $G$ contains a spanning 2-regular subgraph $F$ such that every connected component of $F$ has order divisible by three, then $G$ has a noninduced $P_3$ -factor:

\operatorname{HasDivisibleTwoFactor}(G) \quad\Longrightarrow\quad \operatorname{Nonempty}(\operatorname{P3Factor}(G)).

Cubicity and connectivity are not assumptions. This is the formal target for the constructive implication used by the strengthened matching route.

Preamble

import Definitions.Def_cubic_p3_partition_models

Formal statement

namespace CubicP3Partition

universe u

/-- Split every component of a divisible 2-factor into three-vertex paths. -/
theorem divisible_two_factor_implies_p3_factor
    {V : Type u} [Fintype V] (G : SimpleGraph V)
    (h : HasDivisibleTwoFactor G) : Nonempty (P3Factor G) := by sorry

end CubicP3Partition

Source

Vibe Mathing C01, https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md, Section 2 (C01.1), fixed revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a.

Read-back

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

对宇宙 $u$ 中的任意有限类型 $V$ （带有 Fintype V 实例）和任意简单图 $G$ ，假设 h 表示存在一个简单图 $F$ 定义在同一顶点类型 $V$ 上，使每条 $F$ 边都是 $G$ 的边、每个顶点在 $F$ 中恰有两个邻居，并且每个顶点在 $F$ 中可达分支的顶点数是 $3$ 的倍数；则定理声明存在一个自然数 $b$ 和双射 $Fin\,b×Fin\,3≃V$ ，使得对每个 $i∈Fin\,b$ ， $place(i,0)$ 与 $place(i,1)$ 在 $G$ 中相邻，且 $place(i,1)$ 与 $place(i,2)$ 在 $G$ 中相邻。这里结论是存在至少一个这样的结构，不要求唯一；没有额外的 cubic、连通性或阶数假设，且 $h$ 中的所有顶点量化在空顶点类型上为空真。

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

Divisible 2-factors yield P3P_3P3​-factors

Divisible 2-factors yield $P_3$ -factors