5.2. The incidence forest
Two flags may share support vertices, and the counting of this section
bounds how much. Following the paper, let
V_{\mathcal{T}} = \bigcup_{\gamma \in \Gamma} T_\gamma and let
B_{\mathcal{T}} be the bipartite incidence graph with vertex classes
\Gamma and V_{\mathcal{T}}, in which \gamma is adjacent to x if
and only if x \in T_\gamma.
In a sparse collinearity-flag system, every nonempty subfamily of j \ge 1
flags uses q \ge 2j + 1 support vertices in total; consequently
B_{\mathcal{T}} is a forest. Moreover X^\circ_{\mathcal{T}} is
irreducible of codimension 2|\Gamma| in (\mathbb{A}^3_k)^V.
(Zheng, 2026, Proposition 3.3)
Lean code for Lemma5.2.1●3 theorems
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagForest.leancomplete
theorem RB31E2E.ProvenanceFlag.State.card_terminal_inter_le_one.{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) {t u : Flag} (htu : t ≠ u) : (S.terminals t ∩ S.terminals u).card ≤ 1
theorem RB31E2E.ProvenanceFlag.State.card_terminal_inter_le_one.{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) {t u : Flag} (htu : t ≠ u) : (S.terminals t ∩ S.terminals u).card ≤ 1
Completion sparsity forbids two distinct flags from sharing two live terminals.
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagForest.leancomplete
theorem RB31E2E.ProvenanceFlag.State.two_mul_card_add_one_le_card_terminalUnion.{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) {A : Finset Flag} (hA : A.Nonempty) : 2 * A.card + 1 ≤ (S.terminalUnion A).card
theorem RB31E2E.ProvenanceFlag.State.two_mul_card_add_one_le_card_terminalUnion.{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) {A : Finset Flag} (hA : A.Nonempty) : 2 * A.card + 1 ≤ (S.terminalUnion A).card
Every nonempty family of `j` active flags uses at least `2*j+1` distinct live terminals.
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagForest.leancomplete
theorem RB31E2E.ProvenanceFlag.State.terminalHyperforest.{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) : S.TerminalHyperforest
theorem RB31E2E.ProvenanceFlag.State.terminalHyperforest.{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) : S.TerminalHyperforest
For each \gamma, the set T_\gamma \cup \{g_\gamma\} induces a tight
copy of K_4 in \widehat{G}. Two distinct flags share at most one
support vertex: equal triples would put nine edges on five vertices, and two
shared vertices would put eleven on six, both violating sparsity. Any j
flags therefore contribute 6j pairwise disjoint edges on q + j
vertices, so 6j \le 2(q + j) - 2, which is q \ge 2j + 1. A cycle of
j flag vertices in B_{\mathcal{T}} would use at most 2j support
vertices, contradicting that bound, so B_{\mathcal{T}} is a forest.
For the geometric half, the paper puts coordinates on one support triple:
collinearity of three points is the condition
\operatorname{rank}[\,u\ v\,] \le 1 on the two difference vectors, an
irreducible determinantal variety of codimension two. Adding flags one at a
time along an incidence tree meets the existing supports in at most one
vertex, so each flag multiplies by the same variety and the codimension grows
by two; products over components, free factors for untouched vertices, and
removing the collision diagonals give (3.5).
The counting half is formalized and the geometric half is not. Distinct
triples sharing at most one live vertex is
card_terminal_inter_le_one,
and (3.4) is
two_mul_card_add_one_le_card_terminalUnion;
both are derived from the actual finite edge unions, with the six-edge count
and the pairwise disjointness proved as Finset identities.
The bipartite graph B_{\mathcal{T}} is never constructed: the proof of
the selection lemma below uses only the quantified inequality itself, stated
as TerminalHyperforest
and proved from completion sparsity.
/-- Live terminals used by a finite family of flags. -/
def State.terminalUnion (S : State V Flag) (A : Finset Flag) : Finset V :=
A.biUnion S.terminals/-- Derived hyperforest property of the terminal triples. This definition
is only an abbreviation for the quantified Finset inequality; it is never a
field of `State` and the theorem below constructs it from completion
sparsity. -/
def State.TerminalHyperforest (S : State V Flag) : Prop :=
∀ A : Finset Flag, A.Nonempty → 2 * A.card + 1 ≤ (S.terminalUnion A).card
The variety X^\circ_{\mathcal{T}}, its irreducibility, and the
codimension (3.5) have no Lean counterpart, in the same way that
the scheme-theoretic statements of the strata
chapter have none. The number 2|\Gamma| still appears, as the flag term
of the semismallness budget defined before Theorem 3.9: the formal induction
proves the inequality (3.14) directly, and the paper's reading of
2|\Gamma| as a codimension is not needed for it.