R03 P3-factor structural result: p12PositionEquiv symm inr one
ProvedCubicP3Partition.p12PositionEquiv_symm_inr_onegraph-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 CubicP3Partition.p12PositionEquiv_symm_inr_one 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 2754267b0ebe3d53cfc7f5e2d10e4b0b5dbccef6bbd9182c690a0781ee4f8202.
Formal statement
import Definitions.Def_cubic_p3_partition_models
import Definitions.Def_r03_defs_5719a22c9e_R03CenterHall
namespace CubicP3Partition
open CubicP3Partition
universe u
variable {V : Type u}
theorem p12PositionEquiv_symm_inr_one (k : Nat) (i : Fin k) :
(p12PositionEquiv k).symm (Sum.inr (i, (1 : Fin 2))) = (i, (2 : Fin 3)) := by sorry
end CubicP3Partition
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/phase12/R03CenterHall.lean; source SHA-256 2754267b0ebe3d53cfc7f5e2d10e4b0b5dbccef6bbd9182c690a0781ee4f8202; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.