The rigidity matrix R(G,p) of a body-hinge framework

The definitions and rank lemmas of sec:molecular-rigidity-matrix, after Katoh and Tanigawa (2011, A proof of the molecular conjecture, Discrete Comput. Geom. 45, §§2.2–2.4 and 5). The dimension is written d = k + 1, so that the screw space is ⋀^k K^(k+2), of dimension D = (k+2 choose 2) (def:screw-space). A body-hinge framework is a multigraph with an element C(e) of the screw space at each edge, the supporting extensor of its hinge (def:hinge-constraint). The file proves:

• the hinge constraint S u − S v ∈ span C(e) and its form as D − 1 linear equations (def:hinge-constraint, def:hinge-row-block);
• the rows of R(G,p) and the infinitesimal motions, the space on which all the rows vanish (def:rigidity-matrix); the independence of the rows of an edge, of the rows of edges with ends of their own, and of the rows of a forest (lem:edge-rows-independent, lem:own-end-rows-independent, lem:forest-rows-independent); and the row space as the forms that vanish on the motions (lem:span-rigidityRows-eq-of-motions-eq);
• the trivial motions and the bound rank R(G,p) ≤ D(|V| − 1) (def:trivial-motions-rigid, lem:trivial-motions-rank-bound); KT Lemmas 5.1 and 5.3 (lem:rank-delete-vertex, lem:rank-parallel-full); and the comparison of two frameworks whose hinges have nested spans (lem:rank-rotation-semicont);
• the column operation and the blocks of independent forms with which Katoh and Tanigawa read the rank in their Cases II and III (KT eqs. (6.14)–(6.16) and (6.26)–(6.29), pp. 679 and 685–686; lem:case-III-columnop, lem:case-III-vanish-off-column, lem:case-III-transport-collapse, lem:case-II-placement-block-independent, lem:case-III-conditional-block).

No basis of the screw space is fixed. A row of R(G,p) is the linear form S ↦ r (S u − S v) on screw assignments, for an edge with ends u and v and a linear form r on the screw space that vanishes at C(e), and the rank of R(G,p) is the dimension of the span of the rows. The file also defines the transport of a framework along a linear automorphism of the screw space (mapExtensor, thm:projective-invariance) and the extensors that lie in a panel (ExtensorInPanel, def:genuine-hinge-realization). Bricks.lean proves the rank-addition lemmas (sec:molecular-rigidity-matrix-blocks).

The screw space (def:screw-space)

The number D = screwDim k, the screw space ScrewSpace K k with its constructor ScrewSpace.mk and value ScrewSpace.val, and its dimension D (screwSpace_finrank).

@[reducible, inline]

abbrev CombinatorialRigidity.Molecular.screwDim (k : ℕ) : ℕ

The number D (def:screw-space): screwDim k = (k+2 choose 2), which is D = (d+1 choose 2) for d = k + 1, the dimension of the space of screw centers of a body in K^d (Katoh and Tanigawa 2011, §2.2) and of the screw space (screwSpace_finrank).

Equations

• CombinatorialRigidity.Molecular.screwDim k = (k + 2).choose 2

theorem CombinatorialRigidity.Molecular.screwDim_one : screwDim 1 = 3

screwDim 1 = 3: the screw dimension of d = 2-dimensional (planar) body-hinge rigidity, two translations plus one planar rotation.

theorem CombinatorialRigidity.Molecular.screwDim_two : screwDim 2 = 6

screwDim 2 = 6: the screw dimension of d = 3-dimensional (spatial) body-hinge rigidity, three translations plus three spatial rotations.

def CombinatorialRigidity.Molecular.ScrewSpace (K : Type u_2) [Field K] (k : ℕ) : Type u_2

The screw space (def:screw-space): ScrewSpace K k is the degree-k piece ⋀[K]^k (Fin (k+2) → K) of the exterior algebra of K^(k+2), of dimension D = screwDim k (screwSpace_finrank). A screw center, the value of a screw assignment at a body, lies in it, and so do the supporting extensors of the hinges (affineSubspaceExtensor_mem_exteriorPower). No basis is fixed: the identification of the screw space with K^D enters only through its dimension.

It is a def, not an abbrev, so that unification at reducible and instance transparency does not unfold it to the subtype of the exterior algebra. ScrewSpace_def unfolds it, by rfl; the module instances below are those of the subtype; and ScrewSpace.mk, ScrewSpace.val and ScrewSpace.equivExteriorPower pass between the two.

Equations

• CombinatorialRigidity.Molecular.ScrewSpace K k = ↥(⋀[K]^k (Fin (k + 2) → K))

theorem CombinatorialRigidity.Molecular.ScrewSpace_def (K : Type u_2) [Field K] (k : ℕ) : ScrewSpace K k = ↥(⋀[K]^k (Fin (k + 2) → K))

ScrewSpace K k unfolds to the degree-k piece of the exterior algebra, by rfl at default transparency.

@[instance_reducible]

noncomputable instance CombinatorialRigidity.Molecular.instAddCommGroupScrewSpace {K : Type u_1} [Field K] (k : ℕ) : AddCommGroup (ScrewSpace K k)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance CombinatorialRigidity.Molecular.instModuleScrewSpace {K : Type u_1} [Field K] (k : ℕ) : Module K (ScrewSpace K k)

Equations

• One or more equations did not get rendered due to their size.

instance CombinatorialRigidity.Molecular.instFiniteDimensionalScrewSpace {K : Type u_1} [Field K] (k : ℕ) : FiniteDimensional K (ScrewSpace K k)

def CombinatorialRigidity.Molecular.ScrewSpace.mk {K : Type u_1} [Field K] {k : ℕ} (v : ExteriorAlgebra K (Fin (k + 2) → K)) (h : v ∈ ⋀[K]^k (Fin (k + 2) → K)) : ScrewSpace K k

The screw given by an element v of the degree-k piece of the exterior algebra (h). It stands for the anonymous constructor ⟨v, h⟩ of the subtype.

Equations

• CombinatorialRigidity.Molecular.ScrewSpace.mk v h = ⋯ ▸ ⟨v, h⟩

def CombinatorialRigidity.Molecular.ScrewSpace.val {K : Type u_1} [Field K] {k : ℕ} (C : ScrewSpace K k) : ExteriorAlgebra K (Fin (k + 2) → K)

The element of the exterior algebra that a screw is, which stands for the coercion Subtype.val of the subtype.

Equations

• C.val = ↑(⋯ ▸ C)

@[simp]

theorem CombinatorialRigidity.Molecular.ScrewSpace.val_mk {K : Type u_1} [Field K] {k : ℕ} (v : ExteriorAlgebra K (Fin (k + 2) → K)) (h : v ∈ ⋀[K]^k (Fin (k + 2) → K)) : (mk v h).val = v

theorem CombinatorialRigidity.Molecular.ScrewSpace.val_mem {K : Type u_1} [Field K] {k : ℕ} (C : ScrewSpace K k) : C.val ∈ ⋀[K]^k (Fin (k + 2) → K)

@[simp]

theorem CombinatorialRigidity.Molecular.ScrewSpace.val_smul {K : Type u_1} [Field K] {k : ℕ} (c : K) (C : ScrewSpace K k) : (c • C).val = c • C.val

@[simp]

theorem CombinatorialRigidity.Molecular.ScrewSpace.val_add {K : Type u_1} [Field K] {k : ℕ} (C D : ScrewSpace K k) : (C + D).val = C.val + D.val

@[simp]

theorem CombinatorialRigidity.Molecular.ScrewSpace.val_zero {K : Type u_1} [Field K] {k : ℕ} : val 0 = 0

@[simp]

theorem CombinatorialRigidity.Molecular.ScrewSpace.mk_val {K : Type u_1} [Field K] {k : ℕ} (C : ScrewSpace K k) : mk C.val ⋯ = C

theorem CombinatorialRigidity.Molecular.ScrewSpace.val_injective {K : Type u_1} [Field K] {k : ℕ} : Function.Injective val

theorem CombinatorialRigidity.Molecular.ScrewSpace.ext {K : Type u_1} [Field K] {k : ℕ} {C D : ScrewSpace K k} (h : C.val = D.val) : C = D

theorem CombinatorialRigidity.Molecular.ScrewSpace.ext_iff {K : Type u_1} [Field K] {k : ℕ} {C D : ScrewSpace K k} : C = D ↔ C.val = D.val

noncomputable def CombinatorialRigidity.Molecular.ScrewSpace.equivExteriorPower (K : Type u_2) [Field K] (k : ℕ) : ScrewSpace K k ≃ₗ[K] ↥(⋀[K]^k (Fin (k + 2) → K))

The screw space is linearly equivalent to the degree-k piece: the cast along ScrewSpace_def, whose additivity and homogeneity hold by rfl. The _apply and _symm_apply lemmas below state it as the cast.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CombinatorialRigidity.Molecular.ScrewSpace.equivExteriorPower_apply {K : Type u_1} [Field K] {k : ℕ} (C : ScrewSpace K k) : (equivExteriorPower K k) C = cast ⋯ C

@[simp]

theorem CombinatorialRigidity.Molecular.ScrewSpace.equivExteriorPower_symm_apply {K : Type u_1} [Field K] {k : ℕ} (C : ↥(⋀[K]^k (Fin (k + 2) → K))) : (equivExteriorPower K k).symm C = cast ⋯ C

