Body-hinge Tay–Whiteley theorem — edge multiplication and body-hinge frameworks

The body-hinge Tay–Whiteley theorem in n-space (Tay 1989, §7; Whiteley 1988, Theorem 10) reduces to the body-bar Tay theorem through Whiteley's device (1988, proof of Theorem 10, p. 244): a hinge leaves its two bodies one relative degree of freedom, so it acts as a bundle of δ - 1 bars, δ = bodyBarDim n. Combinatorially this is parallel-edge multiplication of the underlying multigraph — the (δ-1) · G, written G̃, of Katoh and Tanigawa (2011, §1).

The file holds the four nodes of body-hinge.tex:

• def:edge-multiply — the multiplied multigraph m · G on the carrier Graph α β (mathlib core), and the facts about it below.
• def:body-hinge-framework — the body-hinge framework Graph.BodyHingeFramework as a thin wrapper over the induced Graph.BodyBarFramework on (δ-1)·G (toBodyBar), with independence and infinitesimal rigidity read off it.
• lem:edge-multiply-sparse — edgeMultiply_isSparse_iff, the body-hinge ⇔ body-bar existential transport (exists_toBodyBar_iff) composed with the body-bar Tay theorem (tay_witness) on (δ-1)·G.
• thm:body-hinge-tay — body_hinge_tay: edgeMultiply_isSparse_iff with (δ-1)·G's sparsity read as a forest packing (tutte_nash_williams on (δ-1)·G).

m · G (def:edge-multiply)

For m : ℕ, G.edgeMultiply m : Graph α (β × Fin m) keeps the vertex set of G and replaces each edge e by the m parallel copies (e, 0), …, (e, m-1), each linking the same endpoints as e. The edge type is β × Fin m; the incidence (m · G).IsLink (e, i) x y holds exactly when G.IsLink e x y. The facts about it:

• vertexSet_edgeMultiply — V(m · G) = V(G) (definitionally).
• edgeMultiply_edgeSet_ncard — |E(m · G)| = m · |E(G)|.
• spanningVerts_edgeMultiply — a bar set E' in G spans the same vertices as its preimage (· .1 ∈ E') in m · G, for m ≠ 0.
• edgeMultiply_inc and edgeMultiply_mono — incidence, and monotonicity in the subgraph order.

Phrased Set-side throughout (Set.ncard, [Finite]) to line up with the Graph.IsSparse predicate (def:graph-sparse). The blueprint presents the file in sec:body-hinge.

def Graph.edgeMultiply {α : Type u_1} {β : Type u_2} (G : Graph α β) (m : ℕ) : Graph α (β × Fin m)

Parallel-edge multiplication m · G (def:edge-multiply): the multigraph on the same vertex set as G : Graph α β in which each edge e is replaced by m parallel copies indexed by Fin m. The edge type is β × Fin m, and (m · G).IsLink (e, i) x y holds exactly when G.IsLink e x y. The hinge-to-bar reduction of the body-hinge Tay–Whiteley theorem takes m = bodyBarDim n - 1 (bodyHingeMult n).

Equations

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

@[simp]

theorem Graph.vertexSet_edgeMultiply {α : Type u_1} {β : Type u_2} (G : Graph α β) (m : ℕ) : (G.edgeMultiply m).vertexSet = G.vertexSet

@[simp]

theorem Graph.edgeMultiply_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) (m : ℕ) (p : β × Fin m) (x y : α) : (G.edgeMultiply m).IsLink p x y = G.IsLink p.1 x y

@[simp]

theorem Graph.edgeMultiply_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (m : ℕ) : (G.edgeMultiply m).edgeSet = {p : β × Fin m | p.1 ∈ G.edgeSet}

theorem Graph.edgeMultiply_inc {α : Type u_1} {β : Type u_2} (G : Graph α β) (m : ℕ) {p : β × Fin m} {x : α} : (G.edgeMultiply m).Inc p x ↔ G.Inc p.1 x

