feat: add transported exterior basis anchors

[utensil]

Summary

Introduce a coordinate basis of CliffordAlgebra Q by transporting the chosen exterior finite-subset basis through (CliffordAlgebra.equivExterior Q).symm. The module proves its empty-subset and singleton anchors.

Mathematical contribution

For a basis b of the generating module, the module names

B_{Q,b}(s) = (equivExterior Q).symm (E_b(s)).

It proves B_{Q,b}(∅) = 1 and B_{Q,b}({i}) = ι Q (b i). These are the first 2 explicit coordinate anchors; they do not determine a product formula for arbitrary finite subsets.

Theory modeling implications

The selected basis makes a coordinate choice explicit at the boundary from Mathlib's abstract Clifford algebra to later concrete representations. equivExterior is a linear equivalence, not an algebra equivalence, so the construction does not transport Clifford multiplication to exterior multiplication. The API is deliberately provisional: later representation work may refine its names or normal forms, but must preserve the stated mathematical boundary rather than silently treating the chosen coordinates as intrinsic.

Dependencies

No direct FCAP pull-request prerequisites.

Mathematical grounding

• Eric Wieser's 2024 thesis, §9.3.5 provides the exterior-equivalence formalization context. It does not prescribe this named coordinate API; the selected basis interface and its anchors are the formalization bridge in this pull request.
• The pinned Mathlib interfaces are CliffordAlgebra.equivExterior and Module.Basis.ExteriorAlgebra.
• Paired Forest note fcap-0003 states the coordinate choice and its non-multiplicative boundary.

Scope

This pull request includes only the transported basis and its empty and singleton anchors. It does not prove multiplicative preservation, blade-product rules, sign conventions, masks, or executable representations.

Verification

The target module and the full FCAP library build cache-first. Exact-head review found no incomplete declarations, disallowed imports, or stated-boundary drift.

Base

main at e1605218c5105bbab09c2c24cde6ad86bb38bd30.

Review state

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

[utensil]

This is a careful, narrowly scoped first bridge from Mathlib’s abstract Clifford algebra to explicit coordinates.

Its API shape is not final, it's part of my local spike tests, and seems reasonable for the first few baby steps.

Similar things are being pursued in FGAP project, where we explicily write the concrete stuff out, bridging the abstract infrastructure in mathlib, hopefully informative to our symbolic/numeric computation implementation.