theorem CombinatorialRigidity.Molecular.screwSpace_finrank {K : Type u_1} [Field K] (k : ℕ) : Module.finrank K (ScrewSpace K k) = screwDim k

The screw space has dimension D (def:screw-space): finrank K (ScrewSpace K k) = screwDim k. The degree-k piece of the exterior algebra of K^(k+2) has dimension (k+2 choose k) (exteriorPower.finrank_eq), which is (k+2 choose 2) by the symmetry of the binomial coefficients. The rank counts use this in place of a basis of the screw space.

theorem CombinatorialRigidity.Molecular.card_le_screwDim_of_linearIndependent {K : Type u_1} [Field K] {k m : ℕ} (c : Fin m → ScrewSpace K k) (h : LinearIndependent K c) : m ≤ screwDim k

At most D independent screws (lem:cycle-realization-dim-bound): a linearly independent family of m elements of the screw space has m ≤ D = screwDim k, as the space has dimension D (screwSpace_finrank, LinearIndependent.fintype_card_le_finrank). A cycle whose m supporting extensors are independent therefore has m ≤ D, the upper bound in the hypothesis 3 ≤ |V| ≤ D of Katoh and Tanigawa's Lemma 5.4 (p. 670).

Bounds on D

D ≥ 1 always, and D ≥ 2 and D ≥ 3 when d = k + 1 ≥ 2; at k = 0 the screw space is ⋀^0 K^2 = K, and D = 1. Also D − 2 ≤ D(m − 1) when m ≥ 2.

theorem CombinatorialRigidity.Molecular.one_le_screwDim {k : ℕ} : 1 ≤ screwDim k

D ≥ 1 (def:screw-space): (k+2 choose 2) ≠ 0, as 2 ≤ k + 2 (Nat.choose_eq_zero_iff).

theorem CombinatorialRigidity.Molecular.two_le_screwDim {k : ℕ} (hk : 1 ≤ k) : 2 ≤ screwDim k

D ≥ 2 when d ≥ 2 (def:screw-space): screwDim k ≥ 2 when k ≥ 1, that is, when d = k + 1 ≥ 2; at k = 0, D = 1. As screwDim 1 = 3 and n ↦ (n choose 2) is monotone (Nat.choose_mono).

theorem CombinatorialRigidity.Molecular.three_le_screwDim {k : ℕ} (hk : 1 ≤ k) : 3 ≤ screwDim k

D ≥ 3 when d ≥ 2 (def:screw-space): screwDim k ≥ 3 when k ≥ 1, as screwDim 1 = 3 and n ↦ (n choose 2) is monotone (Nat.choose_mono). With bodyBarDim n = screwDim k it gives 3 ≤ bodyBarDim n.

theorem CombinatorialRigidity.Molecular.screwDim_sub_two_le_mul {k m : ℕ} (hm : 2 ≤ m) : screwDim k - 2 ≤ screwDim k * (m - 1)

D − 2 ≤ D(m − 1) when m ≥ 2 (a step of lem:case-III-nested-rank-lower): so the lower bound D(m − 1) − (D − 2) of KT eq. (6.22) (p. 684, where D − 2 = 4) is a subtraction in ℕ that does not truncate. D − 2 ≤ D ≤ D(m − 1), as 1 ≤ m − 1.

Panels, and body-hinge frameworks (def:hinge-constraint)

The extensors that lie in a panel (ExtensorInPanel), and the structure BodyHingeFramework: a multigraph with a screw at each edge.

def CombinatorialRigidity.Molecular.ExtensorInPanel {K : Type u_1} [Field K] {k : ℕ} (C : ScrewSpace K k) (n : Fin (k + 2) → K) : Prop

An extensor in the panel with normal n (def:genuine-hinge-realization): a screw C lies in the panel with normal n if it is the extensor x₁ ∨ ⋯ ∨ x_k of k vectors of the hyperplane n^⊥ = {x | x ⬝ᵥ n = 0} of K^(k+2). When k ≥ 1, C = 0 lies in every panel (take x₁ = 0). At k = 0 the only extensor is that of the empty family, 1, so the predicate says C = 1, whatever n.

Equations

• CombinatorialRigidity.Molecular.ExtensorInPanel C n = ∃ (p : Fin k → Fin (k + 2) → K), C.val = CombinatorialRigidity.Molecular.extensor p ∧ ∀ (i : Fin k), p i ⬝ᵥ n = 0

theorem CombinatorialRigidity.Molecular.exists_extensor_eq_of_extensorInPanel {K : Type u_1} [Field K] {k : ℕ} [NeZero k] {C : ScrewSpace K k} {nv : Fin (k + 2) → K} (hC : C ≠ 0) (hP : ExtensorInPanel C nv) : ∃ (p : Fin k → Fin (k + 2) → K), p 0 ≠ 0 ∧ C = ScrewSpace.mk (extensor p) ⋯

A nonzero screw in a panel is decomposable, with a nonzero leading vector: if C ≠ 0 lies in a panel (ExtensorInPanel), then C is the extensor of k vectors, the first of them nonzero. The vectors are those ExtensorInPanel gives; a nonzero extensor has linearly independent vectors (extensor_ne_zero_iff_linearIndependent), so in particular p 0 ≠ 0.

structure CombinatorialRigidity.Molecular.BodyHingeFramework (K : Type u_2) [Field K] (k : ℕ) (α : Type u_3) (β : Type u_4) : Type (max (max u_2 u_3) u_4)

A body-hinge framework (G,p) in K^d, d = k + 1 (def:hinge-constraint): a multigraph G : Graph α β with, at each edge label e, an element supportExtensor e of the screw space ⋀^k K^(k+2), which stands for the supporting extensor C(p(e)) of the hinge p(e). The bodies are the elements of α, among which there may be bodies on no edge of G. When p(e) is the affine span of k points of K^(k+1), C(p(e)) is their extensor (ofHinge); for a panel-hinge framework it is the meet of the panels at the two ends of e (PanelHingeFramework.toBodyHinge). The extensor need not be nonzero, nor come from points.

Writing d = k + 1 avoids the subtractions d − 1 and d − 2 in the numbers of points.

• graph : Graph α β

  The multigraph: the bodies on its edges are its vertices, and the hinges its edges.

• supportExtensor : β → ScrewSpace K k

  The supporting extensor C(p(e)) at the edge label e, a screw of ⋀^k K^(k+2) (def:hinge-constraint). For points it is nonzero exactly when they are affinely independent (affineSubspaceExtensor_ne_zero_iff); for two panels, exactly when their normals are linearly independent (panelSupportExtensor_ne_zero_iff).

The rank equation in ℤ and in ℕ

Two facts of integer arithmetic for Case II (PanelHingeFramework.case_II_realization_all_k). There the rank equation N + (D − 1) = D(V − 1) − k holds in ℤ, where N = D(V − 2) − (k − 1) is the rank of the realization of G_v^{ab} and D(V − 1) − k the target rank of G (the count at the end of the proof of KT Lemma 6.8, p. 679). They give k.toNat ≤ D(V − 1) and D(V − 1) − k.toNat = N + (D − 1) in ℕ.

theorem CombinatorialRigidity.Molecular.toNat_le_of_add_pred_eq {D V N : ℕ} {k : ℤ} (hV : 1 ≤ V) (hD : 1 ≤ D) (hNpD : ↑N + (↑D - 1) = ↑D * (↑V - 1) - k) : k.toNat ≤ D * (V - 1)

k.toNat ≤ D(V − 1) from the rank equation N + (D − 1) = D(V − 1) − k: with N ≥ 0 and D ≥ 1, the left side is nonnegative, so k ≤ D(V − 1), and V ≥ 1 makes V − 1 a subtraction in ℕ that does not truncate.

theorem CombinatorialRigidity.Molecular.sub_toNat_eq_of_add_pred_eq {D V N : ℕ} {k : ℤ} (hk : 0 < k) (hV : 1 ≤ V) (hD : 1 ≤ D) (hNpD : ↑N + (↑D - 1) = ↑D * (↑V - 1) - k) : D * (V - 1) - k.toNat = N + (D - 1)

D(V − 1) − k.toNat = N + (D − 1) from the rank equation N + (D − 1) = D(V − 1) − k, when k > 0: then (k.toNat : ℤ) = k, and both sides are cast to ℤ, through toNat_le_of_add_pred_eq.

The hinge constraint and the hinge-row block (def:hinge-constraint, def:hinge-row-block)

The framework of a hinge assignment (ofHinge), the transport along an automorphism of the screw space (mapExtensor), the hinge-row block with its membership test (mem_hingeRowBlock_iff), and the hinge constraint S u − S v ∈ span C(p(e)) with its form as the D − 1 equations of the hinge-row block (hingeConstraint_iff_hingeRowBlock).

