5. Collinearity flags
Section 3 of Zheng (2026) proves the estimate at the centre
of the paper: for a (2,2)-sparse graph F and an injective configuration
a : V \to K^3 whose coordinates generate the finitely generated extension
K/k,
\dim_K \ker D_F(a)^T + \trdeg_k K \le 3|V|.
The inequality is proved by deleting one low-degree vertex at a time, and by
the deletion ledger the change in the defect at
each step is the local increment u + \delta_v less three, so the defect
does not increase exactly when u + \delta_v \le 3. In the exceptional
case of
the local classification that bound
fails — the deleted vertex has exactly three neighbours, their configuration
points are collinear, and u + \delta_v = 4 — but
the three rigidity rows on pairs of
neighbours already lie in the row space of the deleted graph. When one of
the three neighbour edges is absent and can be added, adding it restores the
lost stress dimension and the induction continues. When all three are
present, no edge can be added, and the paper instead strengthens the
statement being proved: the triple is retained as a collinearity flag,
together with a chosen missing edge on it and an auxiliary vertex, and the
inequality becomes
\dim_K \ker D_G(a)^T + \trdeg_k K + 2|\Gamma| \le 3|V|
for a graph carrying a family \Gamma of such flags, with a term of two
for each flag, the codimension of the collinearity condition on its triple.
That statement is Theorem 3.9, this chapter's main result; the flag-free
case \Gamma = \emptyset is Theorem 1.2, the inequality above.
We first state the flag vocabulary and the sparsity condition on the simultaneous completion, then the counting facts about how flags may overlap. A selection lemma then gives a low-degree vertex that is in no flag or in exactly one; for the second type there are a pivot and a local classification; two augmentation lemmas give the edge that is added back in each exceptional case; and the proof of Theorem 3.9 combines them into the induction. A closing section describes the transitions between flag states that the formalization builds and the paper performs inside one proof.
The formalization renames every object of this section, so the two vocabularies are set side by side once, here, before either is used:
The paper | The formalization |
|---|---|
collinearity flag | provenance flag |
support triple |
terminals ( |
distinguished missing edge |
missing terminal edge ( |
auxiliary vertex | ghost vertex, an inhabitant of the flag type itself |
base-graph vertices and edges | live vertices and live edges |
simultaneous completion |
|
support multiplicity | |
the sets | |
self-stress dimension | |
the inequality |
the semismallness budget ( |
local payment | |
certified response edge | virtual response edge |