theorem Graph.edgeMultiply_edgeSet_ncard {α : Type u_1} {β : Type u_2} (G : Graph α β) (m : ℕ) : (G.edgeMultiply m).edgeSet.ncard = m * G.edgeSet.ncard

|E(m · G)| = m · |E(G)| (def:edge-multiply): each of the |E(G)| edges of G is replaced by m parallel copies.

@[simp]

theorem Graph.spanningVerts_edgeMultiply {α : Type u_1} {β : Type u_2} (G : Graph α β) (m : ℕ) [NeZero m] (E' : Set β) : (G.edgeMultiply m).spanningVerts {p : β × Fin m | p.1 ∈ E'} = G.spanningVerts E'

A bar set E' in G spans the same vertices as its preimage under the first projection in m · G (def:edge-multiply): spanningVerts transports across edge multiplication. Requires m ≠ 0 so each G-edge has at least one parallel copy (for m = 0 the multiplied graph is edgeless); m = bodyBarDim n - 1 is at least 2 for n ≥ 2.

theorem Graph.edgeMultiply_mono {α : Type u_1} {β : Type u_2} {H G : Graph α β} (h : H ≤ G) (m : ℕ) : H.edgeMultiply m ≤ G.edgeMultiply m

Edge multiplication is monotone in the subgraph order: H ≤ G implies m · H ≤ m · G. Each parallel copy of a link of H is the corresponding copy of the same link of G, and the vertex sets are inherited verbatim.

Body-hinge frameworks (def:body-hinge-framework)

A body-hinge framework in ℝⁿ on a multigraph G : Graph α β (def:body-hinge-framework) joins bodies by hinges, (n-2)-dimensional affine subspaces (Whiteley 1988, §3.3). A hinge constrains all but one of the δ relative screw freedoms of the two bodies it joins, δ = bodyBarDim n, so it behaves like a bundle of δ - 1 bars meeting the hinge whose Plücker vectors are linearly independent (Whiteley 1988, proof of Theorem 10, p. 244). Combinatorially this is the parallel-edge multiplication (δ-1)·G (edgeMultiply above).

