feat: add contraction kernels for exterior transport

[utensil]

Summary

Add 2 correction-kernel results for exterior transport: a vanishing criterion for left contraction on an ordered generator product, and the 2-generator equivExterior calculation when orthogonality removes its correction.

Mathematical contribution

For a dual vector d that vanishes on every member of a list l, the module proves that left contraction by d vanishes on List.prod (List.map (ι Q) l). It also proves that Q.IsOrtho m n gives

equivExterior Q (ι Q m * ι Q n) = ι 0 m * ι 0 n.

The contraction criterion has no invertibility-of-2 assumption; the exterior-equivalence calculation retains the assumption required by equivExterior.

Theory modeling implications

The module exposes the correction term that later ordered transport must eliminate, rather than presenting equivExterior as multiplicative. It separates the generic contraction kernel from the additional orthogonality condition that removes the 2-generator correction. This is a deliberately small interface for later list transport, not a general product-preservation theorem.

Dependencies

No direct FCAP pull-request prerequisites.

Mathematical grounding

• Eric Wieser's 2024 thesis, §8.4, equation (8.54) gives the contraction recurrence; §§8.4 and 9.3.5 give the change-of-form and exterior-equivalence context. The finite-list criterion and named 2-generator interface are formalization bridges in this pull request, not claims that the source states these API results.
• The pinned Mathlib interfaces are CliffordAlgebra.contractLeft_ι_mul, CliffordAlgebra.contractLeft_one, CliffordAlgebra.changeForm_ι_mul_ι, and CliffordAlgebra.equivExterior.
• Paired Forest notes fcap-0004 and fcap-0005 state the orthogonal calculation and contraction criterion.

Scope

This pull request includes only these correction-kernel results. It does not prove pairwise-list transport, basis or blade results, sign conventions, encodings, executable representations, or multiplicative equivalence.

Verification

The target module and the full FCAP library build cache-first. Exact-head review checked the distinct assumption boundaries and found no duplicate current Mathlib theorem.

Base

main at e1605218c5105bbab09c2c24cde6ad86bb38bd30.

Review state

Exact head: d8db9d94a89be6d114ed9d89e5e01754423c06c8. Exact-head review has passed and lgta is applied. No dev integration has occurred.

[utensil]

This turns the first orthogonal calculation into a reusable contraction step for the coming ordered-transport work.