R03 P3-factor structural result: induced singleton connected
ProvedR03SP08NativeBridgeless.induced_singleton_connectedgraph-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 R03SP08NativeBridgeless.induced_singleton_connected 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 85e8d1e0a7cc8716acb1bde1a6acfee9603711caa68c4c78efff68f076ffe1a9.
Formal statement
import Mathlib
import Definitions.Def_cubic_p3_partition_models
import Definitions.Def_r03_defs_117d348ee0_SP08_NATIVE_BRIDGELESS_FROM_3CONN_CUBIC_v1
namespace R03SP08NativeBridgeless
open R03SP08NativeBridgeless
open CubicP3Partition
universe u
variable {V : Type u} [Fintype V]
theorem induced_singleton_connected {G : SimpleGraph V}
(hconn : ThreeVertexConnected G) (u : V) :
(G.induce {v : V | v ∉ ({u} : Finset V)}).Connected := by sorry
end R03SP08NativeBridgeless
Source
VibeMathing candidate artifact: research/artifacts/candidates/r03/parallel/sp08/SP08_NATIVE_BRIDGELESS_FROM_3CONN_CUBIC_v1.lean; source SHA-256 85e8d1e0a7cc8716acb1bde1a6acfee9603711caa68c4c78efff68f076ffe1a9; ProblemContract problem:opg-46613-p3-partition; candidate-only formalization.