Body-Pin Rigidity

3.2. Two consequences of supermodularity🔗

Both lemmas of this section follow from the supermodularity of the edge-count function: for any two vertex sets A and B,

|E_F(A)| + |E_F(B)| \le |E_F(A \cup B)| + |E_F(A \cap B)|,

since an edge inside A or inside B is inside A \cup B, and an edge inside both is inside A \cap B.

Lemma3.2.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
Definition 3.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 3.3.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagspaper

The union and the intersection of two tight sets with nonempty intersection are again tight. (Zheng, 2026, Section 2.1)

Lean code for Lemma3.2.1●2 theorems
  • theoremdefined in RB31EndToEnd/Combinatorics/Sparse22/Uncrossing.lean
    complete
    theorem RB31E2E.card_edgesInside_supermodular.{u_1} {V : Type u_1}
  [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (A B : Finset V) :
  Finset.card (RB31E2E.edgesInside F A) +
      Finset.card (RB31E2E.edgesInside F B) ≤
    Finset.card (RB31E2E.edgesInside F (A ∪ B)) +
      Finset.card (RB31E2E.edgesInside F (A ∩ B))
    theorem RB31E2E.card_edgesInside_supermodular.{u_1}
  {V : Type u_1} [DecidableEq V]
  (F : RB31E2E.SimpleEdgeSet V)
  (A B : Finset V) :
  Finset.card (RB31E2E.edgesInside F A) +
      Finset.card
        (RB31E2E.edgesInside F B) ≤
    Finset.card
        (RB31E2E.edgesInside F (A ∪ B)) +
      Finset.card
        (RB31E2E.edgesInside F (A ∩ B))
    Induced-edge count is supermodular on vertex sets.
  • theoremdefined in RB31EndToEnd/Combinatorics/Sparse22/Uncrossing.lean
    complete
    theorem RB31E2E.tight22_union_inter.{u_1} {V : Type u_1} [DecidableEq V]
  {F : RB31E2E.SimpleEdgeSet V} {A B : Finset V}
  (hF : RB31E2E.Sparse22 F) (hA : RB31E2E.Tight22 F A)
  (hB : RB31E2E.Tight22 F B) (hAB : (A ∩ B).Nonempty) :
  RB31E2E.Tight22 F (A ∪ B) ∧ RB31E2E.Tight22 F (A ∩ B)
    theorem RB31E2E.tight22_union_inter.{u_1}
  {V : Type u_1} [DecidableEq V]
  {F : RB31E2E.SimpleEdgeSet V}
  {A B : Finset V}
  (hF : RB31E2E.Sparse22 F)
  (hA : RB31E2E.Tight22 F A)
  (hB : RB31E2E.Tight22 F B)
  (hAB : (A ∩ B).Nonempty) :
  RB31E2E.Tight22 F (A ∪ B) ∧
    RB31E2E.Tight22 F (A ∩ B)
    Two tight sets with nonempty intersection uncross: both their union and
their intersection are tight.  A one-vertex intersection is allowed.

Suppose A and B are tight and intersect. Adding the two sparsity bounds on A \cup B and A \cap B to the two tightness equalities on A and B forces both bounds to be equalities, which is the lemma. card_edgesInside_supermodular is the supermodularity inequality and tight22_union_inter is the conclusion.

The intersection has to be nonempty because tightness is defined only for nonempty sets, and a one-vertex intersection is enough. For disjoint A and B neither conclusion holds.

Lemma3.2.2
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
Definition 3.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1used by 1✓L∃∀N
Tagspaperdeviation

If adding a nonedge xy to a (2,2)-sparse graph violates sparsity, then some tight set contains both x and y. (Zheng, 2026, Section 2.1)

Lean code for Lemma3.2.2●1 theorem
  • theoremdefined in RB31EndToEnd/Combinatorics/Sparse22/Basic.lean
    complete
    theorem RB31E2E.exists_tight22_of_not_sparse22_insert.{u_1} {V : Type u_1}
  [DecidableEq V] {F : RB31E2E.SimpleEdgeSet V}
  {e : RB31E2E.SimpleEdge V} (hF : RB31E2E.Sparse22 F) (heF : e ∉ F)
  (hbad : ¬RB31E2E.Sparse22 (insert e F)) :
  ∃ X, X.Nonempty ∧ e.vertices ⊆ X ∧ RB31E2E.Tight22 F X
    theorem RB31E2E.exists_tight22_of_not_sparse22_insert.{u_1}
  {V : Type u_1} [DecidableEq V]
  {F : RB31E2E.SimpleEdgeSet V}
  {e : RB31E2E.SimpleEdge V}
  (hF : RB31E2E.Sparse22 F) (heF : e ∉ F)
  (hbad :
    ¬RB31E2E.Sparse22 (insert e F)) :
  ∃ X,
    X.Nonempty ∧
      e.vertices ⊆ X ∧ RB31E2E.Tight22 F X
    If adjoining a new simple edge destroys `(2,2)`-sparsity, some nonempty
vertex set contains both endpoints and was already tight before the edge
was adjoined.

The paper obtains this lemma from the same supermodularity argument. The formal proof is more direct. Let X be a vertex set witnessing the violation. Then X contains both x and y, since otherwise adding the edge changes no induced edge count; hence |E_F(X)| + 1 > 2|X| - 2, while sparsity of F gives |E_F(X)| \le 2|X| - 2, and X is tight. Supermodularity is never invoked, so exists_tight22_of_not_sparse22_insert is proved in the same module as the definitions, independently of uncrossing.