2.3. From a rigid graph to a rigid twist system
The cross-block compatibility constraints of a grounded block assignment,
grouped by unordered block pair. Twist rigidity makes it injective, so its rank
is at least 6(t-1); the rank of a product of linear maps is at most the sum
of the coordinate ranks, so it is at most the partition capacity.
Lean code for Lemma2.3.1●3 declarations
Associated Lean declarations
-
defdefined in RB31EndToEnd/Rigidity/TwistNecessity.leancomplete
def RB31E2E.BodyPinIncidence.groupedGroundedBlockOperator (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) (p : H.Pin → RB31E2E.Vec3 ℝ) (root : Fin t) : (RB31E2E.OffRoot root → RB31E2E.Twist ℝ) →ₗ[ℝ] (b : ↥(RB31E2E.BodyPinIncidence.PartitionEdge t)) → ↥(H.PartitionBundlePin π b) → RB31E2E.Vec3 ℝ
def RB31E2E.BodyPinIncidence.groupedGroundedBlockOperator (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) (p : H.Pin → RB31E2E.Vec3 ℝ) (root : Fin t) : (RB31E2E.OffRoot root → RB31E2E.Twist ℝ) →ₗ[ℝ] (b : ↥(RB31E2E.BodyPinIncidence.PartitionEdge t)) → ↥(H.PartitionBundlePin π b) → RB31E2E.Vec3 ℝ
All crossing constraints of a grounded block assignment, grouped by their unordered block bundle. Internal pins are omitted because a block-constant twist makes their relative twist identically zero.
-
theoremdefined in RB31EndToEnd/Rigidity/TwistNecessity.leancomplete
theorem RB31E2E.BodyPinIncidence.six_mul_pred_le_groupedGroundedBlockOperator_rank (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) (hπ : Function.Surjective π) (p : H.Pin → RB31E2E.Vec3 ℝ) (hRigid : RB31E2E.TwistRigidAt H.left H.right p) (root : Fin t) : 6 * (t - 1) ≤ Module.finrank ℝ ↥(H.groupedGroundedBlockOperator π p root).range
theorem RB31E2E.BodyPinIncidence.six_mul_pred_le_groupedGroundedBlockOperator_rank (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) (hπ : Function.Surjective π) (p : H.Pin → RB31E2E.Vec3 ℝ) (hRigid : RB31E2E.TwistRigidAt H.left H.right p) (root : Fin t) : 6 * (t - 1) ≤ Module.finrank ℝ ↥(H.groupedGroundedBlockOperator π p root).range
The grouped grounded operator has at least the full dimension of the grounded block-twist space.
-
theoremdefined in RB31EndToEnd/Rigidity/TwistNecessity.leancomplete
theorem RB31E2E.BodyPinIncidence.groupedGroundedBlockOperator_rank_le_partitionCapacity (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) (p : H.Pin → RB31E2E.Vec3 ℝ) (root : Fin t) : Module.finrank ℝ ↥(H.groupedGroundedBlockOperator π p root).range ≤ H.partitionCapacity π
theorem RB31E2E.BodyPinIncidence.groupedGroundedBlockOperator_rank_le_partitionCapacity (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) (p : H.Pin → RB31E2E.Vec3 ℝ) (root : Fin t) : Module.finrank ℝ ↥(H.groupedGroundedBlockOperator π p root).range ≤ H.partitionCapacity π
The grouped operator's rank is at most the sum of the proved capacities of its unordered bundles.
/-- All crossing constraints of a grounded block assignment, grouped by
their unordered block bundle. Internal pins are omitted because a
block-constant twist makes their relative twist identically zero. -/
noncomputable def groupedGroundedBlockOperator (H : BodyPinIncidence)
{t : ℕ} (π : H.Body → Fin t) (p : H.Pin → Vec3 ℝ) (root : Fin t) :
(OffRoot root → Twist ℝ) →ₗ[ℝ]
((b : PartitionEdge t) → H.PartitionBundlePin π b → Vec3 ℝ) :=
LinearMap.pi fun b ↦
(H.blockBundleOperator π p b).comp (extendGroundedLinear root)
The grounding is visible in the quoted body:
extendGroundedLinear extends an
assignment by giving the root block the zero twist, so the source of the
operator is indexed by OffRoot, one twist per block
except the chosen one. Working on this subspace replaces the paper's quotient
by the diagonal.
The grouping introduces a sign that the paper's paragraph does not mention. The
constraints of a bundle are all expressed through a single relative twist, the
one belonging to the bundle's chosen orientation, and each pin occurrence
carries a sign recording whether its own orientation agrees. Signed and
unsigned evaluations have the same kernel, so the 3, 5, 6 bounds apply to the
signed form unchanged.
A placement attaining the maximum rigidity rank can be chosen so that every body's four private core vertices are affinely independent; at such a placement, equality with the complete-graph rank forces the twist system itself to be rigid.
Lean code for Lemma2.3.2●3 declarations
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Rigidity/GraphNecessity.leancomplete
theorem RB31E2E.BarJoint.isOpen_setOf_le_rigidityRank {V : Type} [Fintype V] {d : ℕ} (G : SimpleGraph V) (r : ℕ) : IsOpen {p | r ≤ RB31E2E.BarJoint.rigidityRank G p}
theorem RB31E2E.BarJoint.isOpen_setOf_le_rigidityRank {V : Type} [Fintype V] {d : ℕ} (G : SimpleGraph V) (r : ℕ) : IsOpen {p | r ≤ RB31E2E.BarJoint.rigidityRank G p}
A fixed lower bound on rigidity rank is an open condition on placements.
-
theoremdefined in RB31EndToEnd/Rigidity/GraphNecessity.leancomplete
theorem RB31E2E.BodyPinIncidence.exists_allCores_rigidityRank_eq_genericRigidityRank (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) : ∃ p, H.AllCoresAffinelyIndependent extra p ∧ RB31E2E.BarJoint.rigidityRank (H.bodyPinGraph extra) p = RB31E2E.BarJoint.genericRigidityRank (H.bodyPinGraph extra) 3
theorem RB31E2E.BodyPinIncidence.exists_allCores_rigidityRank_eq_genericRigidityRank (H : RB31E2E.BodyPinIncidence) (extra : H.Body → ℕ) : ∃ p, H.AllCoresAffinelyIndependent extra p ∧ RB31E2E.BarJoint.rigidityRank (H.bodyPinGraph extra) p = RB31E2E.BarJoint.genericRigidityRank (H.bodyPinGraph extra) 3
The maximum rigidity rank is attained at a placement whose canonical private cores are all affine-independent. This is the reusable generic-open perturbation bridge needed to descend from graph motions to body twists.
-
defdefined in RB31EndToEnd/Rigidity/GraphNecessity.leancomplete
def RB31E2E.BodyPinIncidence.coreLineDetPolynomial {V : Type} (p q : RB31E2E.BarJoint.Placement V 3) (f : Fin 4 → V) : Polynomial ℝ
def RB31E2E.BodyPinIncidence.coreLineDetPolynomial {V : Type} (p q : RB31E2E.BarJoint.Placement V 3) (f : Fin 4 → V) : Polynomial ℝ
The determinant polynomial detecting degeneracy of one core.
The paper's necessity argument begins with a generic realization, and genericity gives at one stroke every property the argument needs. The formalization has no genericity theory, by the design decision recorded on the maximum-rank definition, so a placement with the two properties actually used — maximum rigidity rank, and affine independence of the core of every body, i.e. of its four designated private vertices — is constructed by a one-parameter avoidance argument.
A lower bound on the rigidity rank is an open condition on placements, because
the rigidity operator depends continuously and linearly on the coordinates.
Take a placement p attaining the maximum rank and the standard placement
q in which every body's core is the tetrahedron 0, e_1, e_2, e_3, and
consider the segment from p to q. Degeneracy of one body's core along
the segment is the vanishing of an explicit univariate determinant polynomial,
which is nonzero as a polynomial because its value at the parameter of q is
nonzero. Finitely many finite root sets cannot cover an interval, so some
placement near p attains the maximum rank and has every core affinely
independent.
/-- The determinant polynomial detecting degeneracy of one core. -/
noncomputable def coreLineDetPolynomial {V : Type}
(p q : BarJoint.Placement V 3) (f : Fin 4 → V) : Polynomial ℝ :=
(coreLinePolynomialMatrix p q f).det
The polynomial is the determinant of
coreLinePolynomialMatrix,
whose three columns are the displacements of a body's other three core vertices
from the first, each interpolated linearly along the segment. Its value at a
parameter is therefore the determinant of the displacement matrix at that
placement, which is nonzero exactly when the four points are affinely
independent, and the avoidance argument concerns the roots of one univariate
real polynomial per body.
At the placement so constructed, the graph rank equals the complete-graph rank, so the two infinitesimal-motion kernels agree; a complete framework containing one nondegenerate tetrahedron admits only the global Euclidean motions; hence every twist motion is diagonal, and the twist system is rigid at the pin coordinates. The empty-body case is separate and immediate: every twist assignment on an empty type is diagonal.