R03 P3-factor structural result: cubic three connected has perfect matching
ProvedR03PerfectMatchingCandidate.cubic_three_connected_has_perfect_matchinggraph-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 R03PerfectMatchingCandidate.cubic_three_connected_has_perfect_matching 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 1e67fc5e7a242895e94a4bf5b396f3b143d7004721b08f2910a424ad0abec2e5.
Formal statement
import Mathlib
import Definitions.Def_cubic_p3_partition_models
namespace R03PerfectMatchingCandidate
open R03PerfectMatchingCandidate
open CubicP3Partition
open SimpleGraph
open scoped BigOperators
universe u
variable {V : Type u} [Fintype V]
theorem cubic_three_connected_has_perfect_matching
{G : SimpleGraph V} (hG : Cubic G) (hconn : ThreeVertexConnected G)
(hEven : Even (Nat.card V)) :
∃ M : G.Subgraph, M.IsPerfectMatching := by sorry
end R03PerfectMatchingCandidate
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp01/r03-sp01-cubic-three-connected-perfect-matching-candidate-v1.lean; source SHA-256 1e67fc5e7a242895e94a4bf5b396f3b143d7004721b08f2910a424ad0abec2e5; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.