R03 P3-factor structural result: no unique neighbor of connected cut free
ProvedR03SP06.no_unique_neighbor_of_connected_cut_freegraph-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.no_unique_neighbor_of_connected_cut_free 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 ed046b7ee631aee2f744b8d209ab9c8f4528c5406822f106b3411e682e12e2a9.
Formal statement
import Mathlib
import Definitions.Def_cubic_p3_partition_models
namespace R03SP06
open R03SP06
variable {V : Type} [Fintype V] [DecidableEq V]
theorem no_unique_neighbor_of_connected_cut_free
{G : SimpleGraph V}
(hcard : 3 ≤ Fintype.card V)
(hconn : G.Connected)
(hcut : ∀ x : V, (G.induce {v : V | v ≠ x}).Connected) :
¬ ∃ v u : V, G.Adj v u ∧ ∀ w : V, G.Adj v w → w = u := by sorry
end R03SP06
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp06/no_cut_vertex_min_degree_two.lean; source SHA-256 ed046b7ee631aee2f744b8d209ab9c8f4528c5406822f106b3411e682e12e2a9; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.