OPG-434: the weak pentagon problem
OpenOPG434.root_problemEvery finite simple triangle-free cubic graph has an assignment of five labels to its edges such that deleting any one label leaves a bipartite spanning graph:
The labeling is not assumed proper or surjective. Cubic means every vertex has exactly three neighbors.
import Definitions.Def_opg434_weak_pentagon
namespace OPG434
universe u
/-- OPG-434: every finite simple triangle-free cubic graph has a five-edge
labeling whose five color-class complements are bipartite. -/
theorem root_problem
{V : Type u} [Fintype V] (G : SimpleGraph V)
(hG : IsTriangleFreeCubic G) :
HasWeakPentagonColoring G := by sorry
end OPG434Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
For a finite vertex type V, a simple graph G on V, and a hypothesis that for all vertices a, b, and c, adjacency of a to b and b to c implies that c is not adjacent to a, while every vertex has a neighbor set of cardinality exactly 3, the statement asserts that there exists an edge coloring c with five possible colors, symmetric on adjacent ordered pairs, such that for every color i in Fin 5 there is a Boolean assignment of the vertices for which every edge whose color is not i has endpoints assigned different Boolean values.
Confirmed by the mission captain (proposal self-audit).