R03 P3-factor structural result: two-cycle residue bridge (dependency-clean)

Proved

CubicP3Partition.R03SP01TwoFactorTwoCycleP3FactorOfDivisibleOrderV2

by hao jia · Sep 20, 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.

Formalization Note The component supports carry their induced finite-type instances explicitly, matching the Lean statement. This V2 node removes an unavailable auxiliary import from the earlier platform target while preserving the same mathematical hypotheses and conclusion.

Preamble

import Definitions.Def_cubic_p3_partition_models

Formal statement

namespace CubicP3Partition

universe u

/--
A two-component two-factor residue bridge.  The hypotheses select two distinct
components covering the vertex set; total order divisibility and connectivity
then yield a spanning non-induced P3-factor.  This is a conditional lemma and
is not the unrestricted R03 root theorem.
-/
theorem R03SP01TwoFactorTwoCycleP3FactorOfDivisibleOrderV2
    {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; ProblemContract problem:opg-46613-p3-partition; dependency-clean V2 extraction of the candidate-only formalization.

View graph