R03 P3-factor structural result: cubic three dvd implies six dvd
ProvedR03SP06Arithmetic.cubic_three_dvd_implies_six_dvdgraph-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 R03SP06Arithmetic.cubic_three_dvd_implies_six_dvd 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 bf2eb6b8104f68128595b7363eb5e689c65693bde4ca787df0ce29b4d8d2aea9.
Formal statement
import Mathlib
import Definitions.Def_cubic_p3_partition_models
namespace R03SP06Arithmetic
open R03SP06Arithmetic
open CubicP3Partition
universe u
variable {V : Type u} [Fintype V]
theorem cubic_three_dvd_implies_six_dvd {G : SimpleGraph V}
(hC : Cubic G) (h3 : 3 ∣ Fintype.card V) :
6 ∣ Fintype.card V := by sorry
end R03SP06Arithmetic
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp06/cubic_even_six_divisibility.lean; source SHA-256 bf2eb6b8104f68128595b7363eb5e689c65693bde4ca787df0ce29b4d8d2aea9; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.