noncomputable def CombinatorialRigidity.Molecular.BodyHingeFramework.ofHinge {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (G : Graph α β) (hinge : β → Fin k → Fin (k + 1) → K) : BodyHingeFramework K k α β

The framework of a hinge assignment (the affine hinges of def:hinge-constraint): each edge label e gets k points hinge e of K^(k+1), and its supporting extensor is affineSubspaceExtensor (hinge e), the extensor of the homogenized points, which is nonzero exactly when the points are affinely independent (affineSubspaceExtensor_ne_zero_iff). The hinges of a panel-hinge framework are given by PanelHingeFramework.toBodyHinge instead.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.ofHinge_graph {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (G : Graph α β) (hinge : β → Fin k → Fin (k + 1) → K) : (ofHinge G hinge).graph = G

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.ofHinge_supportExtensor_val {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (G : Graph α β) (hinge : β → Fin k → Fin (k + 1) → K) (e : β) : ((ofHinge G hinge).supportExtensor e).val = affineSubspaceExtensor (hinge e)

noncomputable def CombinatorialRigidity.Molecular.BodyHingeFramework.mapExtensor {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (Λ : ScrewSpace K k ≃ₗ[K] ScrewSpace K k) : BodyHingeFramework K k α β

The framework transported along a linear automorphism Λ of the screw space (thm:projective-invariance): the same multigraph, with the supporting extensor Λ C(p(e)) at each edge e. A projective transformation of K³ acts on the screw space ⋀² K⁴ in this way (Crapo and Whiteley 1982, §3.6). It leaves the motions unchanged up to Λ (Molecule/ProjectiveInvariance.lean, thm:projective-invariance) and the rank of the rigidity matrix unchanged (finrank_span_rigidityRows_mapExtensor, lem:screw-map-rows).

Equations

• F.mapExtensor Λ = { graph := F.graph, supportExtensor := fun (e : β) => Λ (F.supportExtensor e) }

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.mapExtensor_graph {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (Λ : ScrewSpace K k ≃ₗ[K] ScrewSpace K k) : (F.mapExtensor Λ).graph = F.graph

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.mapExtensor_supportExtensor {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (Λ : ScrewSpace K k ≃ₗ[K] ScrewSpace K k) (e : β) : (F.mapExtensor Λ).supportExtensor e = Λ (F.supportExtensor e)

def CombinatorialRigidity.Molecular.BodyHingeFramework.hingeConstraint {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (S : α → ScrewSpace K k) (e : β) (u v : α) : Prop

The hinge constraint at an edge label e with ends u and v (def:hinge-constraint; KT eq. (2.3), p. 653): a screw assignment S : α → ScrewSpace K k satisfies it if S u − S v ∈ span C(p(e)) = Submodule.span K {C(p(e))}.

Equations

• F.hingeConstraint S e u v = (S u - S v ∈ K ∙ F.supportExtensor e)

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeConstraint_iff {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (S : α → ScrewSpace K k) (e : β) (u v : α) : F.hingeConstraint S e u v ↔ S u - S v ∈ K ∙ F.supportExtensor e

noncomputable def CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRowBlock {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (e : β) : Submodule K (Module.Dual K (ScrewSpace K k))

The hinge-row block r(p(e)) at an edge label e (def:hinge-row-block; KT §2.4, p. 653): the space (span C(p(e)))^⊥ of the linear forms on the screw space that vanish on span C(p(e)), its dual annihilator. When C(p(e)) ≠ 0 it has dimension D − 1 (finrank_hingeRowBlock), and the D − 1 rows r_i(p(e)) of Katoh and Tanigawa's matrix r(p(e)), read through the dot product of K^D, are a basis of it.

No basis of the screw space is fixed: the dot product r_i(p(e)) · x is the value r x of a form r of the block, and the equivalence of the hinge constraint with the vanishing of these values is the identity (span C)^⊥⊥ = span C (Subspace.dualAnnihilator_dualCoannihilator_eq).

Equations

• F.hingeRowBlock e = (K ∙ F.supportExtensor e).dualAnnihilator

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRowBlock_apply {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (e : β) : F.hingeRowBlock e = (K ∙ F.supportExtensor e).dualAnnihilator

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.mem_hingeRowBlock_iff {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (e : β) (r : Module.Dual K (ScrewSpace K k)) : r ∈ F.hingeRowBlock e ↔ r (F.supportExtensor e) = 0

A form lies in the hinge-row block if and only if it vanishes at the extensor (def:hinge-row-block): r ∈ F.hingeRowBlock e ↔ r (C(e)) = 0. The block is the space of the forms that vanish on span {C(e)} (hingeRowBlock), and a form vanishes on the multiples of C(e) if and only if it vanishes at C(e) (the remark after def:hinge-row-block).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeConstraint_iff_hingeRowBlock {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (S : α → ScrewSpace K k) (e : β) (u v : α) : F.hingeConstraint S e u v ↔ ∀ r ∈ F.hingeRowBlock e, r (S u - S v) = 0

The hinge constraint as D − 1 linear equations (def:hinge-row-block): a screw assignment S satisfies the hinge constraint at e with ends u and v (def:hinge-constraint) if and only if r (S u − S v) = 0 for every form r of the hinge-row block F.hingeRowBlock e. This is Katoh and Tanigawa's (S(u) − S(v)) · r_i(p(e)) = 0 for 1 ≤ i ≤ D − 1 (KT §2.4, p. 653).

One direction is the definition of the dual annihilator; the other is the identity (span C)^⊥⊥ = span C of a finite-dimensional vector space over a field (Subspace.dualAnnihilator_dualCoannihilator_eq).

The rows of R(G,p) (def:rigidity-matrix)

The relative screw screwDiff u v, the form hingeRow u v r : S ↦ r (S u − S v) and the set rigidityRows of rows, with the independence of the rows of an edge (lem:edge-rows-independent) and the spans of families of rows.

noncomputable def CombinatorialRigidity.Molecular.BodyHingeFramework.screwDiff {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (u v : α) : (α → ScrewSpace K k) →ₗ[K] ScrewSpace K k

The relative screw of two bodies (def:rigidity-matrix's S(u) − S(v)): the linear map screwDiff u v : S ↦ S u − S v from screw assignments to the screw space, the difference of the projections at u and at v. The hinge constraint (def:hinge-constraint) and the rows of R(G,p) (hingeRow) are built from it.

Equations

• CombinatorialRigidity.Molecular.BodyHingeFramework.screwDiff u v = LinearMap.proj u - LinearMap.proj v

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.screwDiff_apply {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (u v : α) (S : α → ScrewSpace K k) : (screwDiff u v) S = S u - S v

noncomputable def CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (u v : α) (r : Module.Dual K (ScrewSpace K k)) : Module.Dual K (α → ScrewSpace K k)

A row of R(G,p) (def:rigidity-matrix; KT §2.4, p. 654): for bodies u, v and a linear form r on the screw space, the linear form hingeRow u v r : S ↦ r (S u − S v) on screw assignments, r ∘ₗ screwDiff u v. For an edge e from u to v and r in the hinge-row block r(p(e)) (def:hinge-row-block), it is a row of R(G,p): the row with r in the columns of u, −r in those of v, and zeros elsewhere. It depends only on u, v and r; the edge enters in the set of rows (rigidityRows), whose span is the row space and whose forms all vanish exactly on the motions (infinitesimalMotions_eq_dualCoannihilator).

Equations

• CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow u v r = r ∘ₗ CombinatorialRigidity.Molecular.BodyHingeFramework.screwDiff u v

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow_apply {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (u v : α) (r : Module.Dual K (ScrewSpace K k)) (S : α → ScrewSpace K k) : (hingeRow u v r) S = r (S u - S v)

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow_self {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (a : α) (r : Module.Dual K (ScrewSpace K k)) : hingeRow a a r = 0

The row of a loop is zero (def:rigidity-matrix): hingeRow a a r = 0, as S a − S a = 0. So a loop adds only zero rows, which hasPencilRealization_of_isLoopAt and span_rigidityRows_eq_of_eq_off_loops use.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.screwDiff_surjective {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {u v : α} (huv : u ≠ v) : Function.Surjective ⇑(screwDiff u v)

The relative screw is onto at distinct bodies (def:rigidity-matrix): for u ≠ v, every screw x is S u − S v for S = Function.update 0 u x. So its dual map hingeRow u v = (screwDiff u v).dualMap (hingeRow_eq_dualMap) is injective, and the rows of an edge with distinct ends are independent (linearIndependent_hingeRow).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow_eq_dualMap {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (u v : α) (r : Module.Dual K (ScrewSpace K k)) : hingeRow u v r = (screwDiff u v).dualMap r

A row is the dual map of the relative screw applied to its form (def:rigidity-matrix): hingeRow u v r = (screwDiff u v).dualMap r, by rfl; linearIndependent_hingeRow reads injectivity off it (LinearMap.dualMap_injective_of_surjective).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow_swap {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (u v : α) (r : Module.Dual K (ScrewSpace K k)) : hingeRow u v r = hingeRow v u (-r)

Reversing an edge negates the form of a row (def:rigidity-matrix): hingeRow u v r = hingeRow v u (-r), as S u − S v = −(S v − S u). The hinge-row block is a subspace, so the rows of an edge taken in the two orientations are the same set of forms. The span identities that match the ends of a row to those of a link up to order (IsLink.eq_and_eq_or_eq_and_eq) use it.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow_funLeft_dualMap {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (u v : α) (r : Module.Dual K (ScrewSpace K k)) (ρ : α → α) : (LinearMap.funLeft K (ScrewSpace K k) ρ).dualMap (hingeRow u v r) = hingeRow (ρ u) (ρ v) r

Relabelling the bodies moves the ends of a row (the relabelling of KT eq. (6.31), p. 687): for any map ρ : α → α, the transpose of funLeft ρ : S ↦ S ∘ ρ sends hingeRow u v r to hingeRow (ρ u) (ρ v) r, as (hingeRow u v r) (S ∘ ρ) = r (S (ρ u) − S (ρ v)). The map ρ need not be invertible. Case III's relabelled frameworks use it (lem:case-III-chain-relabel-rows, lem:case-III-chain-eq666).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow_sub_hingeRow_eq {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (u v w : α) (r : Module.Dual K (ScrewSpace K k)) : hingeRow u w r - hingeRow v w r = hingeRow u v r

Two rows with a common end and form subtract to a row (lem:case-III-transport-collapse; KT eqs. (6.26)–(6.27), p. 685): hingeRow u w r − hingeRow v w r = hingeRow u v r, as (S u − S w) − (S v − S w) = S u − S v. In Case III the row of vb in R(G, q₀) minus the row of ab in R(G_v^{ab}, q) with the same form is the form S ↦ x (S v − S a) (PanelHingeFramework.panelRow_vb_sub_panelRow_ab_eq_hingeRow_va).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.linearIndependent_hingeRow {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {ι : Type u_4} {u v : α} (huv : u ≠ v) {r : ι → Module.Dual K (ScrewSpace K k)} (hr : LinearIndependent K r) : LinearIndependent K fun (i : ι) => hingeRow u v (r i)

The forms of one edge are independent (lem:edge-rows-independent, its claim for linear forms): for u ≠ v and linearly independent forms r i on the screw space, the forms hingeRow u v (r i) on screw assignments are linearly independent. hingeRow u v is the dual map of screwDiff u v (hingeRow_eq_dualMap), which is onto (screwDiff_surjective), so it is injective (LinearMap.dualMap_injective_of_surjective) and keeps the family independent (LinearIndependent.map').

def CombinatorialRigidity.Molecular.BodyHingeFramework.rigidityRows {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : Set (Module.Dual K (α → ScrewSpace K k))

The rows of R(G,p) (def:rigidity-matrix; KT §2.4, pp. 653–654): the set of the forms hingeRow u v r on screw assignments, over the links e of G from u to v and the forms r of the hinge-row block r(p(e)) (def:hinge-row-block). Its span is the row space of R(G,p), whose dimension is the rank, and the forms all vanish exactly on the motions Z(G,p) (infinitesimalMotions_eq_dualCoannihilator). A link is taken in both orientations, which give the same forms (hingeRow_swap). In place of the (D − 1)|E| × D|V| matrix, the rank arguments work with this set and the dual space.

Equations

• One or more equations did not get rendered due to their size.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.exists_edgeIndexed_combination_of_mem_span_rigidityRows {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) {φ : Module.Dual K (α → ScrewSpace K k)} (hφ : φ ∈ Submodule.span K F.rigidityRows) : ∃ (n : ℕ) (c : Fin n → K) (ev : Fin n → β) (uv : Fin n → α) (vv : Fin n → α) (rv : Fin n → Module.Dual K (ScrewSpace K k)), (∀ (j : Fin n), F.graph.IsLink (ev j) (uv j) (vv j)) ∧ (∀ (j : Fin n), rv j ∈ F.hingeRowBlock (ev j)) ∧ φ = ∑ j : Fin n, c j • hingeRow (uv j) (vv j) (rv j)

A form in the row space is a combination of rows, edge by edge (def:rigidity-matrix): a form φ ∈ span F.rigidityRows is ∑ j, c j • hingeRow (uv j) (vv j) (rv j) for finitely many links ev j from uv j to vv j and forms rv j of their hinge-row blocks. Submodule.mem_span_set' gives a finite combination of rows, and each row is unpacked to its link and form.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.span_rigidityRows_eq_of_eq_off_loops {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F F' : BodyHingeFramework K k α β) (hG : F.graph = F'.graph) (h : ∀ (e : β) (u v : α), F.graph.IsLink e u v → u ≠ v → F.supportExtensor e = F'.supportExtensor e) : Submodule.span K F.rigidityRows = Submodule.span K F'.rigidityRows

The rows read the hinges only at the links between distinct bodies (a step of lem:generic-yields-genuine-hinge; def:rigidity-matrix): two body-hinge frameworks on the same multigraph whose supporting extensors agree at every link between two distinct bodies have the same row space. The rows of a loop are zero (hingeRow_self), so the hinge at a loop, like the extensor at a label outside the edges, enters no row. hasPanelRealization_of_generic replaces the hinge at each loop so.

The infinitesimal motions Z(G,p) (def:rigidity-matrix)

The motions as the space on which all the rows vanish (infinitesimalMotions_eq_dualCoannihilator), the row space as the forms that vanish on the motions (span_rigidityRows_eq_dualAnnihilator_infinitesimalMotions), the dimension D − 1 of a hinge-row block (finrank_hingeRowBlock), and families of independent rows.

def CombinatorialRigidity.Molecular.BodyHingeFramework.IsInfinitesimalMotion {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (S : α → ScrewSpace K k) : Prop

An infinitesimal motion of a body-hinge framework (G,p) (def:rigidity-matrix; KT §2.3, p. 653): a screw assignment S : α → ScrewSpace K k that satisfies the hinge constraint (def:hinge-constraint) at every link of G, that is, S u − S v ∈ span C(p(e)) whenever e links u and v.

These are the vectors of the null space of Katoh and Tanigawa's rigidity matrix R(G,p): the rows of e = uv carry r(p(e)) in the columns of u and −r(p(e)) in those of v, so the rows of e vanish at S exactly when the hinge constraint holds at e (def:hinge-row-block). The matrix itself is not formed; its rows are rigidityRows.

Equations

• F.IsInfinitesimalMotion S = ∀ (e : β) (u v : α), F.graph.IsLink e u v → F.hingeConstraint S e u v

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.isInfinitesimalMotion_iff {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (S : α → ScrewSpace K k) : F.IsInfinitesimalMotion S ↔ ∀ (e : β) (u v : α), F.graph.IsLink e u v → S u - S v ∈ K ∙ F.supportExtensor e

def CombinatorialRigidity.Molecular.BodyHingeFramework.infinitesimalMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : Submodule K (α → ScrewSpace K k)

The space Z(G,p) of infinitesimal motions (def:rigidity-matrix): the submodule of the screw assignments α → ScrewSpace K k that are infinitesimal motions (IsInfinitesimalMotion), the null space ker R(G,p) of Katoh and Tanigawa (KT p. 654). Each hinge constraint asks for membership in the subspace span C(p(e)), so the motions form a subspace.

Equations

• F.infinitesimalMotions = { carrier := {S : α → CombinatorialRigidity.Molecular.ScrewSpace K k | F.IsInfinitesimalMotion S}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.mem_infinitesimalMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (S : α → ScrewSpace K k) : S ∈ F.infinitesimalMotions ↔ F.IsInfinitesimalMotion S

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.infinitesimalMotions_eq_of_isLink_supportExtensor {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F F' : BodyHingeFramework K k α β) (hgraph : F'.graph = F.graph) (hext : ∀ (e : β) (u v : α), F.graph.IsLink e u v → F'.supportExtensor e = F.supportExtensor e) : F.infinitesimalMotions = F'.infinitesimalMotions

The motions read the supporting extensors only at the links (def:rigidity-matrix): two frameworks on the same multigraph whose supporting extensors agree at every edge label that links two bodies have the same motions, as the hinge constraints are taken only at the links (IsInfinitesimalMotion). So changing the extensors at labels that are not edges of the graph, as withNormal does at a body on no edge, leaves the motions unchanged (PanelHingeFramework.toBodyHinge_withNormal_infinitesimalMotions_eq).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.infinitesimalMotions_eq_of_isLink_span_supportExtensor {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F F' : BodyHingeFramework K k α β) (hgraph : F'.graph = F.graph) (hspan : ∀ (e : β) (u v : α), F.graph.IsLink e u v → K ∙ F'.supportExtensor e = K ∙ F.supportExtensor e) : F.infinitesimalMotions = F'.infinitesimalMotions

The motions read only the spans of the supporting extensors at the links (def:rigidity-matrix): the form of infinitesimalMotions_eq_of_isLink_supportExtensor in which the two frameworks' extensors at each link span the same line. The hinge constraint is membership in span {C(p(e))}, so only the span enters. Changing the sign of an extensor, as recording the ends of an edge in the other order does (panelSupportExtensor_swap), changes the extensor but not its span.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.infinitesimalMotions_eq_dualCoannihilator {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : F.infinitesimalMotions = (Submodule.span K F.rigidityRows).dualCoannihilator

The motions are the screw assignments at which every row vanishes (def:rigidity-matrix; KT §2.4, p. 654):

F.infinitesimalMotions = (Submodule.span K F.rigidityRows).dualCoannihilator.

The dual coannihilator of a span is the common kernel of its generators (Submodule.coe_dualCoannihilator_span). So this says that S is a motion exactly when hingeRow u v r vanishes at S for every link e from u to v and every form r of the hinge-row block at e, that is, by hingeConstraint_iff_hingeRowBlock, when S satisfies every hinge constraint.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.span_rigidityRows_eq_dualAnnihilator_infinitesimalMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} [Finite α] (F : BodyHingeFramework K k α β) : Submodule.span K F.rigidityRows = F.infinitesimalMotions.dualAnnihilator

The row space is the space of forms that vanish on the motions (lem:span-rigidityRows-eq-of-motions-eq): for finitely many bodies, span F.rigidityRows = Z(G,p).dualAnnihilator. The motions are the common kernel of the rows (infinitesimalMotions_eq_dualCoannihilator), and in the dual of a finite-dimensional space a subspace is the annihilator of its kernel (Subspace.dualCoannihilator_dualAnnihilator_eq).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.span_rigidityRows_eq_of_infinitesimalMotions_eq {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} [Finite α] (F G : BodyHingeFramework K k α β) (h : F.infinitesimalMotions = G.infinitesimalMotions) : Submodule.span K F.rigidityRows = Submodule.span K G.rigidityRows

Frameworks with the same motions have the same row space (lem:span-rigidityRows-eq-of-motions-eq): for finitely many bodies, two body-hinge frameworks with the same infinitesimal motions have the same row space, and so the same rank, by span_rigidityRows_eq_dualAnnihilator_infinitesimalMotions. The frameworks need not be rigid. PanelHingeFramework.infinitesimalMotions_ofNormals_eq_of_ends_swap gives such an equality of motions.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.finrank_hingeRowBlock {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) {e : β} (he : F.supportExtensor e ≠ 0) : Module.finrank K ↥(F.hingeRowBlock e) = screwDim k - 1

A hinge-row block has dimension D − 1 (def:hinge-row-block): when the supporting extensor C(p(e)) is nonzero, finrank K (F.hingeRowBlock e) = screwDim k − 1. The extensor spans a line of the D-dimensional screw space (finrank_span_singleton, screwSpace_finrank), and the dimension of a dual annihilator is the codimension (Subspace.finrank_add_finrank_dualAnnihilator_eq). This is the count 1 ≤ i ≤ D − 1 of the rows of Katoh and Tanigawa's r(p(e)).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.exists_independent_rigidityRows_of_edge {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) {e : β} {u v : α} (huv : u ≠ v) (hlink : F.graph.IsLink e u v) (he : F.supportExtensor e ≠ 0) : ∃ (r : Fin (screwDim k - 1) → Module.Dual K (α → ScrewSpace K k)), LinearIndependent K r ∧ ∀ (i : Fin (screwDim k - 1)), r i ∈ F.rigidityRows

An edge gives D − 1 independent rows (lem:edge-rows-independent, its form for rows): if e links u ≠ v and C(p(e)) ≠ 0, there are D − 1 = screwDim k − 1 linearly independent rows of R(G,p) at e. They are hingeRow u v applied to a basis of the hinge-row block, which has dimension D − 1 (finrank_hingeRowBlock, Submodule.exists_linearIndependent_fin_of_finrank_eq), and they are independent by linearIndependent_hingeRow.

The column operation and blocks of independent forms (KT eqs. (6.14)–(6.29))

The column operation of KT eqs. (6.14)–(6.15) (columnOp), the forms that depend only on the screw of one body, and the joint independence of a family of forms independent at a body v with a family of forms that vanish at the screw assignments that vanish off v (linearIndependent_sum_pinned_block), with its variants for Cases II and III.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.dualMap_eq_comp_single_proj_of_vanish_off {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] (f : Module.Dual K (α → ScrewSpace K k)) (v : α) (hvanish : ∀ (S : α → ScrewSpace K k), S v = 0 → f S = 0) : f = (f ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v) ∘ₗ LinearMap.proj v

A form that vanishes where S v = 0 depends only on S v (lem:case-III-vanish-off-column; the form of KT eq. (6.28), p. 686): if f S = 0 for every screw assignment S with S v = 0, then f = (f ∘ₗ single v) ∘ₗ proj v, that is, f S = f (single v (S v)). The assignment S − single v (S v) vanishes at v, so f kills it. In KT eq. (6.28), the row operations leave a row whose entries outside the columns of v are zero.

noncomputable def CombinatorialRigidity.Molecular.BodyHingeFramework.columnOp {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] {v a : α} (hva : v ≠ a) : (α → ScrewSpace K k) ≃ₗ[K] α → ScrewSpace K k

The column operation Φ (lem:case-III-columnop; KT eqs. (6.14)–(6.15), p. 679): for bodies v ≠ a, the linear automorphism Φ S = Function.update S v (S v + S a) of the screw assignments, with inverse S ↦ Function.update S v (S v − S a); both fix the value at a, as a ≠ v. Replacing each row f of a rigidity matrix by f ∘ₗ Φ adds the columns of v to those of a, and leaves the rank unchanged. The row hingeRow v a ρ becomes S ↦ ρ (S v) (hingeRow_comp_columnOp_apply).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.columnOp_apply {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] {v a : α} (hva : v ≠ a) (S : α → ScrewSpace K k) (a✝ : α) : (columnOp hva) S a✝ = Function.update S v (S v + S a) a✝

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.columnOp_apply_single {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] {v b : α} (hvb : v ≠ b) (x : ScrewSpace K k) : (columnOp hvb) ((LinearMap.single K (fun (x : α) => ScrewSpace K k) v) x) = (LinearMap.single K (fun (x : α) => ScrewSpace K k) v) x

Φ fixes the screw assignments that vanish off v (from the proof of lem:case-III-columnop): for v ≠ b and Φ = columnOp hvb, Φ (single v x) = single v x. At v the value is x + 0, as b ≠ v, and elsewhere Φ changes nothing.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.comp_columnOp_comp_single {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] {v b : α} (hvb : v ≠ b) (g : Module.Dual K (α → ScrewSpace K k)) : (g ∘ₗ ↑(columnOp hvb)) ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v = g ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v

Composing with Φ keeps a form's columns of v (from the proof of lem:case-III-columnop): (g ∘ₗ Φ) ∘ₗ single v = g ∘ₗ single v for every form g on screw assignments, by columnOp_apply_single.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow_comp_columnOp_apply {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] {v a : α} (hva : v ≠ a) (ρ : Module.Dual K (ScrewSpace K k)) (S : α → ScrewSpace K k) : (hingeRow v a ρ) ((columnOp hva) S) = ρ (S v)

After Φ, the form hingeRow v a ρ reads only S v (lem:case-III-columnop; KT eqs. (6.14)–(6.16), p. 679): (hingeRow v a ρ) (Φ S) = ρ (S v), as Φ S has the value S v + S a at v and S a at a.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.hingeRow_comp_columnOp_vanish_off {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] {v a : α} (hva : v ≠ a) (ρ : Module.Dual K (ScrewSpace K k)) (S : α → ScrewSpace K k) (hS : S v = 0) : (hingeRow v a ρ) ((columnOp hva) S) = 0

After Φ, the form hingeRow v a ρ vanishes where S v = 0 (lem:case-III-columnop): by hingeRow_comp_columnOp_apply, its value is ρ (S v) = ρ 0 = 0.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.comp_columnOp_eq_comp_single_proj {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] {v a : α} (hva : v ≠ a) (ρ : Module.Dual K (ScrewSpace K k)) : hingeRow v a ρ ∘ₗ ↑(columnOp hva) = ((hingeRow v a ρ ∘ₗ ↑(columnOp hva)) ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v) ∘ₗ LinearMap.proj v

After Φ, the form hingeRow v a ρ factors through S v (lem:case-III-transport-collapse, its last claim; KT eq. (6.28), p. 686): with w = (hingeRow v a ρ) ∘ₗ Φ, w = (w ∘ₗ single v) ∘ₗ proj v. By hingeRow_comp_columnOp_vanish_off, w vanishes where S v = 0, and dualMap_eq_comp_single_proj_of_vanish_off applies.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.linearIndependent_hingeRow_star {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {J : Type u_4} [Finite J] {I : J → Type u_5} [∀ (j : J), Finite (I j)] {v : α} {w : J → α} (hw : Function.Injective w) (hwv : ∀ (j : J), w j ≠ v) {r : (j : J) → I j → Module.Dual K (ScrewSpace K k)} (hr : ∀ (j : J), LinearIndependent K (r j)) : LinearIndependent K fun (p : (j : J) × I j) => hingeRow (w p.fst) v (r p.fst p.snd)

The forms of a star are independent (lem:own-end-rows-independent, the case of a star): let w : J → α be distinct bodies other than a body v, and for each j let the forms r j i on the screw space be linearly independent. Then the forms hingeRow (w j) v (r j i) over Σ j, I j are linearly independent.

Evaluate a vanishing combination at Function.update 0 (w j₀) x. The forms of j ≠ j₀ vanish there, as w j ≠ w j₀ and v ≠ w j₀, and those of j₀ take the values r j₀ i x. So the coefficients of j₀ give a vanishing combination of the forms r j₀ i, and they are zero.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.linearIndependent_sum_pinned_block {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {ιn : Type u_4} {ιo : Type u_5} [Finite ιn] [Finite ιo] [DecidableEq α] {v : α} {rn : ιn → Module.Dual K (α → ScrewSpace K k)} {ro : ιo → Module.Dual K (α → ScrewSpace K k)} (hold : ∀ (j : ιo) (x : ScrewSpace K k), (ro j) (Function.update 0 v x) = 0) (hnewpin : LinearIndependent K fun (i : ιn) => rn i ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v) (holdindep : LinearIndependent K ro) : LinearIndependent K (Sum.elim rn ro)

Forms independent at v and forms vanishing at v are jointly independent (lem:case-II-placement-block-independent): let rn be forms on screw assignments whose restrictions to the assignments that vanish off v, rn i ∘ₗ single v, are linearly independent (hnewpin), and ro linearly independent forms (holdindep) that vanish at those assignments (hold). Then Sum.elim rn ro is linearly independent.

Evaluate a vanishing combination at Function.update 0 v x: the forms ro vanish there, so the coefficients of rn vanish by hnewpin; what is left is a vanishing combination of ro.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.linearIndependent_sum_restriction_block {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {ιt : Type u_4} {ιb : Type u_5} [Finite ιt] [Finite ιb] [DecidableEq α] {v : α} {top : ιt → Module.Dual K (α → ScrewSpace K k)} {bot : ιb → Module.Dual K (α → ScrewSpace K k)} (htopvanish : ∀ (i : ιt) (S : α → ScrewSpace K k), S v = 0 → (top i) S = 0) (htoppin : LinearIndependent K fun (i : ιt) => top i ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v) (hbotrestrict : LinearIndependent K fun (j : ιb) => bot j ∘ₗ (LinearMap.id - LinearMap.single K (fun (x : α) => ScrewSpace K k) v ∘ₗ LinearMap.proj v)) : LinearIndependent K (Sum.elim top bot)

Forms that depend only on S v, and forms independent off v (a step of lem:case-III-candidate-row; the shape of KT eq. (6.29), p. 686): let the forms top vanish where S v = 0 (htopvanish), with restrictions to the assignments that vanish off v linearly independent (htoppin), and let the restrictions of the forms bot to the other bodies, bot j ∘ₗ (id − single v ∘ₗ proj v), be linearly independent (hbotrestrict). Then Sum.elim top bot is linearly independent.

Evaluate a vanishing combination at S with its value at v replaced by 0: the forms top vanish there, so the coefficients of bot vanish by hbotrestrict; then those of top vanish by htoppin. It is linearIndependent_sum_pinned_block with the roles of the columns of v and of the other columns exchanged.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.linearIndependent_sum_pinned_block_augment_block {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {ιn : Type u_4} {ιo : Type u_5} {ιc : Type u_6} [Finite ιn] [Finite ιo] [Finite ιc] [DecidableEq α] {v : α} {rn : ιn → Module.Dual K (α → ScrewSpace K k)} {ro : ιo → Module.Dual K (α → ScrewSpace K k)} {wc : ιc → Module.Dual K (α → ScrewSpace K k)} (hold : ∀ (j : ιo) (x : ScrewSpace K k), (ro j) (Function.update 0 v x) = 0) (hnewpinaug : LinearIndependent K (Sum.elim (fun (i : ιn) => rn i ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v) fun (i : ιc) => wc i ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v)) (holdindep : LinearIndependent K ro) : LinearIndependent K (Sum.elim (Sum.elim rn wc) ro)

Forms independent at v, in two families, and forms vanishing at v (a step of lem:case-III-conditional-block): if the restrictions of the forms rn and wc to the screw assignments that vanish off v are jointly linearly independent (hnewpinaug), and the forms ro are as in linearIndependent_sum_pinned_block (hold, holdindep), then Sum.elim (Sum.elim rn wc) ro is linearly independent: that lemma, with Sum.elim rn wc as the first family.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.linearIndependent_sum_pinned_block_augment {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {ιn : Type u_4} {ιo : Type u_5} [Finite ιn] [Finite ιo] [DecidableEq α] {v : α} {rn : ιn → Module.Dual K (α → ScrewSpace K k)} {ro : ιo → Module.Dual K (α → ScrewSpace K k)} {w : Module.Dual K (α → ScrewSpace K k)} (hold : ∀ (j : ιo) (x : ScrewSpace K k), (ro j) (Function.update 0 v x) = 0) (hnewpinaug : LinearIndependent K (Sum.elim (fun (i : ιn) => rn i ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v) fun (x : Unit) => w ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v)) (holdindep : LinearIndependent K ro) : LinearIndependent K (Sum.elim (Sum.elim rn fun (x : Unit) => w) ro)

Two blocks of independent forms, with one more form independent at v (lem:case-III-conditional-block; for KT eq. (6.29), p. 686): if the restrictions of the forms rn and of a form w to the screw assignments that vanish off v are linearly independent, and the forms ro are linearly independent and vanish at those assignments, then rn, w and ro are jointly linearly independent. It is the case ιc = Unit of linearIndependent_sum_pinned_block_augment_block.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.linearIndependent_sum_augment_candidateRow_restriction {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [DecidableEq α] {v a : α} (hva : v ≠ a) {ιn : Type u_4} {ιo : Type u_5} [Finite ιn] [Finite ιo] {rn : ιn → Module.Dual K (α → ScrewSpace K k)} {ro : ιo → Module.Dual K (α → ScrewSpace K k)} {ρ : Module.Dual K (ScrewSpace K k)} (hrnvanish : ∀ (i : ιn) (S : α → ScrewSpace K k), S v = 0 → (rn i ∘ₗ ↑(columnOp hva)) S = 0) (hnewpinaug : LinearIndependent K (Sum.elim (fun (i : ιn) => (rn i ∘ₗ ↑(columnOp hva)) ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v) fun (x : Unit) => (hingeRow v a ρ ∘ₗ ↑(columnOp hva)) ∘ₗ LinearMap.single K (fun (x : α) => ScrewSpace K k) v)) (hbotrestrict : LinearIndependent K fun (j : ιo) => (ro j ∘ₗ ↑(columnOp hva)) ∘ₗ (LinearMap.id - LinearMap.single K (fun (x : α) => ScrewSpace K k) v ∘ₗ LinearMap.proj v)) : LinearIndependent K (Sum.elim (Sum.elim rn fun (x : Unit) => hingeRow v a ρ) ro)

The rows of va, the form hingeRow v a ρ and forms independent off v, through the column operation (a step of lem:case-III-candidate-row; KT eqs. (6.14)–(6.16) and (6.29), pp. 679 and 686): let Φ = columnOp hva. Suppose that the forms rn i ∘ₗ Φ vanish where S v = 0 (hrnvanish); that the restrictions of the forms rn i ∘ₗ Φ and (hingeRow v a ρ) ∘ₗ Φ to the screw assignments that vanish off v are linearly independent (hnewpinaug); and that the restrictions of the forms ro j ∘ₗ Φ to the other bodies are linearly independent (hbotrestrict). Then rn, hingeRow v a ρ and ro are jointly linearly independent.

The forms composed with Φ satisfy linearIndependent_sum_restriction_block, the form (hingeRow v a ρ) ∘ₗ Φ by hingeRow_comp_columnOp_vanish_off, and composing with Φ is an injective linear map of the forms.

Joint row independence at hinges with ends of their own (a star forest)

The rows of several hinges are jointly independent when each hinge has an end that no other hinge meets (linearIndependent_hingeRow_starForest, exists_independent_rigidityRows_of_starForest), the multi-body form of linearIndependent_hingeRow_star.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.linearIndependent_hingeRow_starForest {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {J : Type u_4} [Finite J] {I : J → Type u_5} [∀ (j : J), Finite (I j)] {u other : J → α} (hu : Function.Injective u) (hsep : ∀ (j j' : J), other j ≠ u j') {r : (j : J) → I j → Module.Dual K (ScrewSpace K k)} (hr : ∀ (j : J), LinearIndependent K (r j)) : LinearIndependent K fun (p : (j : J) × I j) => hingeRow (u p.fst) (other p.fst) (r p.fst p.snd)

The forms of hinges with ends of their own are jointly independent (lem:own-end-rows-independent, its claim for linear forms). Each hinge j : J runs from an end u j of its own to an other end other j: the u j are distinct (hu), and no other end is any hinge's own end (hsep : ∀ j j', other j ≠ u j'; in particular u j ≠ other j). The pairs (u j, other j) then form a star forest, a forest each of whose components is a star: each u j is a leaf whose one neighbour is other j. Not every forest is one: the edges of a path with three edges allow no such choice of ends. If for each j the forms r j : Iⱼ → Module.Dual K (ScrewSpace K k) are linearly independent, the forms ⟨j, i⟩ ↦ hingeRow (u j) (other j) (r j i) over Σ j, Iⱼ are linearly independent on α → ScrewSpace K k.

linearIndependent_hingeRow_star is the case of one star, u = w and other = const v. The proof evaluates a vanishing combination at the screw assignment Function.update 0 (u j₀) x: a hinge j ≠ j₀ reads 0 at both ends (u j ≠ u j₀ by hu, other j ≠ u j₀ by hsep) and the hinge j₀ reads x at u j₀ and 0 at other j₀, so ∑ i, c⟨j₀,i⟩ • (r j₀ i) x = 0 for every x, and every coefficient at j₀ vanishes, as the forms r j₀ are independent.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.exists_independent_rigidityRows_of_starForest {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) {J : Type u_4} [Finite J] {u other : J → α} {e : J → β} (hu : Function.Injective u) (hsep : ∀ (j j' : J), other j ≠ u j') (hlink : ∀ (j : J), F.graph.IsLink (e j) (u j) (other j)) (he : ∀ (j : J), F.supportExtensor (e j) ≠ 0) : ∃ (r : (_ : J) × Fin (screwDim k - 1) → Module.Dual K (α → ScrewSpace K k)), LinearIndependent K r ∧ ∀ (p : (_ : J) × Fin (screwDim k - 1)), r p ∈ F.rigidityRows

Edges with ends of their own give (D − 1)·|J| independent rigidity rows (lem:own-end-rows-independent, its form for rows). Let each edge e j link an end u j of its own to other j (hlink; hu and hsep as in linearIndependent_hingeRow_starForest, so the edges form a star forest), with F.supportExtensor (e j) ≠ 0 at each edge (he). Then there is a linearly independent family of members of F.rigidityRows indexed by Σ j, Fin (screwDim k − 1), of cardinality |J|·(D − 1) with D = screwDim k (Nat.card_sigma).

The D − 1 forms of each edge are a basis of its hinge-row block (finrank_hingeRowBlock, extracted by Submodule.exists_linearIndependent_fin_of_finrank_eq), and linearIndependent_hingeRow_starForest makes the rows of all the edges jointly independent; the link hlink j and the block membership witness each as a rigidity row.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.exists_independent_rigidityRows_of_isForest {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} [Finite β] (F : BodyHingeFramework K k α β) {T : Graph α β} (hT : T.IsForest) (hTF : T ≤ F.graph) (he : ∀ e ∈ T.edgeSet, F.supportExtensor e ≠ 0) : ∃ (r : (_ : ↑T.edgeSet) × Fin (screwDim k - 1) → Module.Dual K (α → ScrewSpace K k)), LinearIndependent K r ∧ ∀ (p : (_ : ↑T.edgeSet) × Fin (screwDim k - 1)), r p ∈ F.rigidityRows

The rows of a forest of nondegenerate hinges are independent (lem:forest-rows-independent). Let T ≤ F.graph be a forest (Graph.IsForest) with F.supportExtensor e ≠ 0 at each edge e of T, the edge labels being finite. Then there is a linearly independent family of members of F.rigidityRows indexed by Σ _ : T.edgeSet, Fin (screwDim k − 1), D − 1 rows per edge. Unlike exists_independent_rigidityRows_of_starForest, no edge needs an end of its own: a path with three edges is a forest.

The proof is by induction on the number of edges, for rows at the links of T itself. A forest with an edge has a pendant edge e at a body x (Graph.IsForest.exists_isPendant), and T less e is a forest (Graph.IsForest.anti) none of whose edges is at x. Its rows vanish on the screw assignments supported at x, where the D − 1 rows hingeRow x y (c i) of e, for a basis c of its hinge-row block (finrank_hingeRowBlock), read c; so linearIndependent_sum_pinned_block makes the two families jointly independent, and they are the rows of T reindexed.

Trivial motions, rigidity and the rank lemmas (KT §§2.3–2.4 and 5)

The trivial motions, of dimension D (lem:trivial-motions-rank-bound); infinitesimal rigidity, and rigidity on a set of bodies; KT Lemma 5.1 (finrank_pinnedMotions_add_screwDim, lem:rank-delete-vertex) and Lemma 5.3 (eq_of_hingeConstraint_two_parallel, lem:rank-parallel-full); and the comparison of two frameworks whose hinges have nested spans (lem:rank-rotation-semicont), which is not KT Lemma 5.2.

def CombinatorialRigidity.Molecular.BodyHingeFramework.IsTrivialMotion {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} (S : α → ScrewSpace K k) : Prop

A trivial screw assignment (def:trivial-motions-rigid; KT §2.3, p. 653): S u = S v for all bodies u and v. The trivial assignments are infinitesimal motions (isInfinitesimalMotion_of_isTrivialMotion), and they form a space of dimension D when there is a body (finrank_trivialMotions).

Equations

• CombinatorialRigidity.Molecular.BodyHingeFramework.IsTrivialMotion S = ∀ (u v : α), S u = S v

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.isInfinitesimalMotion_of_isTrivialMotion {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) {S : α → ScrewSpace K k} (hS : IsTrivialMotion S) : F.IsInfinitesimalMotion S

Every trivial motion is an infinitesimal motion (lem:trivial-motions-rank-bound): a constant screw assignment has S u - S v = 0, which lies in every hinge constraint's span, so it satisfies the hinge constraint at every edge.

def CombinatorialRigidity.Molecular.BodyHingeFramework.trivialMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (_F : BodyHingeFramework K k α β) : Submodule K (α → ScrewSpace K k)

The space of trivial motions (def:trivial-motions-rigid): the constant screw assignments, a subspace of α → ScrewSpace K k. Katoh and Tanigawa's D motions S*_i are a basis of it (KT p. 654); it is the image of the screw space under s ↦ (fun _ => s) (trivialMotions_eq_range_const), of dimension D when there is a body (finrank_trivialMotions).

The framework _F is an argument only so that F.trivialMotions reads as F.infinitesimalMotions does; the space does not depend on it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.mem_trivialMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (S : α → ScrewSpace K k) : S ∈ F.trivialMotions ↔ IsTrivialMotion S

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.trivialMotions_le_infinitesimalMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : F.trivialMotions ≤ F.infinitesimalMotions

The trivial motions are motions (a step of lem:trivial-motions-rank-bound): trivialMotions ≤ infinitesimalMotions, by isInfinitesimalMotion_of_isTrivialMotion.

def CombinatorialRigidity.Molecular.BodyHingeFramework.IsInfinitesimallyRigid {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : Prop

Infinitesimal rigidity (def:trivial-motions-rigid; KT §2.3, p. 653): every infinitesimal motion is trivial, Z(G,p) ≤ trivialMotions. It holds exactly when Z(G,p) is the space of trivial motions (infinitesimalMotions_eq_trivialMotions_iff), which has dimension D when there is a body (finrank_trivialMotions); that is, when rank R(G,p) = D(|V| − 1) (lem:trivial-motions-rank-bound).

Equations

• F.IsInfinitesimallyRigid = (F.infinitesimalMotions ≤ F.trivialMotions)

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.isInfinitesimallyRigid_iff {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : F.IsInfinitesimallyRigid ↔ ∀ (S : α → ScrewSpace K k), F.IsInfinitesimalMotion S → IsTrivialMotion S

def CombinatorialRigidity.Molecular.BodyHingeFramework.IsInfinitesimallyRigidOn {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (s : Set α) : Prop

Infinitesimal rigidity on a set s of bodies (the rank form of def:rank-hypothesis at deficiency zero): every infinitesimal motion is constant on s. All frameworks have the same bodies α, and a body of α that is not a vertex of G moves freely; on s = V(G) the condition is the rank D(|V(G)| − 1) (rem:rank-hypothesis-relative). On s = Set.univ it is infinitesimal rigidity (isInfinitesimallyRigidOn_univ_iff).

Equations

• F.IsInfinitesimallyRigidOn s = ∀ (S : α → CombinatorialRigidity.Molecular.ScrewSpace K k), F.IsInfinitesimalMotion S → ∀ u ∈ s, ∀ v ∈ s, S u = S v

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.isInfinitesimallyRigidOn_iff {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (s : Set α) : F.IsInfinitesimallyRigidOn s ↔ ∀ (S : α → ScrewSpace K k), F.IsInfinitesimalMotion S → ∀ u ∈ s, ∀ v ∈ s, S u = S v

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.IsInfinitesimallyRigidOn.mono {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) {s t : Set α} (hst : s ⊆ t) (h : F.IsInfinitesimallyRigidOn t) : F.IsInfinitesimallyRigidOn s

Rigidity on a set gives rigidity on its subsets (def:rank-hypothesis): a motion constant on t is constant on every s ⊆ t.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.isInfinitesimallyRigidOn_univ_iff {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : F.IsInfinitesimallyRigidOn Set.univ ↔ F.IsInfinitesimallyRigid

Rigidity on all of α is infinitesimal rigidity (def:rank-hypothesis): F.IsInfinitesimallyRigidOn Set.univ ↔ F.IsInfinitesimallyRigid.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.isInfinitesimallyRigidOn_union_of_inter {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) {s t : Set α} {c : α} (hcs : c ∈ s) (hct : c ∈ t) (hs : F.IsInfinitesimallyRigidOn s) (ht : F.IsInfinitesimallyRigidOn t) : F.IsInfinitesimallyRigidOn (s ∪ t)

Rigidity on two sets with a common body gives rigidity on their union (a step of lem:case-I-splice-seed): if every motion is constant on s and on t, and c ∈ s ∩ t, then every motion takes the value S c on s ∪ t. In Case I the vertex set of the rigid subgraph H and that of the contraction G/E(H) share the body to which H is contracted, and cover V(G).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.infinitesimalMotions_eq_trivialMotions_iff {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : F.infinitesimalMotions = F.trivialMotions ↔ F.IsInfinitesimallyRigid

Infinitesimal rigidity is the equality Z(G,p) = trivialMotions (lem:trivial-motions-rank-bound): the trivial motions are always motions (trivialMotions_le_infinitesimalMotions), so rigidity, the other inclusion, gives the equality.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.trivialMotions_eq_range_const {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) : F.trivialMotions = (LinearMap.pi fun (x : α) => LinearMap.id).range

The trivial motions are the constant assignments (a step of lem:trivial-motions-rank-bound): trivialMotions is the image of s ↦ (fun _ => s). With injective_const_pi it gives their dimension D (finrank_trivialMotions).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.injective_const_pi {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [Nonempty α] : Function.Injective ⇑(LinearMap.pi fun (x : α) => LinearMap.id)

The map s ↦ (fun _ => s) is injective when there is a body (a step of lem:trivial-motions-rank-bound): two constant assignments that agree agree at a body.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.finrank_trivialMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} [Nonempty α] (F : BodyHingeFramework K k α β) : Module.finrank K ↥F.trivialMotions = screwDim k

The trivial motions have dimension D (lem:trivial-motions-rank-bound; KT p. 654): when there is a body, finrank K F.trivialMotions = screwDim k. They are the image of the injective map s ↦ (fun _ => s) (trivialMotions_eq_range_const, injective_const_pi), which preserves dimension (LinearMap.finrank_range_of_inj), and the screw space has dimension D (screwSpace_finrank).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.finrank_screwAssignment {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} [Fintype α] : Module.finrank K (α → ScrewSpace K k) = screwDim k * Fintype.card α

The screw assignments have dimension D|V| (a step of lem:trivial-motions-rank-bound): finrank K (α → ScrewSpace K k) = screwDim k * Fintype.card α, the number of columns of R(G,p) (Module.finrank_pi_const, screwSpace_finrank). With finrank_trivialMotions it gives rank R(G,p) = D|V| − dim Z(G,p) ≤ D(|V| − 1).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.span_inf_span_eq_bot_of_linearIndependent {K : Type u_1} [Field K] {k : ℕ} {c₁ c₂ : ScrewSpace K k} (h : LinearIndependent K ![c₁, c₂]) : K ∙ c₁ ⊓ K ∙ c₂ = ⊥

The spans of two independent screws meet in 0 (lem:rank-parallel-full; the step of KT Lemma 5.3, p. 670): if c₁ and c₂ are linearly independent, then span {c₁} ⊓ span {c₂} = ⊥. Two hinges spanned by d − 1 of d + 1 affinely independent points, omitting different pairs, have independent extensors by KT Lemma 2.1 (omitTwoExtensor_linearIndependent).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.eq_of_hingeConstraint_two_parallel {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (S : α → ScrewSpace K k) {e₁ e₂ : β} {u v : α} (hgen : LinearIndependent K ![F.supportExtensor e₁, F.supportExtensor e₂]) (h₁ : F.hingeConstraint S e₁ u v) (h₂ : F.hingeConstraint S e₂ u v) : S u = S v

Two parallel edges with independent hinges fix the relative screw (lem:rank-parallel-full; KT Lemma 5.3, pp. 669–670): if the edges e₁ and e₂ join the bodies u and v, with linearly independent supporting extensors, then every screw assignment that satisfies both hinge constraints has S u = S v. The difference S u − S v lies in both spans (span_inf_span_eq_bot_of_linearIndependent). The graph with two bodies and two such edges is the base case of the algebraic induction (lem:theorem-55-base).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.eq_zero_of_mem_span_singleton_of_sum_eq_zero {K : Type u_1} [Field K] {k m : ℕ} {c d : Fin m → ScrewSpace K k} (hc : LinearIndependent K c) (hd : ∀ (i : Fin m), d i ∈ K ∙ c i) (hsum : ∑ i : Fin m, d i = 0) (i : Fin m) : d i = 0

Independent screws admit no vanishing sum of nonzero multiples (a step of lem:cycle-realization-rigid): if the screws c i are linearly independent, d i ∈ span {c i} for each i, and ∑ i, d i = 0, then every d i = 0. Write d i = a i • c i (Submodule.mem_span_singleton); then every a i = 0 (Fintype.linearIndependent_iff). It is the step behind the cycles of KT Lemma 5.4 (p. 670): around a cycle of bodies vᵢ whose supporting extensors are independent, the differences d i = S(vᵢ) − S(vᵢ₊₁) of a motion satisfy these hypotheses, so the motion is constant on the cycle. The case of two screws is span_inf_span_eq_bot_of_linearIndependent.

def CombinatorialRigidity.Molecular.BodyHingeFramework.pinnedMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (v : α) : Submodule K (α → ScrewSpace K k)

The motions that vanish at a body v (the space pinned(v) of lem:rank-delete-vertex): the infinitesimal motions S with S v = 0. Deleting the D columns of v from R(G,p) leaves the matrix whose null space consists of their restrictions to the other bodies.

Equations

• F.pinnedMotions v = { carrier := {S : α → CombinatorialRigidity.Molecular.ScrewSpace K k | F.IsInfinitesimalMotion S ∧ S v = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.mem_pinnedMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (v : α) (S : α → ScrewSpace K k) : S ∈ F.pinnedMotions v ↔ F.IsInfinitesimalMotion S ∧ S v = 0

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.isInfinitesimalMotion_sub_const {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) {S : α → ScrewSpace K k} (hS : F.IsInfinitesimalMotion S) (c : ScrewSpace K k) : F.IsInfinitesimalMotion fun (u : α) => S u - c

A motion minus a constant assignment is a motion (a step of lem:rank-delete-vertex): the hinge constraints read only the differences S u − S w, which subtracting c from every value does not change.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.trivialMotions_inf_pinnedMotions_eq_bot {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (v : α) : F.trivialMotions ⊓ F.pinnedMotions v = ⊥

The trivial motions and the motions that vanish at v meet in 0 (lem:rank-delete-vertex): a constant assignment with value 0 at v is zero. With trivialMotions_sup_pinnedMotions it makes Z(G,p) their direct sum.

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.trivialMotions_sup_pinnedMotions {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F : BodyHingeFramework K k α β) (v : α) : F.trivialMotions ⊔ F.pinnedMotions v = F.infinitesimalMotions

Every motion is a trivial motion plus one that vanishes at v (lem:rank-delete-vertex): trivialMotions ⊔ pinnedMotions v = infinitesimalMotions. A motion S is the constant assignment with value S v plus u ↦ S u − S v, which vanishes at v and is a motion (isInfinitesimalMotion_sub_const).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.finrank_pinnedMotions_add_screwDim {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} [Nonempty α] [Finite α] (F : BodyHingeFramework K k α β) (v : α) : Module.finrank K ↥(F.pinnedMotions v) + screwDim k = Module.finrank K ↥F.infinitesimalMotions

Deleting the columns of one body keeps the rank (lem:rank-delete-vertex; KT Lemma 5.1, pp. 667–668): for finitely many bodies, at least one,

finrank (pinnedMotions v) + D = finrank Z(G,p),

as Z(G,p) is the direct sum of the trivial motions, of dimension D, and the motions that vanish at v (trivialMotions_inf_pinnedMotions_eq_bot, trivialMotions_sup_pinnedMotions). Equivalently, deleting the D columns of v from R(G,p) does not change its rank. Katoh and Tanigawa cite White and Whiteley (1987, §2) for the fact that fixing a body does not change the space of nontrivial motions (KT p. 668).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.infinitesimalMotions_mono_of_span_le {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} (F F' : BodyHingeFramework K k α β) (hgraph : F.graph = F'.graph) (hspan : ∀ (e : β), K ∙ F'.supportExtensor e ≤ K ∙ F.supportExtensor e) : F'.infinitesimalMotions ≤ F.infinitesimalMotions

Smaller hinge spans give fewer motions (lem:rank-rotation-semicont): if F and F' have the same multigraph and span C'(e) ≤ span C(e) at every edge label e, where C and C' are the supporting extensors of F and F', then every motion of F' is one of F. At a link e from u to v, S u − S v ∈ span C'(e) ≤ span C(e). When all the extensors are nonzero, the hypothesis says that the spans are equal; the inclusion can be strict at an edge with C'(e) = 0 ≠ C(e). It is not KT Lemma 5.2, which rotates a panel without lowering the rank (KT p. 669).

theorem CombinatorialRigidity.Molecular.BodyHingeFramework.finrank_infinitesimalMotions_le_of_span_le {K : Type u_1} [Field K] {k : ℕ} {α : Type u_2} {β : Type u_3} [Finite α] (F F' : BodyHingeFramework K k α β) (hgraph : F.graph = F'.graph) (hspan : ∀ (e : β), K ∙ F'.supportExtensor e ≤ K ∙ F.supportExtensor e) : Module.finrank K ↥F'.infinitesimalMotions ≤ Module.finrank K ↥F.infinitesimalMotions

Smaller hinge spans give a motion space of no larger dimension (lem:rank-rotation-semicont): for finitely many bodies and F, F' as in infinitesimalMotions_mono_of_span_le, finrank Z(G,p') ≤ finrank Z(G,p), so rank R(G,p) ≤ rank R(G,p'), the rank being D|V| − finrank Z (finrank_screwAssignment). Submodule.finrank_mono on infinitesimalMotions_mono_of_span_le.