R03 P3-factor structural result: port swaps
ProvedR03DiamondCover.port_swapsgraph-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 R03DiamondCover.port_swaps 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 5aab1a44028750d73cefba297986bf5646c6c399e6f7aac27a9e508d3c5a5c9b.
Formal statement
import Mathlib.Data.Fin.VecNotation
import Definitions.Def_r03_defs_09e80204d5_R03DiamondCover_v1
namespace R03DiamondCover
open R03DiamondCover
theorem port_swaps : ∀ a b c d : Fin 3,
(Diamond a b c d ↔ Diamond b a c d) ∧
(Diamond a b c d ↔ Diamond a b d c) := by sorry
end R03DiamondCover
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/R03DiamondCover_v1.lean; source SHA-256 5aab1a44028750d73cefba297986bf5646c6c399e6f7aac27a9e508d3c5a5c9b; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.