Matching cuts and immune high-girth graph packages
Definitionopg37364_matching_cutsThis module fixes finite simple-graph conventions for the cited paper. A matching cut is determined by a nonempty proper vertex shore and requires every vertex to have at most one neighbor across the resulting bipartition. An immune graph has no such cut.
A simple cycle is a cyclic list of at least three distinct vertices. Girth at least means every simple cycle has length at least , with forests satisfying every threshold. Connectedness uses nonempty graph reachability, bipartiteness uses a Boolean side assignment, and exact regularity counts each neighbor set.
A perfect matching is represented by an adjacent involution on vertices. The combined package requires connectedness, bipartiteness, degree fourteen, the girth bound, absence of matching cuts, and a perfect matching.
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Logic.Relation
import Mathlib.Data.Set.Card
namespace OPG37364
universe u
/-- A simple cycle encoded by a 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
/-- Every simple cycle has length at least `g`; forests satisfy this for every
`g`. -/
def HasGirthAtLeast {V : Type u} (G : SimpleGraph V) (g : ℕ) : Prop :=
∀ vs : List V, IsCycleList G vs → g ≤ vs.length
/-- Boolean bipartiteness witness. -/
def IsBipartite {V : Type u} (G : SimpleGraph V) : Prop :=
∃ side : V → Bool, ∀ ⦃u v : V⦄, G.Adj u v → side u ≠ side v
/-- Nonempty connectedness under graph reachability. -/
def IsConnected {V : Type u} (G : SimpleGraph V) : Prop :=
Nonempty V ∧ ∀ u v : V, Relation.ReflTransGen G.Adj u v
/-- A nontrivial shore `A` defines a matching cut when every vertex has at
most one neighbor across the cut. -/
def IsMatchingCut {V : Type u} (G : SimpleGraph V) (A : Set V) : Prop :=
A.Nonempty ∧ Aᶜ.Nonempty ∧
∀ ⦃v x y : V⦄,
G.Adj v x → ((v ∈ A ∧ x ∉ A) ∨ (v ∉ A ∧ x ∈ A)) →
G.Adj v y → ((v ∈ A ∧ y ∉ A) ∨ (v ∉ A ∧ y ∈ A)) → x = y
def HasMatchingCut {V : Type u} (G : SimpleGraph V) : Prop :=
∃ A : Set V, IsMatchingCut G A
/-- Every vertex has exactly `d` neighbors. -/
def IsRegularOfDegree {V : Type u} (G : SimpleGraph V) (d : ℕ) : Prop :=
∀ v : V, (G.neighborSet v).encard = d
/-- A perfect matching represented by a fixed-point-free adjacent involution.
Fixed-point-freeness follows from looplessness and adjacency. -/
def HasPerfectMatching {V : Type u} (G : SimpleGraph V) : Prop :=
∃ mate : V → V,
(∀ v : V, G.Adj v (mate v)) ∧ Function.Involutive mate
/-- The graph package asserted by Lemma 5 of Feghali--Lucke--Paulusma--Ries. -/
def IsImmuneHighGirthPackage {V : Type u} (G : SimpleGraph V) (g : ℕ) : Prop :=
IsConnected G ∧ IsBipartite G ∧ IsRegularOfDegree G 14 ∧
HasGirthAtLeast G g ∧ ¬ HasMatchingCut G ∧ HasPerfectMatching G
end OPG37364Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
IsCycleList. For a simple graph G on a vertex type V and a list vs of vertices, vs is a cycle list if there exist vertices x and y and a list middle such that vs consists of x followed by middle and then y, vs has length at least 3, its entries are pairwise distinct, every consecutive pair is adjacent in G, and y is adjacent to x. HasGirthAtLeast. For a natural number g, every cycle list vs in G has length at least g; if G has no cycle lists, this condition holds vacuously. IsBipartite. There exists a function side assigning each vertex one of the two Boolean values such that adjacent vertices receive different values. IsConnected. V is nonempty, and for every vertices u and v there is a finite graph walk from u to v, allowing a walk of length zero. IsMatchingCut. A subset A of V is nonempty, its complement V ∖ A is nonempty, and for every vertex v, any two neighbors x and y of v that lie on the opposite side of the partition determined by A are equal. HasMatchingCut. There exists a subset A that is a matching cut. IsRegularOfDegree. Every vertex v has a neighbor set of cardinality exactly d, where d is a natural number. HasPerfectMatching. There exists a function mate from V to V such that every vertex v is adjacent to mate(v) and mate(mate(v)) = v. Since the graph has no loops, each chosen mate is distinct from its vertex. IsImmuneHighGirthPackage. G is connected, bipartite, regular of degree 14, has girth at least g, has no matching cut, and has a perfect matching, with each of these terms having the meanings given above.
Confirmed by the mission captain (proposal self-audit).