Weak-pentagon edge labels, odd cycles, and the sixteen-vertex target
Definitionopg434_weak_pentagonThis module defines a symmetric five-label assignment on graph edges; values on nonedges are irrelevant. The assignment is weak-pentagon when deleting each one color class leaves a bipartite spanning graph. Properness and surjectivity are not required.
Simple cycles are cyclic lists of at least three distinct vertices and need not be induced. A color meets every odd cycle when some cyclically consecutive edge of each simple odd cycle has that color.
The module also fixes an explicit sixteen-vertex homomorphism target. Its vertices are the four-bit vectors, and two labels are related when their Hamming distance is exactly three or four. This is the four-bit model of the Clebsch graph used by the existence reformulation.
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Finset.Card
import Mathlib.Data.Set.Card
namespace OPG434
universe u
/-- A symmetric edge labeling. Values away from graph edges are irrelevant. -/
structure EdgeColoring {V : Type u} (G : SimpleGraph V) (K : Type*) where
color : V → V → K
color_symm : ∀ ⦃u v : V⦄, G.Adj u v → color u v = color v u
/-- The graph is finite, triangle-free, and every vertex has exactly three
neighbors. -/
def IsTriangleFreeCubic {V : Type u} (G : SimpleGraph V) : Prop :=
(∀ ⦃a b c : V⦄, G.Adj a b → G.Adj b c → ¬ G.Adj c a) ∧
∀ v : V, (G.neighborSet v).encard = 3
/-- After deleting one color class, the remaining spanning graph is
bipartite, witnessed by a Boolean side assignment. -/
def ComplementOfColorIsBipartite {V : Type u} {G : SimpleGraph V}
(c : EdgeColoring G (Fin 5)) (i : Fin 5) : Prop :=
∃ side : V → Bool,
∀ ⦃u v : V⦄, G.Adj u v → c.color u v ≠ i → side u ≠ side v
/-- The weak-pentagon five-color condition. No properness or surjectivity is
required. -/
def IsWeakPentagonColoring {V : Type u} {G : SimpleGraph V}
(c : EdgeColoring G (Fin 5)) : Prop :=
∀ i : Fin 5, ComplementOfColorIsBipartite c i
def HasWeakPentagonColoring {V : Type u} (G : SimpleGraph V) : Prop :=
∃ c : EdgeColoring G (Fin 5), IsWeakPentagonColoring c
/-- A simple cycle encoded by a nonempty cyclic list of distinct vertices. -/
def IsCycleList {V : Type u} (G : SimpleGraph V) (vs : List V) : Prop :=
∃ x y : V, ∃ middle : List V,
vs = x :: (middle ++ [y]) ∧ 3 ≤ vs.length ∧
vs.Nodup ∧ vs.Chain' G.Adj ∧ G.Adj y x
/-- Two vertices occur consecutively in the cyclic order of `vs`. -/
def ConsecutiveInCycle {V : Type u} (vs : List V) (x y : V) : Prop :=
(∃ before after : List V, vs = before ++ x :: y :: after) ∨
(vs.head? = some y ∧ vs.getLast? = some x)
/-- Color `i` meets every simple odd cycle of `G`. -/
def ColorMeetsEveryOddCycle {V : Type u} {G : SimpleGraph V}
(c : EdgeColoring G (Fin 5)) (i : Fin 5) : Prop :=
∀ vs : List V, IsCycleList G vs → (∃ m : ℕ, vs.length = 2 * m + 1) →
∃ x y : V, ConsecutiveInCycle vs x y ∧ c.color x y = i
/-- Four-bit labels; this type has sixteen elements. -/
abbrev Bit4 := Fin 4 → Bool
def hammingDistance (x y : Bit4) : ℕ :=
(Finset.univ.filter fun i => x i ≠ y i).card
/-- The explicit sixteen-vertex target relation: Hamming distance three or
four. It is an even-coordinate model of the Clebsch graph. -/
def HasClebsch16Homomorphism {V : Type u} (G : SimpleGraph V) : Prop :=
∃ f : V → Bit4,
∀ ⦃u v : V⦄, G.Adj u v →
hammingDistance (f u) (f v) = 3 ∨ hammingDistance (f u) (f v) = 4
end OPG434Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
EdgeColoring. For a type of vertices V, a simple graph G on V, and a type K, an edge coloring consists of a function assigning an element of K to every ordered pair of vertices, together with the requirement that adjacent vertices u and v receive equal values in both orders. No condition is imposed on nonedges. IsTriangleFreeCubic. A simple graph G on V satisfies this predicate exactly when, for all vertices a, b, and c, adjacency of a to b and b to c implies that c is not adjacent to a, and every vertex v has neighbor set of cardinality exactly 3. ComplementOfColorIsBipartite. Given an edge coloring c of G with values in a five-element type Fin 5 and a color i, this predicate says that there exists a Boolean assignment to the vertices such that every edge whose color is not i has endpoints assigned different Boolean values. Edges of color i are unrestricted by this condition. IsWeakPentagonColoring. An edge coloring c with five possible colors satisfies this predicate when the preceding Boolean-side condition holds separately for every i in Fin 5. HasWeakPentagonColoring. A graph G has this property when there exists an edge coloring c with five possible colors that satisfies IsWeakPentagonColoring. IsCycleList. A list vs of vertices is a cycle list when there exist vertices x and y and a middle list such that vs is x followed by the middle list and then y, vs has length at least 3, all entries of vs are distinct, every consecutive pair in the listed order is adjacent in G, and y is adjacent to x. ConsecutiveInCycle. Vertices x and y are consecutive in a list vs when either vs can be written as an arbitrary prefix followed by x, then y, then an arbitrary suffix, or y is the first entry of vs and x is its last entry. ColorMeetsEveryOddCycle. For every list vs that is a cycle list and whose length equals 2m + 1 for some natural number m, there exist vertices x and y that are consecutive in the cyclic order of vs and whose edge-coloring value c.color x y equals i. Bit4. A four-bit label is a function from the four-element type Fin 4 to Bool, so there are sixteen possible labels. hammingDistance. The Hamming distance between two four-bit labels x and y is the cardinality of the set of the four coordinates at which x and y have different Boolean values. HasClebsch16Homomorphism. A graph G has this property when there exists a function f assigning a four-bit label to every vertex such that every adjacent pair u and v satisfies that the Hamming distance between f u and f v is exactly 3 or exactly 4.
Confirmed by the mission captain (proposal self-audit).