4.3. Certified response edges
A nonedge xy of H whose rigidity row already lies in
\operatorname{row}_L D_H(a_H), and for which H + xy is still
(2,2)-sparse, is a certified response edge. Adding one leaves the row space
unchanged and raises the self-stress dimension by exactly one.
(Zheng, 2026, Section 2.2)
Lean code for Definition4.3.1●2 declarations
Associated Lean declarations
-
defdefined in RB31EndToEnd/Linear/DirectionResponse.leancomplete
def RB31E2E.DirectionStress.directionRowSpace.{u_1, u_2} {k : Type u_1} {V : Type u_2} [Field k] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → k) : Submodule k (V → Fin 3 → k)
def RB31E2E.DirectionStress.directionRowSpace.{u_1, u_2} {k : Type u_1} {V : Type u_2} [Field k] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → k) : Submodule k (V → Fin 3 → k)
The span of the actual labelled direction rows of `F`.
-
theoremdefined in RB31EndToEnd/Linear/DirectionResponse.leancomplete
theorem RB31E2E.DirectionStress.stress_augmentation_of_virtual_response.{u_1, u_2} {k : Type u_1} {V : Type u_2} [Field k] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → k) (f : RB31E2E.SimpleEdge V) (hf : f ∉ F) (hVirtualResponse : RB31E2E.DirectionStress.directionRow a f ∈ RB31E2E.DirectionStress.directionRowSpace F a) : RB31E2E.DirectionStress.directionStressDim (insert f F) a = RB31E2E.DirectionStress.directionStressDim F a + 1
theorem RB31E2E.DirectionStress.stress_augmentation_of_virtual_response.{u_1, u_2} {k : Type u_1} {V : Type u_2} [Field k] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → k) (f : RB31E2E.SimpleEdge V) (hf : f ∉ F) (hVirtualResponse : RB31E2E.DirectionStress.directionRow a f ∈ RB31E2E.DirectionStress.directionRowSpace F a) : RB31E2E.DirectionStress.directionStressDim (insert f F) a = RB31E2E.DirectionStress.directionStressDim F a + 1
The same theorem phrased directly as the common virtual-response certificate used by deletion branches.
Example 2.2 of Zheng (2026) is the case that arises in the
induction. If H[\{x,y,z\}] has exactly the edges xy and yz, and
a_x, a_y, a_z are distinct and collinear, then r_{xy}, r_{yz} and
r_{xz} span the same two-dimensional space; so xz is a certified response
edge whenever it can be added, and adding it raises the self-stress dimension
by one without raising the rank.
The row space is formalized as
directionRowSpace, quoted
here; its span runs over the edges of F rather than over all pairs, so
membership of a row in the row space is a condition on the graph as well as on
the placement.
/-- The span of the actual labelled direction rows of `F`. -/
def directionRowSpace (F : SimpleEdgeSet V) (a : V → Fin 3 → k) :
Submodule k (V → Fin 3 → k) :=
Submodule.span k (Set.range (fun e : F ↦ directionRow a e.1))
The second sentence of the definition — the row space is unchanged and the
self-stress dimension rises by exactly one — is proved rather than asserted.
Row-space invariance is
directionRowSpace_insert_eq_of_mem,
and the increment follows from it, since rank–nullity relates stress
dimension, rank and edge count. The result is stated twice under two names:
once as a general augmentation lemma, and once as
stress_augmentation_of_virtual_response,
the same statement in the paper's vocabulary.
The sparsity half of the paper's definition is not part of the Lean statement:
the augmentation lemma needs only that the edge is absent. Sparsity of
H + xy is proved separately, by
the addable-edge lemma, at the point of the
induction where the edge is added.