Theorem. Pairwise orthogonal list transport [wieser2024formalizing, 8.4, (8.55)] [fcap-0006]

✍️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\). 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.