3.3. An addable edge among three vertices
Let Q be a simple graph, let N = \{x, y, z\} \subseteq V(Q), and let
Q + vN be Q with a new vertex v joined to all of N. If Q + vN is
(2,2)-sparse and Q[N] is not a triangle, then some nonedge of Q with
both endpoints in N can be added while preserving (2,2)-sparsity.
(Zheng, 2026, Lemma 2.1)
Lean code for Lemma3.3.1●1 theorem
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Combinatorics/Sparse22/DegreeThreeAugmentation.leancomplete
theorem RB31E2E.degree_three_neighbour_triangle_complete_or_addable.{u_1} {V : Type u_1} [DecidableEq V] {F : RB31E2E.SimpleEdgeSet V} {v a b c : V} (hSparse : RB31E2E.Sparse22 F) (hva : v ≠ a) (hvb : v ≠ b) (hvc : v ≠ c) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hDegree : RB31E2E.edgeSetDegree F v = 3) (hvaF : RB31E2E.simpleEdge v a hva ∈ F) (hvbF : RB31E2E.simpleEdge v b hvb ∈ F) (hvcF : RB31E2E.simpleEdge v c hvc ∈ F) : RB31E2E.simpleEdge a b hab ∈ F ∧ RB31E2E.simpleEdge a c hac ∈ F ∧ RB31E2E.simpleEdge b c hbc ∈ F ∨ ∃ e ∈ {RB31E2E.simpleEdge a b hab, RB31E2E.simpleEdge a c hac, RB31E2E.simpleEdge b c hbc}, e ∉ F ∧ RB31E2E.Sparse22 (insert e (RB31E2E.deleteVertexEdges F v))
theorem RB31E2E.degree_three_neighbour_triangle_complete_or_addable.{u_1} {V : Type u_1} [DecidableEq V] {F : RB31E2E.SimpleEdgeSet V} {v a b c : V} (hSparse : RB31E2E.Sparse22 F) (hva : v ≠ a) (hvb : v ≠ b) (hvc : v ≠ c) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hDegree : RB31E2E.edgeSetDegree F v = 3) (hvaF : RB31E2E.simpleEdge v a hva ∈ F) (hvbF : RB31E2E.simpleEdge v b hvb ∈ F) (hvcF : RB31E2E.simpleEdge v c hvc ∈ F) : RB31E2E.simpleEdge a b hab ∈ F ∧ RB31E2E.simpleEdge a c hac ∈ F ∧ RB31E2E.simpleEdge b c hbc ∈ F ∨ ∃ e ∈ {RB31E2E.simpleEdge a b hab, RB31E2E.simpleEdge a c hac, RB31E2E.simpleEdge b c hbc}, e ∉ F ∧ RB31E2E.Sparse22 (insert e (RB31E2E.deleteVertexEdges F v))
Complete local dichotomy for three named neighbours in an arbitrary sparse graph: they already span their full triangle, or an actually absent neighbour edge can be inserted after deleting the degree-three vertex.
Suppose no nonedge within N is addable. If xy is the only nonedge, take a
tight set A containing x and y. Either z \in A, and A already
contains N, or z \notin A, and the edges xz and yz make
A \cup \{z\} tight. If N has at least two nonedges, take two that share
an endpoint and a tight set containing the endpoints of each; uncrossing makes
their union a tight set containing N. So in every case some tight set B
contains N. Adding v and the three edges vN to B puts three new
edges on one new vertex, which violates the sparsity bound for Q + vN.
The formalization states the lemma as a dichotomy rather than under a
hypothesis: for a sparse edge set F and a vertex v of degree exactly
three with named neighbours a, b, c, either all three edges between the
neighbours are present in F, or one of the absent ones can be inserted
after deleting v. Taking Q = F - v recovers the paper's formulation. The
induction of the flags chapter applies the
dichotomy directly: an inserted edge is a
certified response edge, and on a complete
neighbour triangle a new flag is created.
The formal proof uses only the tight-set combinatorics above; in particular it
does not depend on the construction theorem of the next section. Like the
paper's proof, it splits on how many of the three neighbour edges are missing:
degree_three_neighbour_triangle_complete_or_addable
combines one lemma for a single missing edge and one for two.