R03 P3-factor structural result: q5 subcubic degree pattern

Proved

R03SP06.q5_subcubic_degree_pattern

by hao jia · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-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 R03SP06.q5_subcubic_degree_pattern 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 c56e9af6d273d654fb9b02b50785315e7280a3316a19a7b444e91043787c5a1f.

Formal statement

import Mathlib
import Definitions.Def_cubic_p3_partition_models

namespace R03SP06

open R03SP06
open CubicP3Partition
variable {V : Type} [Fintype V] [DecidableEq V]
theorem q5_subcubic_degree_pattern
    {G : SimpleGraph V}
    (hdeg : ∀ v, 1 ≤ degree G v ∧ degree G v ≤ 3)
    (hdef : ∑ v, (3 - degree G v) = 5) :
    2 * (Finset.filter (fun v => degree G v = 1) Finset.univ).card +
        (Finset.filter (fun v => degree G v = 2) Finset.univ).card = 5 ∧
      ((Finset.filter (fun v => degree G v = 1) Finset.univ).card = 0 ∧
          (Finset.filter (fun v => degree G v = 2) Finset.univ).card = 5 ∨
        (Finset.filter (fun v => degree G v = 1) Finset.univ).card = 1 ∧
          (Finset.filter (fun v => degree G v = 2) Finset.univ).card = 3 ∨
        (Finset.filter (fun v => degree G v = 1) Finset.univ).card = 2 ∧
          (Finset.filter (fun v => degree G v = 2) Finset.univ).card = 1) := by sorry

end R03SP06

Source

VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp06/q5_degree_pattern.lean; source SHA-256 c56e9af6d273d654fb9b02b50785315e7280a3316a19a7b444e91043787c5a1f; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.

View graph