4.1. Direction rows over a coefficient field
-
RB31E2E.DirectionStress.directionRow[complete] -
RB31E2E.DirectionStress.directionEquilibrium[complete] -
RB31E2E.DirectionStress.directionStressDim[complete]
For a configuration b : U \to (L')^3 and distinct x, y \in U, the rigidity
row r_{xy}(b) is the vector whose x-block is b_x - b_y, whose
y-block is b_y - b_x, and whose other blocks vanish. The self-stress space
of (F, a) is the left kernel \ker D_F(a)^T.
(Zheng, 2026, Section 2.2)
Lean code for Definition4.1.1●3 definitions
Associated Lean declarations
-
RB31E2E.DirectionStress.directionRow[complete]
-
RB31E2E.DirectionStress.directionEquilibrium[complete]
-
RB31E2E.DirectionStress.directionStressDim[complete]
-
RB31E2E.DirectionStress.directionRow[complete] -
RB31E2E.DirectionStress.directionEquilibrium[complete] -
RB31E2E.DirectionStress.directionStressDim[complete]
-
defdefined in RB31EndToEnd/Linear/DirectionStress.leancomplete
def RB31E2E.DirectionStress.directionRow.{u_1, u_2} {k : Type u_1} {V : Type u_2} [Field k] [DecidableEq V] (a : V → Fin 3 → k) (e : RB31E2E.SimpleEdge V) : V → Fin 3 → k
def RB31E2E.DirectionStress.directionRow.{u_1, u_2} {k : Type u_1} {V : Type u_2} [Field k] [DecidableEq V] (a : V → Fin 3 → k) (e : RB31E2E.SimpleEdge V) : V → Fin 3 → k
The direction row of one edge, viewed as a load on all vertex-coordinate blocks. It is `a_source - a_target` at the source, its negative at the target, and zero elsewhere.
-
defdefined in RB31EndToEnd/Linear/DirectionStress.leancomplete
def RB31E2E.DirectionStress.directionEquilibrium.{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) : (↥F → k) →ₗ[k] V → Fin 3 → k
def RB31E2E.DirectionStress.directionEquilibrium.{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) : (↥F → k) →ₗ[k] V → Fin 3 → k
The transpose of the direction matrix. It sends edge weights to the three equilibrium coordinates at every vertex.
-
defdefined in RB31EndToEnd/Linear/DirectionStress.leancomplete
def RB31E2E.DirectionStress.directionStressDim.{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) : ℕ
def RB31E2E.DirectionStress.directionStressDim.{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) : ℕ
The finite dimension of the direction-stress space.
The formalization takes the transpose as primary. A placement is a function
V \to (\mathrm{Fin}\ 3 \to k), an edge weighting is a function on the edge
set, and the load a weighting induces at one vertex coordinate is the sum of
the direction rows against it.
directionEquilibrium is
that assignment bundled as a linear map; in its quoted body the proofs of
additivity and homogeneity render as ⋯, leaving the underlying coordinate
function. Its kernel is the self-stress space, and
directionStressDim is its
dimension — the number s of the ledger below, which the induction bounds.
An unordered edge has no distinguished source, so the formalization picks one
and defines the row symmetrically: the block at the chosen source is
a_{\text{source}} - a_{\text{target}} and the block at the target is its
negative, so exchanging the two gives back the same function of the vertices. The paper
writes r_{xy} and lets the symmetry pass without comment.
/-- The oriented difference vector carried by one simple edge. -/
def edgeDirection (a : V → Fin 3 → k) (e : SimpleEdge V) : Fin 3 → k :=
fun j ↦ a e.source j - a e.target j/--
The direction row of one edge, viewed as a load on all vertex-coordinate
blocks. It is `a_source - a_target` at the source, its negative at the
target, and zero elsewhere.
-/
def directionRow (a : V → Fin 3 → k) (e : SimpleEdge V) :
V → Fin 3 → k :=
fun v j ↦
(if e.source = v then edgeDirection a e j else 0) +
(if e.target = v then -(edgeDirection a e j) else 0)/-- One coordinate of the endpoint-equilibrium load of edge weights. -/
def directionEquilibriumCoordinate
(F : SimpleEdgeSet V) (a : V → Fin 3 → k)
(weight : F → k) (v : V) (j : Fin 3) : k :=
∑ e : F, weight e * directionRow a e.1 v j/--
The transpose of the direction matrix. It sends edge weights to the three
equilibrium coordinates at every vertex.
-/
def directionEquilibrium
(F : SimpleEdgeSet V) (a : V → Fin 3 → k) :
(F → k) →ₗ[k] (V → Fin 3 → k) where
toFun weight v j := directionEquilibriumCoordinate F a weight v j
map_add' x y := ⋯
map_smul' c x := ⋯/-- The actual direction-stress vector space. -/
abbrev DirectionStressSpace
(F : SimpleEdgeSet V) (a : V → Fin 3 → k) :=
LinearMap.ker (directionEquilibrium F a)/-- The finite dimension of the direction-stress space. -/
def directionStressDim
(F : SimpleEdgeSet V) (a : V → Fin 3 → k) : ℕ :=
Module.finrank k (DirectionStressSpace F a)