The base case of the pencil reduction

The base case of the induction of sec:pencil-reduction (lem:pencil-base-case): every loopless multigraph on one or two bodies has a pencil realization at the deficiency rank. Every body gets the same normal and the same point of its panel, and the edges get two independent hinges in that panel through that point (lem:extensor-pair-through-point). The loop and cut-edge cases are in Arms.lean.

Main results

• hasPencilRealization_of_ncard_le_two: the base case (lem:pencil-base-case).

The base case

theorem CombinatorialRigidity.Molecular.hasPencilRealization_of_ncard_le_two {K : Type u_1} [Field K] {α : Type u_2} {β : Type u_3} [Finite α] [Finite β] {G : Graph α β} (hloop : G.Loopless) (hne : G.vertexSet.Nonempty) (hV2 : G.vertexSet.ncard ≤ 2) : HasPencilRealization K 3 G

The base case (lem:pencil-base-case): every loopless multigraph G on one or two bodies has a pencil realization at the deficiency rank, at n = 3, where Graph.bodyBarDim 3 = screwDim 2 = 6. Every body gets the normal n₀ = Pi.single 0 1 and the point q₀ of exists_linearIndependent_extensor_pair_through_point (lem:extensor-pair-through-point), which also gives two independent hinges Ce and Cf in that panel through q₀. By the edges:

• No edge (one body or two): the deficiency is D(|V(G)| - 1) (Graph.deficiency_of_edgeSet_empty), so the deficiency rank is 0; every label gets Ce.
• One edge e: the deficiency is 1 (Graph.deficiency_of_single_edge), and e gets Ce. The rank is at least D - 1, as the nonzero hinge of an edge gives D - 1 independent rows (BodyHingeFramework.exists_independent_rigidityRows_of_edge, lem:edge-rows-independent), and at most the deficiency rank (BodyHingeFramework.finrank_span_rigidityRows_add_deficiency_le, lem:relative-deficiency-rank-bound).
• Two edges or more, all joining the two bodies, as G is loopless: the deficiency is 0, as that of two of the edges e ≠ f is (Graph.isKDof_zero_of_parallel_pair, on G ↾ {e, f}) and adding edges on the same bodies does not raise it (Graph.deficiency_le_deficiency_of_le_vertexSet_eq). The edge e gets Ce and every other label Cf. The independent hinges at e and f make the two bodies rigid (BodyHingeFramework.theorem_55_base, lem:theorem-55-base), so the rank is D (BodyHingeFramework.isInfinitesimallyRigidOn_vertexSet_iff_finrank_span_rigidityRows).