Body-Pin Rigidity

3.1. Sparsity and tight sets🔗

Definition3.1.1
Group: The paper's sparsity vocabulary: the counting condition, tight sets, and the two facts about them that the vertex-deletion induction uses. (3)
Group member previews
Preview
Lemma 3.2.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 0
Used by 10
Reverse dependency previews
Preview
Lemma 3.2.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagspaper

A simple graph F = (V, E_F) is (2,2)-sparse when every nonempty U \subseteq V satisfies |E_F(U)| \le 2|U| - 2, where E_F(U) is the edge set of the induced subgraph F[U]. A nonempty U attaining equality is tight. (Zheng, 2026, Equation 1.3)

Lean code for Definition3.1.1●2 definitions
  • defdefined in RB31EndToEnd/Combinatorics/Sparse22/Basic.lean
    complete
    def RB31E2E.Sparse22.{u_1} {V : Type u_1} [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V) : Prop
    def RB31E2E.Sparse22.{u_1} {V : Type u_1}
  [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V) : Prop
    Every nonempty induced vertex set obeys the `(2,2)` count.
  • defdefined in RB31EndToEnd/Combinatorics/Sparse22/Basic.lean
    complete
    def RB31E2E.Tight22.{u_1} {V : Type u_1} [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V) (X : Finset V) : Prop
    def RB31E2E.Tight22.{u_1} {V : Type u_1}
  [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V)
  (X : Finset V) : Prop
    A nonempty vertex set on which the `(2,2)` inequality is tight.

The bound is stated for nonempty U because 2|U| - 2 is negative at U = \emptyset. A one-vertex set is tight, since both sides are zero, and K_4 is tight on its whole vertex set. Sparsity passes to any subset of the edge set, which is Sparse22.mono; deleting a vertex from a sparse graph therefore leaves a sparse graph, as the deletion step requires.

The formalization states the condition for a finite set of unordered pairs rather than for a SimpleGraph: a SimpleEdge is a Sym2 of two distinct vertices, and a SimpleEdgeSet is a Finset of those, so parallel pins and loops are absent by construction and multiplicity belongs to the body–pin layer, where the paper also keeps it. The accessor vertices is quoted with them because edgesInside is written with it.

/-- An unordered edge with two distinct endpoints. -/ abbrev SimpleEdge (V : Type*) := {e : Sym2 V // ¬e.IsDiag}/-- An occurrence-free finite simple edge set. -/ abbrev SimpleEdgeSet (V : Type*) := Finset (SimpleEdge V)/-- The two endpoints of a simple edge. -/ def vertices (e : SimpleEdge V) : Finset V := e.1.toFinset/-- Edges of `F` whose two endpoints lie in `X`. -/ def edgesInside (F : SimpleEdgeSet V) (X : Finset V) : SimpleEdgeSet V := F.filter fun e => e.vertices ⊆ X/-- Every nonempty induced vertex set obeys the `(2,2)` count. -/ def Sparse22 (F : SimpleEdgeSet V) : Prop := ∀ X : Finset V, X.Nonempty → (edgesInside F X).card ≤ 2 * (X.card - 1)/-- A nonempty vertex set on which the `(2,2)` inequality is tight. -/ def Tight22 (F : SimpleEdgeSet V) (X : Finset V) : Prop := X.Nonempty ∧ (edgesInside F X).card = 2 * (X.card - 1)

The right-hand side is written 2 * (X.card - 1) over \N, where truncated subtraction gives 0 at a one-vertex set. That is the same value as 2|U| - 2 over \Z for every nonempty U, and the nonemptiness hypothesis is kept anyway, so the two readings agree wherever either is stated.