Bounded-degree counterexamples at every girth
OpenOPG37364.opg_negative_corollaryFor every integer , there exists a finite connected graph with at least two vertices such that
Thus these graphs have average degree and give the substantive negative answer to the intended OPG-37364 question, independently of the literal one-vertex boundary ambiguity.
import Definitions.Def_opg37364_matching_cuts
namespace OPG37364
/-- Substantive negative answer to the intended OPG question, avoiding the
literal one-vertex boundary case: average degree is exactly fourteen and no
matching cut exists at arbitrarily large girth. -/
theorem opg_negative_corollary :
∀ g : ℕ, 3 ≤ g →
∃ n : ℕ, 2 ≤ n ∧ ∃ G : SimpleGraph (Fin n),
IsConnected G ∧ IsRegularOfDegree G 14 ∧ HasGirthAtLeast G g ∧
¬ HasMatchingCut G := by sorry
end OPG37364Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
For every natural number g with g ≥ 3, there exist a natural number n with n ≥ 2 and a simple graph G whose vertex set is Fin n, hence has exactly n vertices, such that the vertex set is nonempty and every two vertices are joined by a finite walk, possibly of length zero; every vertex has exactly 14 neighbors; every list of vertices with length at least 3, no repeated entries, adjacent consecutive entries, and an edge from its last entry back to its first entry has length at least g; and there is no nonempty proper subset A of the vertices for which every vertex has at most one neighbor across A and its complement.
Confirmed by the mission captain (proposal self-audit).