Body-Pin Rigidity

7.3. The componentwise Witt shear🔗

The height computation needs pairwise distinct three-dimensional coordinates, because the grounded inequality (4.7) applies to configurations in K^3, while on a component of V(I_F) only the six-dimensional twists are pairwise distinct: the translational parts b_v may coincide. The shear repairs this without moving the ideal.

Lemma7.3.1
Group: The paper's algebraic argument: the form, the ideal, the shear, the dimension formula, and the height theorem. (5)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the Blueprint HTML cache.
uses 1used by 1✓L∃∀N
Tagspaper

Let Z \subseteq V(I_F) be an irreducible component meeting U_{\mathrm{dist}}. There is a constant skew-symmetric matrix S_Z \in \mathfrak{so}_3(k) such that a_v := b_v + S_Z \omega_v satisfies a_u - a_v \ne 0 in k(Z) for every u \ne v, and the linear automorphism \Phi_{S_Z} : (\omega, b) \mapsto (\omega, b + S_Z \omega) fixes every generator of I_F. (Zheng, 2026, Lemma 5.1)

Lean code for Lemma7.3.1●3 declarations
  • defdefined in RB31EndToEnd/NullCellule/WittShear.lean
    complete
    def RB31E2E.WittShear.shear.{u_1} {k : Type u_1} [CommRing k]
  (s : RB31E2E.Vec3 k) (X : RB31E2E.Twist k) : RB31E2E.Twist k
    def RB31E2E.WittShear.shear.{u_1}
  {k : Type u_1} [CommRing k]
  (s : RB31E2E.Vec3 k)
  (X : RB31E2E.Twist k) : RB31E2E.Twist k
    The angular-fixing skew Witt shear with parameter `s`.
  • theoremdefined in RB31EndToEnd/NullCellule/WittShear.lean
    complete
    theorem RB31E2E.WittShear.splitKlein_shear.{u_1} {k : Type u_1} [CommRing k]
  (s : RB31E2E.Vec3 k) (X : RB31E2E.Twist k) :
  (RB31E2E.WittShear.shear s X).splitKlein = X.splitKlein
    theorem RB31E2E.WittShear.splitKlein_shear.{u_1}
  {k : Type u_1} [CommRing k]
  (s : RB31E2E.Vec3 k)
  (X : RB31E2E.Twist k) :
  (RB31E2E.WittShear.shear s
        X).splitKlein =
    X.splitKlein
    A skew Witt shear preserves the Split--Klein quadratic form literally.
  • theoremdefined in RB31EndToEnd/NullCellule/WittShear.lean
    complete
    theorem RB31E2E.WittShear.exists_common_base_shear_snd_ne_zero.{u_1, u_2, u_3}
  {k : Type u_1} {K : Type u_2} {I : Type u_3} [Field k] [Infinite k]
  [Field K] [Algebra k K] [Fintype I] (Z : I → RB31E2E.Twist K)
  (hZ : ∀ (i : I), Z i ≠ 0) :
  ∃ s,
    ∀ (i : I),
      (RB31E2E.WittShear.shear (fun j ↦ (algebraMap k K) (s j))
            (Z i)).2 ≠
        0
    theorem RB31E2E.WittShear.exists_common_base_shear_snd_ne_zero.{u_1,
    u_2, u_3}
  {k : Type u_1} {K : Type u_2}
  {I : Type u_3} [Field k] [Infinite k]
  [Field K] [Algebra k K] [Fintype I]
  (Z : I → RB31E2E.Twist K)
  (hZ : ∀ (i : I), Z i ≠ 0) :
  ∃ s,
    ∀ (i : I),
      (RB31E2E.WittShear.shear
            (fun j ↦
              (algebraMap k K) (s j))
            (Z i)).2 ≠
        0
    A finite family of nonzero twists over an extension field admits one
common shear whose parameter lies in the infinite base field and whose
translational half is nonzero for every member.
Proof for Lemma 7.3.1
uses 0

The intersection Z \cap U_{\mathrm{dist}} is dense in Z, so every difference vector (\omega_u - \omega_v, b_u - b_v) is nonzero in k(Z)^6. For a fixed pair u \ne v, the matrices S \in \mathfrak{so}_3(k) with (b_u - b_v) + S(\omega_u - \omega_v) = 0 form an affine subspace, and it is proper: were it all of \mathfrak{so}_3(k), taking S = 0 would give b_u = b_v and the three elementary skew matrices would give \omega_u = \omega_v, contradicting distinctness. A finite-dimensional affine space over an infinite field is not a union of finitely many proper affine subspaces, so some S_Z avoids the subspaces of all pairs. Finally x^T S_Z x = 0 holds for a skew matrix over every extension field, with x = \omega_u - \omega_v, so each generator f_{uv} is fixed, and \Phi_{-S_Z} inverts \Phi_{S_Z}.

Example 5.2 of Zheng (2026) illustrates the choice on one coincident pair: if \omega_u - \omega_v = e_3 and b_u = b_v, the shear with S x = e_1 \times x moves the difference of the new coordinates to -e_2 \ne 0 while x \cdot S x = 0 keeps the form.

The formal shear is written with the cross product: for a parameter vector s \in k^3 the map takes (\omega, b) to (\omega, b + \omega \times s), which is the paper's \Phi_S for the skew matrix S x = x \times s, and every skew 3 \times 3 matrix arises this way.

/-- The angular-fixing skew Witt shear with parameter `s`. -/ def shear {k : Type*} [CommRing k] (s : Vec3 k) (X : Twist k) : Twist k := (X.1, X.2 + Vec3.cross X.1 s)

splitKlein_shear is the exact invariance of the form, and algEquiv is the induced automorphism of the polynomial ring, under which map_coefficientSelectedNullIdeal_algEquiv shows the selected-null ideal is literally invariant. The existence half is exists_common_base_shear_snd_ne_zero: one parameter drawn from the infinite base field makes the translational half of every member of a finite family of nonzero twists nonzero at once. Its avoidance argument differs from the paper's in one respect: instead of choosing a point outside finitely many proper affine subspaces of \mathfrak{so}_3, the formal proof restricts the parameter to the moment curve r \mapsto (r, r^2, r^3), where each pair's failure locus becomes the root set of a nonzero univariate polynomial, and exists_base_eval_ne_zero finds a rational point avoiding the product. A table correction from this chapter: the declaration previously named on this node, exists_scalar_shear_snd_ne_zero, states a one-twist version with a coordinate-axis parameter, and nothing in the development calls it.