The formalization records a body-hinge framework by the vectors of these bars alone: it is a body-bar framework on (δ-1)·G, with no hinge and no condition on the δ - 1 vectors of an edge (they need not span a hinge's space, nor be independent). Independence and infinitesimal rigidity are those of this body-bar framework (BodyBar/Framework.lean).

def Graph.bodyHingeMult (n : ℕ) : ℕ

The edge-multiplication factor of the body-hinge reduction: δ - 1, where δ = bodyBarDim n. A hinge constrains all but one of a body's δ relative screw freedoms, so each hinge becomes bodyHingeMult n bars. For n ≥ 2 this is ≥ 2 (δ ≥ 3); the lemmas that need a copy of every edge assume [NeZero (bodyHingeMult n)].

Equations

• Graph.bodyHingeMult n = Graph.bodyBarDim n - 1

structure Graph.BodyHingeFramework (n : ℕ) (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

A body-hinge framework in ℝⁿ on a multigraph G : Graph α β (def:body-hinge-framework; Whiteley 1988, §3.3). The combinatorial data is the multigraph G; the geometric data is a placement assigning each of the δ - 1 parallel bars of every hinge a vector of ℝᵈ, d = bodyBarDim n. In the source a hinge's δ - 1 vectors are a basis of the span of the Plücker vectors of the lines meeting the hinge; here they are arbitrary, and no hinge is recorded.

The placement is typed as a placement on the multiplied multigraph (δ-1)·G (graph.edgeMultiply (bodyHingeMult n), edge type β × Fin (δ-1)); the induced body-bar framework toBodyBar is then literally the Graph.BodyBarFramework on (δ-1)·G carrying that placement, and all rigidity notions are inherited from it.

• graph : Graph α β

  The underlying multigraph: bodies are vertices, hinges are edges.

• placement : ↑(self.graph.edgeMultiply (bodyHingeMult n)).edgeSet → EuclideanSpace ℝ (Fin (bodyBarDim n))

  The placement: each of the δ - 1 parallel bars of every hinge gets a vector of ℝᵈ, d = bodyBarDim n. Equivalently a placement on the multiplied multigraph (δ-1)·G; the vectors are unconstrained.

def Graph.BodyHingeFramework.toBodyBar {n : ℕ} {α : Type u_3} {β : Type u_4} (F : BodyHingeFramework n α β) : BodyBarFramework n α (β × Fin (bodyHingeMult n))

The induced body-bar framework of a body-hinge framework on (δ-1)·G (def:body-hinge-framework): the Graph.BodyBarFramework on the multiplied multigraph (δ-1)·G carrying F's per-bar placement. Its rigidity map (Graph.BodyBarFramework.rigidityMap) is the body-hinge framework's, and IsIndependent and IsInfinitesimallyRigid below are read off it.

Equations

• F.toBodyBar = { graph := F.graph.edgeMultiply (Graph.bodyHingeMult n), placement := F.placement }

@[simp]

theorem Graph.BodyHingeFramework.toBodyBar_graph {n : ℕ} {α : Type u_3} {β : Type u_4} (F : BodyHingeFramework n α β) : F.toBodyBar.graph = F.graph.edgeMultiply (bodyHingeMult n)

@[simp]

theorem Graph.BodyHingeFramework.toBodyBar_placement {n : ℕ} {α : Type u_3} {β : Type u_4} (F : BodyHingeFramework n α β) : F.toBodyBar.placement = F.placement

def Graph.BodyHingeFramework.IsIndependent {n : ℕ} {α : Type u_3} {β : Type u_4} (F : BodyHingeFramework n α β) (D : (F.graph.edgeMultiply (bodyHingeMult n)).orientation) : Prop

A body-hinge framework F is independent at an orientation D of (δ-1)·G (def:body-hinge-framework's independence) when its induced body-bar framework is: the rows of all the bars of (δ-1)·G are linearly independent. Inherited verbatim from Graph.BodyBarFramework.IsIndependent.

Equations

• F.IsIndependent D = F.toBodyBar.IsIndependent D

def Graph.BodyHingeFramework.IsInfinitesimallyRigid {n : ℕ} {α : Type u_3} {β : Type u_4} [Finite α] (F : BodyHingeFramework n α β) (D : (F.graph.edgeMultiply (bodyHingeMult n)).orientation) : Prop

A body-hinge framework F is infinitesimally rigid at an orientation D of (δ-1)·G (def:body-hinge-framework's infinitesimal rigidity) when its induced body-bar framework is: rank + δ = δ·b for δ = bodyBarDim n and b the number of bodies. Inherited verbatim from Graph.BodyBarFramework.IsInfinitesimallyRigid; [Finite α] is the same semantic contract guard as there (finite body set).

Equations

• F.IsInfinitesimallyRigid D = F.toBodyBar.IsInfinitesimallyRigid D

theorem Graph.BodyHingeFramework.exists_toBodyBar_iff {n : ℕ} {α : Type u_3} {β : Type u_4} (G : Graph α β) (P : BodyBarFramework n α (β × Fin (bodyHingeMult n)) → Prop) : (∃ (F : BodyHingeFramework n α β), F.graph = G ∧ P F.toBodyBar) ↔ ∃ (Fb : BodyBarFramework n α (β × Fin (bodyHingeMult n))), Fb.graph = G.edgeMultiply (bodyHingeMult n) ∧ P Fb

A body-bar framework on the multiplied multigraph (δ-1)·G arises from a body-hinge framework on G: a property P holds at toBodyBar of some body-hinge framework on G iff it holds at some body-bar framework on (δ-1)·G (the placement passes through unchanged). This is the existential transport of lem:edge-multiply-sparse's proof: the body-hinge frameworks on G and the body-bar frameworks on (δ-1)·G are the same data.

theorem Graph.BodyHingeFramework.edgeMultiply_isSparse_iff {n : ℕ} {α : Type u_3} {β : Type u_4} [Finite α] [Finite β] (G : Graph α β) : ((∃ (F : BodyHingeFramework n α β) (_ : F.graph = G) (D : (F.graph.edgeMultiply (bodyHingeMult n)).orientation), F.IsIndependent D) ↔ (G.edgeMultiply (bodyHingeMult n)).IsSparse (bodyBarDim n) (bodyBarDim n)) ∧ ((∃ (F : BodyHingeFramework n α β) (_ : F.graph = G) (D : (F.graph.edgeMultiply (bodyHingeMult n)).orientation), F.IsIndependent D ∧ F.IsInfinitesimallyRigid D) ↔ (G.edgeMultiply (bodyHingeMult n)).IsTight (bodyBarDim n) (bodyBarDim n))

Tay's theorem for the multiplied multigraph (lem:edge-multiply-sparse; the reduction of Whiteley 1988, proof of Theorem 10). For δ = bodyBarDim n, a multigraph G carries an independent body-hinge framework in ℝⁿ iff (δ-1)·G is (δ,δ)-sparse, and an isostatic one iff (δ-1)·G is (δ,δ)-tight. The proof is the body-bar Tay theorem (tay_witness) applied to the multiplied multigraph (δ-1)·G, transported across the body-hinge ⇔ body-bar existential bijection (exists_toBodyBar_iff): a body-hinge framework on G is a body-bar framework on (δ-1)·G, so independence and isostaticity read off node-for-node.

The count of def:edge-multiply makes the tightness concrete: |E((δ-1)·G)| = (δ-1)|E(G)| (edgeMultiply_edgeSet_ncard), so (δ,δ)-tightness of (δ-1)·G reads (δ-1)|E(G)| + δ = δ·|V(G)|, i.e. (δ-1)|E(G)| = δ(|V(G)|-1).

theorem Graph.BodyHingeFramework.body_hinge_tay {n : ℕ} {α : Type u_3} {β : Type u_4} [Finite α] [Finite β] (G : Graph α β) : ((∃ (F : BodyHingeFramework n α β) (_ : F.graph = G) (D : (F.graph.edgeMultiply (bodyHingeMult n)).orientation), F.IsIndependent D) ↔ (G.edgeMultiply (bodyHingeMult n)).IsForestPacking (bodyBarDim n)) ∧ ((∃ (F : BodyHingeFramework n α β) (_ : F.graph = G) (D : (F.graph.edgeMultiply (bodyHingeMult n)).orientation), F.IsIndependent D ∧ F.IsInfinitesimallyRigid D) ↔ (G.edgeMultiply (bodyHingeMult n)).IsTight (bodyBarDim n) (bodyBarDim n))

Body-hinge Tay–Whiteley theorem (thm:body-hinge-tay; Tay 1989, §7, and Whiteley 1988, Theorem 10). For δ = bodyBarDim n = n(n+1)/2, a multigraph G carries an independent body-hinge framework in ℝⁿ iff E((δ-1)·G) is the edge-disjoint union of δ forests (Graph.IsForestPacking), and an isostatic one iff (δ-1)·G is (δ,δ)-tight. As the definition records a body-hinge framework by its bars alone, the frameworks need not come from hinges.

The sparse/tight characterizations are edgeMultiply_isSparse_iff (the body-hinge ⇔ body-bar reduction composed with the body-bar Tay theorem tay_witness on (δ-1)·G); the forest-packing reformulation is tutte_nash_williams applied to (δ-1)·G. When (δ-1)·G is connected, the tight case is a packing of δ spanning trees by isSpanningTreePacking_of_isTight applied to (δ-1)·G.