R03 P3-factor structural result: R03SP01TwoFactorTwoCycleP3FactorZeroZero
ProvedCubicP3Partition.R03SP01TwoFactorTwoCycleP3FactorZeroZerograph-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.R03SP01TwoFactorTwoCycleP3FactorZeroZero 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 e6f5bf4dedaacfe1b847fe0fe7538c6c9713641ff4f5e55d613d1d6c52541a85.
Formal statement
import Definitions.Def_cubic_p3_partition_models
import Definitions.Def_r03_defs_d5036bedfc_r03_sp01_two_factor_two_cycle_component_bridge_c
namespace CubicP3Partition
open CubicP3Partition
open SimpleGraph
universe u
theorem R03SP01TwoFactorTwoCycleP3FactorZeroZero
{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)
(kA kB : Nat)
[Fintype cA.supp] [Fintype cB.supp]
(hcardA : Fintype.card cA.supp = kA * 3)
(hcardB : Fintype.card cB.supp = kB * 3) :
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-v4.lean; source SHA-256 e6f5bf4dedaacfe1b847fe0fe7538c6c9713641ff4f5e55d613d1d6c52541a85; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.