Proposition. Finite blade coordinates refine Clifford multiplication [fcap-002P]
AGENTDRAFTED
Retain the orthogonal \(R\)-basis \(b:I\to M\) and the inverse of \(2\)
from the preceding theorem. Let \(\mathcal C\) be the \(R\)-module of finitely
supported coefficient families \(c=(c_s)\) indexed by finite subsets of \(I\),
and let \(\delta _s\) be its standard coordinate vectors. Define a bilinear
product by the structure constants
\[\delta _s\ast \delta _t
=k(s,t)\delta _{s\mathbin {\triangle }t}.\]
Equivalently, for every finite subset \(u\),
\[(c\ast d)_u
=\sum _{\substack {s\in \operatorname {supp}(c),\ t\in \operatorname {supp}(d)\\
s\mathbin {\triangle }t=u}}
c_s d_t k(s,t).\]
The sum and the resulting support are finite, even when \(I\) is infinite.
Let
\[\eta (c)=\sum _s c_sE_s,\qquad
\operatorname {enc}=\eta ^{-1}.\]
The transported-basis identification in the preceding theorem makes \(\eta \)
a linear equivalence, and its multiplication refinement is
\[\eta (c\ast d)=\eta (c)\eta (d),\qquad
\operatorname {enc}(xy)
=\operatorname {enc}(x)\ast \operatorname {enc}(y).\]
To prove the first equality, expand the two finite sums, apply the blade
product to each pair, and regroup by symmetric difference. The second follows
by applying \(\eta ^{-1}\). Thus the displayed structure constants, rather than
an implicit transport definition, determine the coordinate product.
For example, work over \(\mathbb Q\) with ordered indices \(0<1<2\) and
diagonal values \((q_0,q_1,q_2)=(0,2,-3)\). The formula gives
\[\begin {aligned}
E_{\{0,2\}}E_{\{1,2\}}&=3E_{\{0,1\}},&
E_{\{1,2\}}E_{\{0,2\}}&=-3E_{\{0,1\}},\\
E_{\{0,1\}}E_{\{0,2\}}&=0,&
E_{\{1,2\}}^2&=6.
\end {aligned}\]
The first product has one strict cross inversion, the second has two, and the
third retains the repeated radical factor \(q_0=0\). Also
\[(\delta _{\{0,2\}}+2\delta _{\{0,1\}})\ast \delta _{\{1,2\}}
=3\delta _{\{0,1\}}+4\delta _{\{0,2\}}.\]
This matches
\((E_{\{0,2\}}+2E_{\{0,1\}})E_{\{1,2\}}\). Nonzero basis blades remain
basis vectors although their products can vanish.
Orthogonality is essential to the symmetric-difference rule. Over
\(\mathbb Q\), take
\(Q(xe_0+ye_1)=x^2+xy+y^2\). Then \(B_Q(e_0,e_1)=1\) and
\[T_Q(\iota _Q(e_0)\iota _Q(e_1))
=e_0\wedge e_1+\frac 12.\]
The correction is the half-polar value. The general construction in
Definition [fcap-0003] already gives \(T_Q\) as a linear equivalence; this example
shows directly that it is not an algebra equivalence. The contraction and
change-of-form recurrences in
[wieser2024formalizing, 8.4, (8.54)--(8.55), p. 106]
give the same sign and normalization.
The ascending-basis theorem and change-of-form maps in
[grinberg2016clifford, Theorem 2, p. 3, and Theorems 34--35, pp. 55--56]
corroborate the ordered basis and orthogonal transport. The latter is the
specialization with symmetric half-polar form \(B_Q/2\); an arbitrary
nonsymmetric form with the same diagonal need not define this transport.
Wieser's exterior equivalence likewise assumes an inverse of \(2\)
[wieser2024formalizing, 9.3.5, p. 120].
The displayed finite formula is a mathematical coordinate refinement.
The currently public FCAP basis transport is noncomputable and does not expose
an executable coordinate type, multiplication kernel, or encode/decode
product theorem. Those declarations, together with any fixed finite-slot or
floating-point contract, remain a separate implementation step.