Lemma. Vanishing list contraction [wieser2024formalizing, 8.4, (8.54)] [fcap-0005]
Lemma. Vanishing list contraction [wieser2024formalizing, 8.4, (8.54)] [fcap-0005]
Let \(R\) be a commutative ring, \(M\) an \(R\)-module, \(Q\) a quadratic form on \(M\), and \(d : M \to R\) a linear functional. For a list \(l\) of generators, define an ordered product by \[P_Q([])=1, \qquad P_Q(m::l)=\iota _Q(m)P_Q(l),\] and write \(C_{Q,d}\) for left contraction by \(d\). The condition \(\forall m\in l,\ d(m)=0\) forces \(C_{Q,d}(P_Q(l))=0\).
There is one induction calculation. The empty product contracts to zero. At a head \(m\), the generator recurrence \[C_{Q,d}(P_Q(m::l))=d(m)P_Q(l)-\iota _Q(m)C_{Q,d}(P_Q(l))\] is the local rule in [wieser2024formalizing, 8.4, (8.54)]. The hypothesis deletes the first summand, and the induction hypothesis deletes the second. This turns the recurrence into a finite-list vanishing criterion rather than a calculation for one fixed product.
The conclusion depends only on the ordered recurrence and pointwise vanishing of \(d\) on the list. In particular, it is independent of a basis or any reordering convention.