9.2. Glossary🔗

The paper and the Lean development do not share names, and several of the paper's own terms are coinages that occur nowhere in its four background references. Each term below is glossed at first use in the chapter that introduces it; this table collects them. The Lean names behind each term are on the linked node, whose panel carries their signatures and source links.

Term	Introduced at	Meaning
equivalent, congruent, locally rigid	the statement chapter	equal lengths on the edges, equal distances on every pair, and congruence of every equivalent placement near enough; the Euclidean vocabulary the geometric roots are stated in, with no counterpart in the paper
regular placement, generic placement	the statement chapter	a placement at which the rigidity operator attains the graph's maximum rank, and one that is regular for every simple graph on the vertex set at once; the second is the formalization's generic, and it asserts nothing about algebraic independence of the coordinates
continuous motion, continuously rigid	the statement chapter	a continuous path of placements along which every edge keeps its length, with no differentiability assumed, and a placement from which every such path stays congruent to it
provenance flag	the flags chapter	the formalization's name for the paper's collinearity flag: a support triple with a distinguished missing edge and an auxiliary vertex
terminals	the flags chapter	the support triple `T_\gamma` of a flag
missing terminal edge	the flags chapter	the distinguished missing edge `d_\gamma`
ghost vertex	the flags chapter	the auxiliary vertex `g_\gamma`; in the formalization it is the flag index itself, the right summand of `V \oplus \Gamma`
live vertices, live edges	the flags chapter	the vertices and edges of the base graph, as opposed to the ghost vertices and the completion edges
completion	the flags chapter	the simultaneous completion `\widehat{G}`: every missing terminal edge restored and every auxiliary star attached
outside, private, shared vertices	the flags chapter	the partition of the live vertices by support multiplicity: outside (`h_x = 0`), private (`h_x = 1`), shared (`h_x \ge 2`); the paper's sets `O`, `P`, `S`
payment, payment failure	the deletion chapter	the local bound `u + \delta_v \le 3`, or `\le 1` at a private support vertex, under which one deletion step does not increase the defect; the exceptional collinear case is its failure
semismallness budget	the flags chapter	the subtraction-free form `s + \trdeg_k K + 2\|\Gamma\| \le 3\|V\|` of the paper's defect inequality `\Delta \le 0`
virtual response edge	the deletion chapter	an absent edge whose direction row already lies in the row space; the paper's certified response edge, without the sparsity clause
direction rows, direction stress	the deletion chapter	the field-extension form (1.4) of the rigidity matrix, and its self-stress space over the coefficient field
grounded	the strata chapter	a root vertex fixed at the origin, removing the translations and nothing else; the paper's coinage, and not the pinned framework of Király and Tanigawa (2019), which fixes points completely
twist	the necessity chapter	an element of `k^3 \oplus k^3`, angular and linear part, describing the infinitesimal motion of one rigid body; (5.1) puts the Split–Klein form on it
null cellule	the Split–Klein chapter	the module family's name for the pair of conditions on a twist assignment: pairwise distinct, and null on every selected edge; not checked against a primary source
Nixon–Owen reduction	the sparsity chapter	the construction moves for `(2,2)`-tight graphs; the module's own name, cited nowhere in the paper and not checked against a primary source

Two conventions of the development are worth stating once. Every declaration lives under the namespace root RB31E2E, and every module under the library root RB31EndToEnd/; the reverse index below is organized by that module tree. And the paper's flags, graphs and fields appear in Lean with exact types rather than as subsets of a fixed universe: deletion and flag registration change the vertex type, and sparsity is transported along the inclusion at every step.