R03 P3-factor structural result: R03SP01ThreeOneAdjacentCenter

Proved

CubicP3Partition.R03SP01ThreeOneAdjacentCenter

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

graph-theoryopg-46613p3-factorsource-faithful-candidate

This is a source-faithful auxiliary theorem from the candidate formalization of the cubic P3-partition problem. It records the structural result CubicP3Partition.R03SP01ThreeOneAdjacentCenter under exactly the explicit hypotheses in the Lean statement. It is a conditional reusable result and does not claim that the open root problem has been solved.

Formalization Note The Lean statement and direct proof were extracted from the cited candidate artifact; its source digest is 4172635da798f59d33ef3d0760884b0adb816f2efd90989a67cc3459df668509.

Formal statement

import Definitions.Def_cubic_p3_partition_models
import Definitions.Def_r03_defs_70d95c7a2a_r03_sp01_three_one_adjacent_center_candidate_v1

namespace CubicP3Partition

open CubicP3Partition
universe u
open SimpleGraph
theorem R03SP01ThreeOneAdjacentCenter
    {A B C : Type u} [Fintype A] [Fintype B] [Fintype C]
    (G : SimpleGraph (A ⊕ (B ⊕ C)))
    (kA kB kC : Nat)
    (eA : Fin (1 + kA * 3) ≃ A)
    (eB : Fin (1 + kB * 3) ≃ B)
    (eC : Fin (1 + kC * 3) ≃ C)
    (cycleA : ∀ i : Fin (1 + kA * 3),
      G.Adj (Sum.inl (eA i))
        (Sum.inl (eA ⟨(i.val + 1) % (1 + kA * 3), Nat.mod_lt _ (by omega)⟩)))
    (cycleB : ∀ i : Fin (1 + kB * 3),
      G.Adj (Sum.inr (Sum.inl (eB i)))
        (Sum.inr (Sum.inl (eB ⟨(i.val + 1) % (1 + kB * 3), Nat.mod_lt _ (by omega)⟩))))
    (cycleC : ∀ i : Fin (1 + kC * 3),
      G.Adj (Sum.inr (Sum.inr (eC i)))
        (Sum.inr (Sum.inr (eC ⟨(i.val + 1) % (1 + kC * 3), Nat.mod_lt _ (by omega)⟩))))
    (hkA : 0 < kA)
    (hcrossAB : G.Adj (Sum.inl (eA ⟨0, by omega⟩))
      (Sum.inr (Sum.inl (eB ⟨0, by omega⟩))))
    (hcrossAC : G.Adj (Sum.inl (eA ⟨1, by omega⟩))
      (Sum.inr (Sum.inr (eC ⟨0, by omega⟩)))) :
    Nonempty (P3Factor G) := by sorry

end CubicP3Partition

Source

VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp01/r03-sp01-three-one-adjacent-center-candidate-v1.lean; source SHA-256 4172635da798f59d33ef3d0760884b0adb816f2efd90989a67cc3459df668509; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.

View graph