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\). For a list \(l\) of vectors, write
\[P_Q([])=1, \qquad P_Q(m::l)=\iota _Q(m)P_Q(l),\]
and write \(T_Q\) for the linear equivalence CliffordAlgebra.equivExterior from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(\bigwedge _R M\). In the corresponding zero-form product notation, suppose every earlier vector in \(l\) is \(Q\)-orthogonal to every later vector. Then
\[T_Q(P_Q(l))=P_0(l).\]
The order of the list is unchanged. The equality concerns this product under the stated orthogonality condition; it does not say that \(T_Q\) preserves arbitrary products.
The calculation proceeds from the head of the list. The one-generator change-of-form recurrence separates \(T_Q(P_Q(m::l))\) into the zero-form generator \(\iota _0(m)\) times the transported tail and a left-contraction correction. Pairwise orthogonality makes the associated dual vector vanish on every member of the tail. The criterion in Lemma [fcap-0005] therefore kills the correction, and the induction hypothesis transports the tail.
The contraction recurrence in [wieser2024formalizing, 8.4, (8.54)], the change-of-form recurrence in [wieser2024formalizing, 8.4, (8.55)], and the exterior equivalence in [wieser2024formalizing, 9.3.5] supply the local identities. Their induction over a pairwise-orthogonal list gives the displayed theorem; the source locations do not state that finite-list consequence separately.
The order of the list is fixed throughout. Reordering would require an additional permutation-sign calculation and is not a consequence of this theorem.