Prove2Me

Cubic matching-complement bridge

Proved
CubicP3Partition.cubic_matching_complement_iff_two_factor

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

combinatoricscubic-graphsgraph-theoryp3-factor

Let GG be a finite simple cubic graph. Then GG has a perfect matching whose relative complement is a spanning 2-factor with every component order divisible by three if and only if GG has a spanning 2-factor with every component order divisible by three:

HasDivisibleComplement⁡(G)⟺HasDivisibleTwoFactor⁡(G).\operatorname{HasDivisibleComplement}(G) \quad\Longleftrightarrow\quad \operatorname{HasDivisibleTwoFactor}(G).

No connectivity or nonemptiness hypothesis is imposed. This bridge identifies the matching formulation of the strengthened route with its 2-factor formulation.

Preamble
import Definitions.Def_cubic_p3_partition_models
Formal statement
namespace CubicP3Partition

universe u

/-- In a cubic graph, divisible complementary perfect matchings and divisible 2-factors coincide. -/
theorem cubic_matching_complement_iff_two_factor
    {V : Type u} [Fintype V] (G : SimpleGraph V) (hCubic : Cubic G) :
    HasDivisibleComplement G ↔ HasDivisibleTwoFactor 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

对宇宙 uu 中的任意类型 VV（带有 Fintype V 实例）、任意定义在 VV 上的简单图 GG，以及假设 hCubic：对每个 v∈Vv∈V，满足 G.AdjvwG.Adj v w 的 ww 的自然数基数恰好为 33，定理声明以下两个命题等价。左侧是：存在一个简单图 MM 定义在 VV 上，使每条 MM 边都是 GG 的边且每个顶点在 MM 中恰有一个邻居；令 CMC_M 为满足 x∼CMyx∼_{C_M}y 当且仅当 x∼Gyx∼_G y 且不满足 x∼Myx∼_M y 的图，则每条 CMC_M 边都是 GG 的边、每个顶点在 CMC_M 中恰有两个邻居，并且对每个 v∈Vv∈V，在 CMC_M 中从 vv 可达的顶点数量是 33 的倍数。右侧是：存在一个简单图 FF 定义在 VV 上，使每条 FF 边都是 GG 的边、每个顶点在 FF 中恰有两个邻居，并且对每个 v∈Vv∈V，在 FF 中从 vv 可达的顶点数量是 33 的倍数。等价关系是双向的；除了有限性实例、图 GG 和 hCubic 外，没有连通性、阶数或非空性前提，因而也包括空的有限顶点类型情形。

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