5.3. A global low-degree choice
For x \in V, the support multiplicity
h_x = |\{\gamma \in \Gamma : x \in T_\gamma\}| counts the flags whose
support triple contains x, and it partitions the live vertices into
O = \{h_x = 0\}, P = \{h_x = 1\} and S = \{h_x \ge 2\}, so
|O| + |P| + |S| = |V|.
(Zheng, 2026, Section 3.2)
Lean code for Definition5.3.1●2 declarations
Associated Lean declarations
-
defdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagSelection.leancomplete
def RB31E2E.ProvenanceFlag.State.flagMultiplicity.{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) (v : V) : ℕ
def RB31E2E.ProvenanceFlag.State.flagMultiplicity.{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) (v : V) : ℕ
Number of active flags containing a live vertex.
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagSelection.leancomplete
theorem RB31E2E.ProvenanceFlag.State.card_live_partition.{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) : Fintype.card V = S.outsideVertices.card + S.privateVertices.card + S.sharedVertices.card
theorem RB31E2E.ProvenanceFlag.State.card_live_partition.{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) : Fintype.card V = S.outsideVertices.card + S.privateVertices.card + S.sharedVertices.card
Exact cardinal partition of the live vertex type.
A vertex in P is called a private support vertex; the vertices in O
are outside every flag, and those in S are shared. The formalization
defines the multiplicity and the three sets as Finsets of the
live vertex type, and the cardinality identity of the node is
card_live_partition.
/-- Active flags containing a live vertex. -/
def State.activeFlagsAt (S : State V Flag) (v : V) : Finset Flag :=
Finset.univ.filter fun t ↦ v ∈ S.terminals t/-- Number of active flags containing a live vertex. -/
def State.flagMultiplicity (S : State V Flag) (v : V) : ℕ :=
(S.activeFlagsAt v).card/-- Live vertices outside every active flag. -/
def State.outsideVertices (S : State V Flag) : Finset V :=
Finset.univ.filter fun v ↦ S.flagMultiplicity v = 0/-- Live vertices belonging to exactly one active flag. -/
def State.privateVertices (S : State V Flag) : Finset V :=
Finset.univ.filter fun v ↦ S.flagMultiplicity v = 1/-- Live vertices belonging to at least two active flags. -/
def (S : State V Flag) : Finset V :=
Finset.univ.filter fun v ↦ 2 ≤ S.flagMultiplicity v
If V \ne \emptyset, then some vertex x \in O has \deg_G(x) \le 3, or
some vertex x \in P has \deg_G(x) \le 2.
(Zheng, 2026, Lemma 3.4)
Lean code for Lemma5.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagSelection.leancomplete
theorem RB31E2E.ProvenanceFlag.State.exists_outside_degree_le_three_or_private_degree_le_two.{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) (hSparse : S.CompletionSparse) (hV : Finset.univ.Nonempty) : (∃ v, S.flagMultiplicity v = 0 ∧ RB31E2E.edgeSetDegree S.edges v ≤ 3) ∨ ∃ v, S.flagMultiplicity v = 1 ∧ RB31E2E.edgeSetDegree S.edges v ≤ 2
theorem RB31E2E.ProvenanceFlag.State.exists_outside_degree_le_three_or_private_degree_le_two.{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) (hSparse : S.CompletionSparse) (hV : Finset.univ.Nonempty) : (∃ v, S.flagMultiplicity v = 0 ∧ RB31E2E.edgeSetDegree S.edges v ≤ 3) ∨ ∃ v, S.flagMultiplicity v = 1 ∧ RB31E2E.edgeSetDegree S.edges v ≤ 2
Sparse completion forces a reducible live vertex: either a vertex outside every flag has degree at most three, or a vertex private to one flag has degree at most two.
Set n = |V|, m = |E| and k = |\Gamma|. Distinct flags share at most
one support vertex, so their missing edges are distinct, absent from the base
graph, and disjoint from every auxiliary star; the completion therefore has
exactly m + 4k edges on n + k vertices, and sparsity gives
m \le 2n - 2k - 2. Each incidence x \in T_\gamma gives an edge of the
induced path G[T_\gamma] at x, and edges selected from distinct flags
differ, so \deg_G(x) \ge h_x.
Suppose neither type of vertex exists. Then every vertex of O has degree
at least four and every vertex of P at least three, so the degree sum
gives 2m \ge 4|O| + 2|P| + 3k, using \sum_{x \in S} h_x = 3k - |P|.
Combining this with the edge bound gives 7k + 4 \le 2|P| + 4|S|, while
h_x \ge 2 on S gives
2|P| + 4|S| \le 2(|P| + \sum_{x \in S} h_x) = 6k, a contradiction.
The formal proof runs the same three ledgers, each proved as an identity of
the literal state: the completion has |E| + 4|\Gamma| edges
(card_completionEdges),
the terminal incidences sum to 3|\Gamma|, the live degrees sum to
2|E|, and each incidence at a vertex gives a distinct live edge
(flagMultiplicity_le_liveDegree).
The closing arithmetic is kept in a separate module of natural-number
inequalities, so no truncated subtraction hides inside graph notation. The
selection conclusion is a theorem about every sparse state, not a field of
the structure.