R03 P3-factor structural result: even order of cubic
ProvedR03SP03CubicOrderParity.even_order_of_cubicgraph-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 R03SP03CubicOrderParity.even_order_of_cubic 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 993dd93dbc2475a3d52be6cd7b88906b457f99a9d73e78d2c9c085936b347e86.
Formal statement
import Mathlib
import Definitions.Def_cubic_p3_partition_models
namespace R03SP03CubicOrderParity
open R03SP03CubicOrderParity
open CubicP3Partition
universe u
theorem even_order_of_cubic
{V : Type u} [Fintype V] {G : SimpleGraph V}
(hCubic : Cubic G) :
Even (Fintype.card V) := by sorry
end R03SP03CubicOrderParity
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp03/r03-sp03-cubic-order-parity-v1.lean; source SHA-256 993dd93dbc2475a3d52be6cd7b88906b457f99a9d73e78d2c9c085936b347e86; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.