Body-Pin Rigidity

5.1. Flags and their completions🔗

Definition5.1.1
Group: The paper's flag vocabulary and the results of Section 3: definitions, overlap counting, selection, pivot, classification, augmentation, and the stress–codimension theorem. (10)
Group member previews
Preview
Definition 5.1.2
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 0used by 1✓L∃∀N
Tagspaperdeviation

A collinearity flag on a finite simple graph G = (V, E) is a chain d_\gamma \subsetneq T_\gamma \subsetneq Q_\gamma together with an auxiliary vertex g_\gamma \notin V: a three-element support triple T_\gamma \subseteq V inducing the two-edge path E(G[T_\gamma]) = \binom{T_\gamma}{2} \setminus \{d_\gamma\}, the distinguished missing edge d_\gamma, and Q_\gamma = T_\gamma \sqcup \{g_\gamma\}. A configuration a : V \to K^3 realizes the flag if the points \{a_x : x \in T_\gamma\} are collinear; the K_4-completion restores d_\gamma and joins g_\gamma to the three support vertices. (Zheng, 2026, Definition 3.1)

Lean code for Definition5.1.1●3 definitions
  • abbrevdefined in RB31EndToEnd/Combinatorics/ProvenanceFlag.lean
    complete
    abbrev RB31E2E.ProvenanceFlag.State.terminals.{u_3, u_4} {V : Type u_3}
  {Flag : Type u_4} [Fintype V] [DecidableEq V] [Fintype Flag]
  [DecidableEq Flag] (self : RB31E2E.ProvenanceFlag.State V Flag) :
  Flag → Finset V
    abbrev RB31E2E.ProvenanceFlag.State.terminals.{u_3,
    u_4}
  {V : Type u_3} {Flag : Type u_4}
  [Fintype V] [DecidableEq V]
  [Fintype Flag] [DecidableEq Flag]
  (self :
    RB31E2E.ProvenanceFlag.State V Flag) :
  Flag → Finset V
  • abbrevdefined in RB31EndToEnd/Combinatorics/ProvenanceFlag.lean
    complete
    abbrev RB31E2E.ProvenanceFlag.State.missing.{u_3, u_4} {V : Type u_3}
  {Flag : Type u_4} [Fintype V] [DecidableEq V] [Fintype Flag]
  [DecidableEq Flag] (self : RB31E2E.ProvenanceFlag.State V Flag) :
  Flag → RB31E2E.SimpleEdge V
    abbrev RB31E2E.ProvenanceFlag.State.missing.{u_3,
    u_4}
  {V : Type u_3} {Flag : Type u_4}
  [Fintype V] [DecidableEq V]
  [Fintype Flag] [DecidableEq Flag]
  (self :
    RB31E2E.ProvenanceFlag.State V Flag) :
  Flag → RB31E2E.SimpleEdge V
  • defdefined in RB31EndToEnd/Combinatorics/ProvenanceFlag.lean
    complete
    def RB31E2E.ProvenanceFlag.ghostEdge.{u_1, u_2} {V : Type u_1}
  {Flag : Type u_2} (t : Flag) (v : V) : RB31E2E.SimpleEdge (V ⊕ Flag)
    def RB31E2E.ProvenanceFlag.ghostEdge.{u_1,
    u_2}
  {V : Type u_1} {Flag : Type u_2}
  (t : Flag) (v : V) :
  RB31E2E.SimpleEdge (V ⊕ Flag)
    The private ghost-to-terminal edge belonging to one active flag.

The formalization calls a collinearity flag a provenance flag and has no object representing one flag on its own. A flag is an inhabitant t of a finite index type, and its data are the values at t of the fields terminals and missing of the system-level structure of the next node, whose remaining fields are conditions (3.1) and (3.2): each terminal set has three elements, the missing edge lies inside it, is absent from the live graph, and every other terminal pair is present. The auxiliary vertex needs no name of its own, since the completion is built on the sum type V \oplus \Gamma and the ghost vertex of the flag t is the right summand t itself. The realization condition is not part of the combinatorial object; it reappears as the collinearity field of the function-field branches defined before Theorem 3.9 below.

