R03 P3-factor structural result: sum binary eq filter card
ProvedR03SP06.sum_binary_eq_filter_cardgraph-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.sum_binary_eq_filter_card 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 98ce4a4c3c239d9dd23d20d4a42d6474480cc13c0457dbd7e5f33bc3788b6def.
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 sum_binary_eq_filter_card
{d : V → Nat}
(hbin : ∀ v, d v = 0 ∨ d v = 1)
(hsum : ∑ v, d v = 3) :
(Finset.filter (fun v => d v = 1) Finset.univ).card = 3 := by sorry
end R03SP06
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp06/q3_degree_pattern.lean; source SHA-256 98ce4a4c3c239d9dd23d20d4a42d6474480cc13c0457dbd7e5f33bc3788b6def; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.