3.4. A construction theorem with no paper counterpart🔗

The formalization keeps an edge set on an ambient vertex type together with an explicit finite set of active vertices, the vertices on which the graph is currently considered. The remaining statements of this chapter are phrased in those terms.

Lemma3.4.1

groupuses 0used by 0✓L∃∀N

Tagslean-only

On an active vertex set with at least two elements, a simple (2,2)-tight graph is either the complete graph on four vertices or admits a strictly smaller legal reduction: one of the four inverse construction moves, or the contraction of a proper tight module in one graph-extension step. Separately, every (2,2)-sparse edge set on a vertex type with at least four elements has a same-vertex (2,2)-tight completion.

Lean code for Lemma3.4.1●3 declarations

defdefined in RB31EndToEnd/Combinatorics/Sparse22/Construction.lean

complete

def RB31E2E.HasNixonOwenReduction.{u_1} {V : Type u_1} [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V) (X : Finset V) : Prop

def RB31E2E.HasNixonOwenReduction.{u_1}
  {V : Type u_1} [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V)
  (X : Finset V) : Prop

The literal four-way reduction conclusion of Nixon--Owen Lemma 3.11.

theoremdefined in RB31EndToEnd/Combinatorics/Sparse22/GraphExtension.lean

complete

theorem RB31E2E.isK4Base_or_hasNixonOwenOrGraphExtensionReduction.{u_1}
  {V : Type u_1} [DecidableEq V] {F : RB31E2E.SimpleEdgeSet V}
  {X : Finset V} (hG : RB31E2E.SimpleTight22On F X)
  (hXcard : 2 ≤ X.card) :
  RB31E2E.IsK4Base F X ∨
    RB31E2E.HasNixonOwenOrGraphExtensionReduction F X

theorem RB31E2E.isK4Base_or_hasNixonOwenOrGraphExtensionReduction.{u_1}
  {V : Type u_1} [DecidableEq V]
  {F : RB31E2E.SimpleEdgeSet V}
  {X : Finset V}
  (hG : RB31E2E.SimpleTight22On F X)
  (hXcard : 2 ≤ X.card) :
  RB31E2E.IsK4Base F X ∨
    RB31E2E.HasNixonOwenOrGraphExtensionReduction
      F X

End-to-end closure of the simple `(2,2)`-tight combinatorial reduction
stage without triangle sequences.  Every graph with at least two active
vertices is either the exact `K₄` base or has a strictly smaller legal
reduction, where the additional graph-extension case is an explicit
supported sparse-and-tight quotient.

theoremdefined in RB31EndToEnd/Combinatorics/Sparse22/TightCompletion.lean

complete

theorem RB31E2E.exists_tight22_completion.{u_1} {V : Type u_1} [DecidableEq V]
  [Fintype V] (F : RB31E2E.SimpleEdgeSet V) (hF : RB31E2E.Sparse22 F)
  (hcard : 4 ≤ Fintype.card V) :
  ∃ G, F ⊆ G ∧ RB31E2E.Sparse22 G ∧ RB31E2E.Tight22 G Finset.univ

theorem RB31E2E.exists_tight22_completion.{u_1}
  {V : Type u_1} [DecidableEq V]
  [Fintype V]
  (F : RB31E2E.SimpleEdgeSet V)
  (hF : RB31E2E.Sparse22 F)
  (hcard : 4 ≤ Fintype.card V) :
  ∃ G,
    F ⊆ G ∧
      RB31E2E.Sparse22 G ∧
        RB31E2E.Tight22 G Finset.univ

Every `(2,2)`-sparse simple edge set on at least four vertices has a
same-vertex `(2,2)`-tight completion.

/-- The literal four-way reduction conclusion of Nixon--Owen Lemma 3.11. -/
def HasNixonOwenReduction (F : SimpleEdgeSet V) (X : Finset V) : Prop :=
  ∃ F' : SimpleEdgeSet V, ∃ X' : Finset V,
    X'.card < X.card ∧
      (LegalInverseHennebergOne F X F' X' ∨
        LegalInverseHennebergTwo F X F' X' ∨
        LegalInverseVertexToK4 F X F' X' ∨
        LegalInverseEdgeToK3 F X F' X')

The four LegalInverse predicates in that disjunction are inverse Henneberg one and two, K_4-to-vertex, and K_3-to-edge, each defined directly on edge sets. Construction.lean calls them the Nixon–Owen reductions; the name is the module's own, and this blueprint has not checked it against a primary source. A legal reduction strictly decreases the number of active vertices, so repeated reductions terminate.