Figure 2 of Zheng (2026) distinguishes the four kinds of edge; in the redrawing below, the support triple induces the two-edge path x - y - z with the dashed arc as the distinguished missing edge d_\gamma = xz, and the completion restores xz and adds the three auxiliary edges from g_\gamma to the support vertices. The auxiliary vertex has no configuration coordinate.

Definition5.1.2
Group: The paper's flag vocabulary and the results of Section 3: definitions, overlap counting, selection, pivot, classification, augmentation, and the stress–codimension theorem. (10)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
Statement uses 2
Statement dependency previews
Preview
Definition 3.1.1
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 6
Reverse dependency previews
Preview
Lemma 5.2.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N
Tagspaperdeviation

A system of collinearity flags on a common base graph G = (V, E) is a family (d_\gamma \subsetneq T_\gamma \subsetneq Q_\gamma)_{\gamma \in \Gamma} with pairwise distinct auxiliary vertices outside V. Its simultaneous flag completion \widehat{G} is the graph on V \sqcup \{g_\gamma : \gamma \in \Gamma\} obtained by restoring every d_\gamma and attaching every auxiliary star \{g_\gamma x : x \in T_\gamma\}. The system is a sparse collinearity-flag system if \widehat{G} is (2,2)-sparse. (Zheng, 2026, Definition 3.2)

Lean code for Definition5.1.2●3 definitions
  • structure(7 fields)defined in RB31EndToEnd/Combinatorics/ProvenanceFlag.lean
    complete
    structure RB31E2E.ProvenanceFlag.State.{u_3, u_4} (V : Type u_3) (Flag : Type u_4)
  [Fintype V] [DecidableEq V] [Fintype Flag] [DecidableEq Flag] :
  Type (max u_3 u_4)
    structure RB31E2E.ProvenanceFlag.State.{u_3, u_4}
  (V : Type u_3) (Flag : Type u_4)
  [Fintype V] [DecidableEq V]
  [Fintype Flag] [DecidableEq Flag] :
  Type (max u_3 u_4)
    Finite provenance-flag data on a live simple graph.

`V` contains exactly the live vertices and `Flag` contains exactly the
active flags.  Consequently every edge and terminal label is active by its
type.  Each terminal set has three elements; `missing t` is one of its three
pairs and is absent from the live graph; every other terminal pair is live.

    Fields

    edges : RB31E2E.SimpleEdgeSet V
    terminals : Flag → Finset V
    missing : Flag → RB31E2E.SimpleEdge V
    terminals_card : ∀ (t : Flag), (self.terminals t).card = 3
    missing_supported : ∀ (t : Flag), (self.missing t).vertices ⊆ self.terminals t
    missing_not_live : ∀ (t : Flag), self.missing t ∉ self.edges
    other_terminal_edges_live : ∀ (t : Flag) (e : RB31E2E.SimpleEdge V), e.vertices ⊆ self.terminals t → e ≠ self.missing t → e ∈ self.edges
  • defdefined in RB31EndToEnd/Combinatorics/ProvenanceFlag.lean
    complete
    def RB31E2E.ProvenanceFlag.State.completionEdges.{u_1, u_2} {V : Type u_1}
  {Flag : Type u_2} [Fintype V] [DecidableEq V] [Fintype Flag]
  [DecidableEq Flag] (S : RB31E2E.ProvenanceFlag.State V Flag) :
  RB31E2E.SimpleEdgeSet (V ⊕ Flag)
    def RB31E2E.ProvenanceFlag.State.completionEdges.{u_1,
    u_2}
  {V : Type u_1} {Flag : Type u_2}
  [Fintype V] [DecidableEq V]
  [Fintype Flag] [DecidableEq Flag]
  (S :
    RB31E2E.ProvenanceFlag.State V Flag) :
  RB31E2E.SimpleEdgeSet (V ⊕ Flag)
    The literal completed edge set: restore one terminal edge and attach
