Five bipartite complements iff every color meets every odd cycle
ProvedOPG434.odd_cycle_equivalenceFor any finite simple graph and any fixed symmetric five-edge labeling, the following are equivalent:
The cycles need not be induced, and edge deletion retains all vertices. The equivalence does not require triangle-freeness, cubicity, properness, or use of every color.
import Definitions.Def_opg434_weak_pentagon
namespace OPG434
universe u
/-- Deleting every edge of one color is bipartite exactly when that color
meets every simple odd cycle. -/
theorem odd_cycle_equivalence
{V : Type u} [Fintype V] {G : SimpleGraph V}
(c : EdgeColoring G (Fin 5)) :
IsWeakPentagonColoring c ↔
∀ i : Fin 5, ColorMeetsEveryOddCycle c i := 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 an edge coloring c assigning one of five colors to every ordered vertex pair and assigning equal values in both orders on edges, the statement asserts the following equivalence. On one side, for every color i in Fin 5 there exists a Boolean assignment to the vertices such that every edge whose c-color is not i has endpoints on different Boolean sides. On the other side, for every i in Fin 5, every list vs with at least three distinct vertices, having the form of a listed cycle with each successive pair and the closing pair adjacent in G, and having odd length 2m + 1 for some natural number m, contains a cyclically consecutive pair x,y whose c-color equals i. Here cyclically consecutive means either x immediately precedes y in the list or x is the last entry and y is the first entry.
Confirmed by the mission captain (proposal self-audit).