R03 P3-factor structural result: leaf masks cover
ProvedR03FiniteBoundaryV5.leaf_masks_covergraph-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 R03FiniteBoundaryV5.leaf_masks_cover 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 920f597d8703fc721fa3bb584dc732a7d917be807c0ef93322ca5c957a5b5b8b.
Formal statement
import Mathlib.Data.Fin.VecNotation import Definitions.Def_r03_defs_308a4c5b4d_v5_FiniteBoundary namespace R03FiniteBoundaryV5 open R03FiniteBoundaryV5 theorem leaf_masks_cover : ∀ m : Fin 32, ones m.val ≤ 2 → ∃ i : Fin 16, leafMasks i = m.val := by sorry end R03FiniteBoundaryV5
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/v5_FiniteBoundary.lean; source SHA-256 920f597d8703fc721fa3bb584dc732a7d917be807c0ef93322ca5c957a5b5b8b; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.