The structure and peripheral cycles of the fixed graph
ProvedOPG500Counterexample.eight_vertex_graph_structurecombinatoricsformalizationgeodesicsgraph-theory
For the fixed eighteen-edge graph on eight vertices:
- is 3-connected: it has at least four vertices and deletion of any set of fewer than three vertices leaves a connected induced graph.
- A simple cycle of is peripheral if and only if its vertex set is one of the twelve triples frozen in
peripheralTriples.
Thus the theorem classifies every cycle of , not only the four triangles contained in the core.
Preamble
import Definitions.Def_opg500_eight_vertex_graph
Formal statement
namespace OPG500Counterexample
/-- The fixed graph is 3-connected, and its peripheral cycles are exactly the
twelve frozen apex triangles, classified by their vertex sets. -/
theorem eight_vertex_graph_structure :
IsThreeConnected H ∧
∀ C : Cycle H,
C.IsPeripheral ↔ C.walk.support.toFinset ∈ peripheralTriples := by sorry
end OPG500CounterexampleSource
Candidate C10, graph and peripheral-cycle classification: https://github.com/vibemathing/problem-opg-500-geodesic-cycles/blob/a41fe59b4535851ea55f6e868e938b9aaf81e924/research/artifacts/candidates/opg500-a01-c10/tight-rank.md
Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
For the graph on vertices with edge set , the graph has at least four vertices and deleting any set of fewer than three vertices leaves a connected induced graph. Moreover, for every cycle of , is chordless and its outside induced subgraph is connected or empty if and only if the finite set of vertices occurring in is one of
Human review
Confirmed by the mission captain (proposal self-audit).