Prove2Me

C02: the 18+12q18+12q route-obstruction family

Proved
CubicP3Partition.c02_obstruction_family

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

combinatoricscubic-graphsgraph-theoryp3-factor

For every natural number qq, including q=0q=0, the explicitly defined graph HqH_q on 18+12q18+12q vertices is cubic and 3-vertex-connected, has a noninduced P3P_3-factor, and has no perfect matching whose complementary 2-factor has all component orders divisible by three:

∀q∈N,Cubic⁡(Hq)∧ThreeVertexConnected⁡(Hq)∧Nonempty⁡(P3Factor⁡(Hq))∧¬HasDivisibleComplement⁡(Hq).\forall q\in\mathbb N,\quad \operatorname{Cubic}(H_q)\land\operatorname{ThreeVertexConnected}(H_q)\land \operatorname{Nonempty}(\operatorname{P3Factor}(H_q))\land \neg\operatorname{HasDivisibleComplement}(H_q).

The family therefore separates the main conclusion from the stronger matching route. It does not refute OPG-46613. The cited repository currently classifies the family as candidate-only; this theorem is the outstanding full formalization target.

Preamble
import Definitions.Def_cubic_p3_partition_models
Formal statement
namespace CubicP3Partition

/-- The full C02 candidate family separates P3-factors from the strengthened matching route. -/
theorem c02_obstruction_family :
    ∀ q : Nat, Cubic (H q) ∧ ThreeVertexConnected (H q) ∧
      Nonempty (P3Factor (H q)) ∧ ¬ HasDivisibleComplement (H q) := by sorry

end CubicP3Partition
Source
Vibe Mathing C02, https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.md, Sections C02.1–C02.2; independent verifier report at https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c08-independent-verifier/verifier-report.md, Sections 6–7; fixed revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a.
Read-back

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

对每个自然数 qq（包括 q=0q=0），令 Vq=Fin(18+12q)V_q=Fin(18+12q)，并令 KqK_q 为 H q：对 u,v∈Vqu,v∈V_q，u∼Kqvu∼_{K_q}v 当且仅当 u≠vu≠v 且 Dq(u.val,v.val)∨Dq(v.val,u.val)D_q(u.val,v.val)∨D_q(v.val,u.val)，其中对自然数 a,ba,b，Dq(a,b)D_q(a,b) 当且仅当 (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)(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))9≤a∧(b=a+1∨b=a+(6q+5))，或 a=0∧b=9a=0∧b=9，或 a=3∧b=17+12qa=3∧b=17+12q，或 a=4∧b=13+6qa=4∧b=13+6q。对每个这样的 qq，定理声明以下四个命题的合取：每个 v∈Vqv∈V_q 有恰好 33 个 KqK_q 邻居；4≤Fintype.cardVq4≤Fintype.card V_q 且对每个有限子集 S⊆VqS⊆V_q，只要 S.card≤2S.card≤2，KqK_q 在满足 v∉Sv∉S 的 subtype 上的诱导图就连通；存在自然数 bb 和双射 Fin b×Fin 3≃VqFin\,b×Fin\,3≃V_q，且对每个 i∈Fin bi∈Fin\,b，place(i,0)place(i,0) 与 place(i,1)place(i,1) 相邻、place(i,1)place(i,1) 与 place(i,2)place(i,2) 相邻；并且不存在简单图 MM 使 MM 的每条边都是 KqK_q 的边、每个顶点有恰好一个 MM 邻居，且令 CMC_M 为 KqK_q 中不属于 MM 的边所成的图后，CM≤KqC_M≤K_q、每个顶点有恰好两个 CMC_M 邻居、每个 CMC_M 中的可达分支大小都被 33 整除。这里全称量化的是所有 q∈Nq∈ℕ，而不是某个固定的正数 qq；有限子集量化仍包括空集。

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