Lemma. Orthogonal pair transport [wieser2024formalizing, 8.4] [fcap-0004]

✍️sourceAGENTDRAFTED

Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). Write \(T_Q\) for the linear equivalence from \(\mathcal {C}\kern -2pt\ell (Q)\) to the exterior algebra supplied by CliffordAlgebra.equivExterior. It is a module equivalence, not an algebra equivalence.

For vectors \(m,n \in M\), the change-of-form calculation for \(T_Q(\iota _Q(m)\iota _Q(n))\) has one extra scalar contribution, evaluated by the bilinear form associated to \(-Q\). If \(m\) and \(n\) are \(Q\)-orthogonal, that contribution vanishes. The resulting two-generator calculation is \[T_Q\bigl (\iota _Q(m)\iota _Q(n)\bigr )=\iota _0(m)\iota _0(n).\] This is the first point at which an orthogonality hypothesis changes the transport calculation. It does not turn \(T_Q\) into a multiplicative map.

The change-of-form construction is the relevant mathematical background in [wieser2024formalizing, 8.4], and the Lean construction of \(\operatorname {equivExterior}\) is described in [wieser2024formalizing, 9.3.5]. The concrete geometric-product discussion in [wieser2024formalizing, 2.1.2] motivates the role of orthogonality, but does not provide this note's formal interface.

Thus orthogonality removes precisely the scalar correction in the two-generator change-of-form identity. No basis or reordering convention is needed.