Lemma 5: immune 14-regular bipartite graphs of arbitrary girth
OpenOPG37364.immune_high_girth_graphsFor every integer , there exists a finite connected bipartite graph with at least two vertices such that
and contains a perfect matching. The graph may depend on . This is the structural existence theorem stated as Lemma 5 in the cited paper.
import Definitions.Def_opg37364_matching_cuts
namespace OPG37364
/-- Feghali--Lucke--Paulusma--Ries, Lemma 5: immune 14-regular bipartite
graphs with arbitrarily large prescribed girth and a perfect matching. -/
theorem immune_high_girth_graphs :
∀ g : ℕ, 3 ≤ g →
∃ n : ℕ, 2 ≤ n ∧ ∃ G : SimpleGraph (Fin n),
IsImmuneHighGirthPackage G 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 all of the following hold: the vertex set is nonempty and every two vertices are joined by a finite walk, possibly of length zero; there is a Boolean assignment to the vertices giving different values to the endpoints of every edge; 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; there is no nonempty proper subset A of the vertices for which every vertex has at most one neighbor across the partition into A and its complement; and there is a function mate on the vertices such that every vertex is adjacent to its mate and applying mate twice returns the original vertex.
Confirmed by the mission captain (proposal self-audit).