A triangle-free graph of small degree on enough vertices has an induced 2K₂

General combinatorial lemma (reusable across n): if a vertex set D induces a triangle-free subgraph of G with every D-vertex having between 1 and 3 neighbours inside D, and |D| ≥ 7, then D contains an induced 2K₂ — two disjoint edges with no edges between them.

Reason: a 2K₂-free triangle-free graph with no isolated vertex is connected; among such graphs of maximum degree ≤ 3 the largest has exactly 7 vertices (a C₅-based extremal example exists, verified by exhaustive search; every such graph on ≥ 8 vertices contains an induced 2K₂). Hence |D| ≥ 8 forces an induced 2K₂.

NOTE: the threshold is 8, not 7 — there is an explicit triangle-free, max-degree-3, 2K₂-free graph on 7 vertices (containing an induced C₅).

theorem ACMax.exists_induced_2K2_of_triangleFree_smalldeg {V : Type u_1} [Fintype V] (G : SimpleGraph V) (D : Finset V) (htri : ∀ a ∈ D, ∀ b ∈ D, ∀ c ∈ D, ¬(G.Adj a b ∧ G.Adj b c ∧ G.Adj a c)) (hmin : ∀ a ∈ D, 1 ≤ (G.neighborFinset a ∩ D).card) (hmax : ∀ a ∈ D, (G.neighborFinset a ∩ D).card ≤ 3) (hcard : 8 ≤ D.card) : ∃ a ∈ D, ∃ b ∈ D, ∃ c ∈ D, ∃ d ∈ D, {a, b, c, d}.card = 4 ∧ G.Adj a b ∧ G.Adj c d ∧ ¬G.Adj a c ∧ ¬G.Adj a d ∧ ¬G.Adj b c ∧ ¬G.Adj b d

If D induces a triangle-free subgraph of G with in-D degrees in [1,3] and |D| ≥ 7, then D contains an induced 2K₂.