one private three-star for every active flag.
  • defdefined in RB31EndToEnd/Combinatorics/ProvenanceFlag.lean
    complete
    def RB31E2E.ProvenanceFlag.State.CompletionSparse.{u_1, u_2} {V : Type u_1}
  {Flag : Type u_2} [Fintype V] [DecidableEq V] [Fintype Flag]
  [DecidableEq Flag] (S : RB31E2E.ProvenanceFlag.State V Flag) : Prop
    def RB31E2E.ProvenanceFlag.State.CompletionSparse.{u_1,
    u_2}
  {V : Type u_1} {Flag : Type u_2}
  [Fintype V] [DecidableEq V]
  [Fintype Flag] [DecidableEq Flag]
  (S :
    RB31E2E.ProvenanceFlag.State V Flag) :
  Prop
    Sparsity of the actual completed edge set.

The formalization's State is this definition on exact types: the vertex type V contains exactly the base graph's vertices, called the live vertices, and the flag type contains exactly the active flags, so no ambient labels, inactive flags, or support predicates occur. Deleting a vertex or a flag therefore changes the types themselves, which is why the transport lemma of the sparsity chapter is used at every step of the induction. The completion is a literal edge set on V \oplus \Gamma, assembled from three packets: the live edges transported along the left injection, one restored missing edge per flag, and one ghost star per flag.

/-- A live simple edge transported along the left injection into `V ⊕ Flag`. -/ def liftLiveEdge (e : SimpleEdge V) : SimpleEdge (V ⊕ Flag) := ⟨e.1.map Sum.inl, V:Type u_1Flag:Type u_2inst✝³:Fintype Vinst✝²:DecidableEq Vinst✝¹:Fintype Flaginst✝:DecidableEq Flage:SimpleEdge V⊢ ¬(Sym2.map Sum.inl ↑e).IsDiag V:Type u_1Flag:Type u_2inst✝³:Fintype Vinst✝²:DecidableEq Vinst✝¹:Fintype Flaginst✝:DecidableEq Flage:SimpleEdge V⊢ ¬(↑e).IsDiag All goals completed! 🐙⟩/-- The private ghost-to-terminal edge belonging to one active flag. -/ def ghostEdge (t : Flag) (v : V) : SimpleEdge (V ⊕ Flag) := simpleEdge (Sum.inr t) (Sum.inl v) (V:Type u_1Flag:Type u_2inst✝³:Fintype Vinst✝²:DecidableEq Vinst✝¹:Fintype Flaginst✝:DecidableEq Flagt:Flagv:V⊢ Sum.inr t ≠ Sum.inl v All goals completed! 🐙)/-- Live edges, transported to the completed vertex type. -/ def State.liftedLiveEdges (S : State V Flag) : SimpleEdgeSet (V ⊕ Flag) := S.edges.map (liftLiveEdgeEmbedding (V := V) (Flag := Flag))/-- The restored distinguished terminal edge of every active flag. -/ def State.restoredMissingEdges (S : State V Flag) : SimpleEdgeSet (V ⊕ Flag) := Finset.univ.image fun t ↦ liftLiveEdge (Flag := Flag) (S.missing t)/-- All private ghost stars, one for every inhabitant of `Flag`. -/ def State.ghostStarEdges (S : State V Flag) : SimpleEdgeSet (V ⊕ Flag) := Finset.univ.biUnion fun t ↦ (S.terminals t).image fun v ↦ ghostEdge t v/-- The literal completed edge set: restore one terminal edge and attach one private three-star for every active flag. -/ def State.completionEdges (S : State V Flag) : SimpleEdgeSet (V ⊕ Flag) := S.liftedLiveEdges ∪ S.restoredMissingEdges ∪ S.ghostStarEdges/-- Sparsity of the actual completed edge set. -/ def State.CompletionSparse (S : State V Flag) : Prop := Sparse22 S.completionEdges

The paper's (3.3) takes a union of edge sets on a disjoint union of vertex sets and lets repeated edges identify themselves; the formalization takes the same union of three Finsets, and CompletionSparse is the sparsity predicate applied to the result. No consequence of sparsity is stored in the structure: the counting facts of the next section are derived from these fields whenever the induction needs them. The variety X^\circ_{\mathcal{T}} has no Lean counterpart; its function-field substitute is defined before Theorem 3.9.