R03 P3-factor structural result: project perfectMatching of subgraph
ProvedVibeMathingCampaign200.r03_sp03_petersen_matching_v1_project_perfectMatching_of_subgraphgraph-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 VibeMathingCampaign200.r03_sp03_petersen_matching_v1_project_perfectMatching_of_subgraph 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 746700599eaa51caa784403598568edc263268ad9d5a5a26c90cb6b02c3391b1.
Formal statement
import Mathlib
import Definitions.Def_cubic_p3_partition_models
namespace VibeMathingCampaign200
open CubicP3Partition
open scoped BigOperators
universe u
variable {V : Type u} [Fintype V]
variable {G : SimpleGraph V} [DecidableRel G.Adj]
variable {W : Type u} [Fintype W]
theorem r03_sp03_petersen_matching_v1_project_perfectMatching_of_subgraph
{G : SimpleGraph V} {M : G.Subgraph}
(hM : M.IsPerfectMatching) :
CubicP3Partition.PerfectMatching G M.spanningCoe := by sorry
end VibeMathingCampaign200
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp03/r03-sp03-petersen-matching-v1.lean; source SHA-256 746700599eaa51caa784403598568edc263268ad9d5a5a26c90cb6b02c3391b1; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.