Weak-pentagon colorings and the sixteen-vertex target
ProvedOPG434.clebsch16_equivalenceFor every finite simple graph , a weak-pentagon five-edge labeling exists exactly when has a homomorphism to the graph on four-bit vectors whose adjacent labels have Hamming distance three or four:
Both sides are existential. The conversion is not required to preserve an arbitrary previously chosen edge labeling or vertex map.
import Definitions.Def_opg434_weak_pentagon
namespace OPG434
universe u
/-- Existence of a weak-pentagon coloring is equivalent to a homomorphism to
the explicit sixteen-vertex Hamming-distance target. -/
theorem clebsch16_equivalence
{V : Type u} [Fintype V] (G : SimpleGraph V) :
HasWeakPentagonColoring G ↔ HasClebsch16Homomorphism 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 and any simple graph G on V, the statement asserts that the following are equivalent. There exists an edge coloring c with values in the five-element type Fin 5, symmetric on every edge, such that for each color i there is a Boolean assignment of the vertices making the endpoints of every edge not colored i lie on opposite sides. Equivalently, there exists a function f from vertices to the sixteen four-bit labels, with every edge mapped to a pair of labels differing in exactly 3 or exactly 4 of the four coordinates.
Confirmed by the mission captain (proposal self-audit).