R03 P3-factor structural result: R03SP01TwoFactorTwoCycleP3FactorOfDivisibleOrder

Proved

CubicP3Partition.R03SP01TwoFactorTwoCycleP3FactorOfDivisibleOrder

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

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

This is a source-faithful conditional lemma from the formalization of the cubic P3-partition problem. Let $G$ be a finite simple graph and let $F$ be a spanning 2-factor of $G$ . Choose two distinct connected components $c_A$ and $c_B$ of $F$ whose supports cover all vertices of $G$ . If $|V(G)|$ is divisible by $3$ and $G$ is connected, then $G$ has a spanning non-induced $P_3$ -factor.

The result is a reusable two-component residue bridge. It does not assert that an arbitrary cubic 3-connected graph has a two-component 2-factor, and it does not close the unrestricted R03 root problem.

Retirement Note The original platform node depended on an auxiliary definition import that is unavailable to the server compiler. It is retained as a reversible deprecated record; the dependency-clean replacement is CubicP3Partition.R03SP01TwoFactorTwoCycleP3FactorOfDivisibleOrderV2.

Formal statement

import Definitions.Def_cubic_p3_partition_models
import Definitions.Def_r03_defs_f035323056_r03_sp01_two_factor_two_cycle_component_bridge_c

namespace CubicP3Partition

open CubicP3Partition
open SimpleGraph
universe u
theorem R03SP01TwoFactorTwoCycleP3FactorOfDivisibleOrder
    {V : Type u} [Fintype V]
    (G F : SimpleGraph V)
    (hTF : TwoFactor G F)
    (cA cB : F.ConnectedComponent)
    (hneq : cA ≠ cB)
    (hcover : ∀ v : V, v ∈ cA.supp ∨ v ∈ cB.supp)
    [Fintype cA.supp] [Fintype cB.supp]
    (horder : 3 ∣ Fintype.card V)
    (hconn : G.Connected) :
    Nonempty (P3Factor G) := by sorry

end CubicP3Partition

Source

VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp01/r03-sp01-two-factor-two-cycle-component-bridge-candidate-v5.lean; source SHA-256 facf51a838332f4e44d7c4f3c0bfd66f0c194af23419ca52fca247873e3554bc; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.

View graph