The degree-two case of the theorem is proved outright: deleting a degree-two vertex of a tight graph leaves a smaller tight graph. The degree-three case ends at a vertex contained in a (2,2)-tight K_4, and a triangle-sequence argument would continue from there; GraphExtension.lean replaces that continuation with a shorter one, over a proper tight module of maximum cardinality, since tightness alone forces every outside vertex to send at most one edge into the module unless that vertex has degree two and gives an inverse Henneberg-one move.

None of this appears in Zheng (2026): the paper proves Lemma 2.1 from uncrossing in a seven-line paragraph, proves Lemmas 3.7 and 3.8 in the same style, and its reference list contains no construction theorem.

Nor does the rest of the formalization depend on this section. Of the modules that develop it, only a few counting facts are reachable from the root theorem — facts about the four-element vertex set of a K_4 and about the edges one outside vertex sends into a tight module — while the reduction disjunction HasNixonOwenReduction, the graph-extension quotient, and the tight completion exists_tight22_completion are not reachable at all. Lemmas 2.1, 3.7 and 3.8 therefore rest on the tight-set arguments above, and this section is a parallel development; the module-by-module accounting appears in the correspondence chapter.

Lemma3.4.2

groupuses 1used by 1✓L∃∀N

Tagslean-only

Sparsity transports along an injective map of vertices: if every image of a child edge is an edge of a sparse parent set, the child set is sparse.

Lean code for Lemma3.4.2●2 declarations

defdefined in RB31EndToEnd/Combinatorics/Sparse22/Transport.lean

complete

def RB31E2E.Sparse22Transport.mapEdgeSet.{u_1, u_2} {V : Type u_1}
  {W : Type u_2} (f : V ↪ W) (F : RB31E2E.SimpleEdgeSet V) :
  RB31E2E.SimpleEdgeSet W

def RB31E2E.Sparse22Transport.mapEdgeSet.{u_1,
    u_2}
  {V : Type u_1} {W : Type u_2}
  (f : V ↪ W)
  (F : RB31E2E.SimpleEdgeSet V) :
  RB31E2E.SimpleEdgeSet W

Map a finite simple edge set along an injective vertex map.

theoremdefined in RB31EndToEnd/Combinatorics/Sparse22/Transport.lean

complete

theorem RB31E2E.Sparse22Transport.sparse22_of_mapEdgeSet_subset.{u_1, u_2}
  {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W]
  (f : V ↪ W) {F : RB31E2E.SimpleEdgeSet V}
  {H : RB31E2E.SimpleEdgeSet W} (hH : RB31E2E.Sparse22 H)
  (hFH : RB31E2E.Sparse22Transport.mapEdgeSet f F ⊆ H) :
  RB31E2E.Sparse22 F

theorem RB31E2E.Sparse22Transport.sparse22_of_mapEdgeSet_subset.{u_1,
    u_2}
  {V : Type u_1} {W : Type u_2}
  [DecidableEq V] [DecidableEq W]
  (f : V ↪ W)
  {F : RB31E2E.SimpleEdgeSet V}
  {H : RB31E2E.SimpleEdgeSet W}
  (hH : RB31E2E.Sparse22 H)
  (hFH :
    RB31E2E.Sparse22Transport.mapEdgeSet f
        F ⊆
      H) :
  RB31E2E.Sparse22 F

If the transported child edges lie in a sparse parent edge set, then
the child itself is sparse.

/-- Map a finite simple edge set along an injective vertex map. -/
def mapEdgeSet (f : V ↪ W) (F : SimpleEdgeSet V) : SimpleEdgeSet W :=
  F.map (mapSimpleEdgeEmbedding f)

In the formalization, deleting a vertex leaves an edge set on a smaller vertex type — the subtype of the remaining vertices — rather than on a subset of one fixed vertex set, and creating a flag changes the type again, by adjoining an auxiliary vertex. A sparse edge set therefore has to be moved along an embedding at every step of the induction, and this lemma justifies each such move. No corresponding statement appears in the paper, whose graphs share one ambient vertex set throughout.

The definition is one line, because an embedding of vertices induces an embedding of unordered pairs, and Finset.map along an embedding is injective. The image then has the cardinality of the source, so both sides of the counting condition transport.