R03 P3-factor structural result: local center balance
ProvedR03ChargeCandidateV3.local_center_balancegraph-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 R03ChargeCandidateV3.local_center_balance 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 78e42ec682d3f2cc891d1c7f40f749f1c43b7311534e23d1a4dce035fdbd8734.
Formal statement
import Mathlib.Data.Fin.VecNotation
import Definitions.Def_r03_defs_04051951db_v3_ChargePatterns
namespace R03ChargeCandidateV3
open R03ChargeCandidateV3
theorem local_center_balance : ∀ a b c : Fin 3,
(a.val + b.val + c.val) % 3 = 2 →
ins a b c + 1 = outs a b c + 3 * isCenter a b c := by sorry
end R03ChargeCandidateV3
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/v3_ChargePatterns.lean; source SHA-256 78e42ec682d3f2cc891d1c7f40f749f1c43b7311534e23d1a4dce035fdbd8734; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.