1.3. Local rigidity and the regular locus🔗

The formalization does not cite Asimow and Roth. For a finite simple graph in any dimension it proves the equivalence Theorem 1.1 needs of them: attaining the complete graph's maximum rigidity rank is the same condition as local rigidity at every placement of some open dense set. The argument is analytic, and it was added to the formalization after the paper was released. We recall the Euclidean vocabulary it is stated in, then the placements at which the comparison is made, and then the equivalence itself. Throughout, \rho_d(G) is the maximum rank of R_G over placements V \to \R^d, so \rho_3 is the rank function of the maximum-rank definition, and K is the complete graph on the vertices of G.

Distances are Euclidean, and taking them costs a change of norm. The coordinate space (\R^d)^V on which the rigidity operator is defined carries the supremum norm, so a placement is moved to its L^2 counterpart by toEuclideanPlacement before any distance is measured. The two spaces are continuously linearly isomorphic and hence homeomorphic, so each of the three notions above also has a native Euclidean form — EuclideanIsEquivalent, EuclideanIsCongruent and EuclideanIsLocallyRigid — and each of those is proved equivalent to the coordinate form it is written from.

Local rigidity concerns a neighbourhood of p and nothing beyond it: a distant equivalent placement may fail to be congruent to p, and no statement below asserts otherwise. Since congruence is equality of all pairwise distances, G is locally rigid at p exactly when the level set of its own squared edge-length map through p is contained, near p, in the level set of K's through p. By hasStrictFDerivAt_squaredLengthMap the derivative of the squared edge-length map at p is 2R_G(p), so map and operator have the same kernel and the same rank at every placement, and the rigidity matrix of (1.4) is the linearization of the edge-length constraints.

The necessity chapter's avoidance argument is the same interpolation along a segment, with the determinant of one body's core displacements in place of a minor of the rigidity operator.

Asimow and Roth prove this openness and density, and prove in addition that the complement is Lebesgue-null. The formalization does not prove the null complement, and the register has an entry for the difference. No step below needs it, since every use made of a regular placement here is a use of density.

Generic in the formalization means simultaneous regularity for every graph on the vertex set, and it is not algebraic independence of the coordinates; the two are nowhere identified. The open dense set in the statement below mentions no rank at all.

Two things separate this from the theorem above, and the register records both. Where Asimow and Roth state a rank formula in the dimension of the affine hull, the formalization compares with the complete graph on the same vertices, which agrees with the formula on frameworks large enough for it and stays correct on the small ones where it fails; the empty vertex set and dimension zero are included in the statement. And where the paper says generic, the formal statement says on an open dense set; whether those name the same class of placements is a reading question, and the reason this node is a deviation rather than a mapping.

Regularity of K is a hypothesis of the pointwise comparison and not a convenience. Two unit bars forming a straight three-vertex path in \R^3 are the standing example. At that collinear placement the path and K_3 both have rank 2, and yet one bar rotates about the middle vertex, so the path is not locally rigid there; K_3 attains its maximum rank 3 only off the line, so the placement is not regular for it. The equivalence above compares with the maximum rank of K rather than with its rank at p, and the pointwise form isLocallyRigid_iff_of_isGenericPlacement asks for a generic placement, which is regular for both graphs at once.