7.1. The Split-Klein form
Definition7.1.1
Group: The paper's algebraic argument: the form, the ideal, the shear, the dimension formula, and the height theorem. (5)
Associated Lean declarations
-
RB31E2E.Twist.splitKlein[complete]
The Split–Klein quadratic form on the six-dimensional twist space
k^3 \oplus k^3 is
q(\omega, b) = \omega \cdot b,
the bilinear dot product of the angular part against the translational part.
(Zheng, 2026, Equation 5.1)
Lean code for Definition7.1.1●1 definition
Associated Lean declarations
-
RB31E2E.Twist.splitKlein[complete]
Associated Lean declarations
-
RB31E2E.Twist.splitKlein[complete]
-
defdefined in RB31EndToEnd/Linear/Vec3Twist.leancomplete
def RB31E2E.Twist.splitKlein.{u_1} {k : Type u_1} [CommRing k] (X : RB31E2E.Twist k) : k
def RB31E2E.Twist.splitKlein.{u_1} {k : Type u_1} [CommRing k] (X : RB31E2E.Twist k) : k
The split Klein quadratic polynomial `ω · v`.
The form is hyperbolic of signature (3,3) over \R, though the paper
uses no signature property: what the arguments use is that q vanishes on
the twist differences of pinned pairs, which is
Lemma 6.2 of the necessity chapter, and that a skew
shear preserves it exactly, which is the next lemma. In the formalization
the form is one line over any commutative ring, on the twist type of
the necessity chapter, and the dot product is the
bilinear coordinate sum rather than a Hermitian product:
/-- The bilinear coordinate dot product (not a Hermitian product). -/
def dot {k : Type*} [CommSemiring k] (x y : Vec3 k) : k :=
∑ i, x i * y i/-- The split Klein quadratic polynomial `ω · v`. -/
def splitKlein {k : Type*} [CommRing k] (X : Twist k) : k :=
Vec3.dot X.1 X.2