1.12 Exact arithmetic coordinates and their complex meaning
On this page · Permalink · Source line 1165
The twelfth root contains \(\sqrt3\) and \(i\). Its relevant exact arithmetic can be represented without floating-point trigonometric evaluation. Let a tuple
denote
The coordinate root is \((0,1/2,1/2,0)\), whose interpretation is \(\sqrt3/2+i/2\). Coordinate conjugation sends \((a,b,c,d)\) to \((a,b,-c,-d)\). Addition is entrywise, and multiplication is
Theorem QA17: Sound interpretation of the exact operations
The map \(\iota\) preserves zero, one, rational scalars, addition, multiplication, conjugation, natural powers, and finite sums. Therefore an equality obtained with these exact coordinate operations yields the corresponding equality in \(\mathbb C\).
Proof
The claims for zero, one, rational scalars, addition, and conjugation follow directly from the definition. For multiplication, write the two interpreted values as \((a+b\sqrt3)+i(c+d\sqrt3)\) and \((A+B\sqrt3)+i(C+D\sqrt3)\). Their product has real part
and imaginary part
Expanding and using \((\sqrt3)^2=3\) gives exactly the displayed tuple product. Power preservation follows by induction from multiplication and one. Finite-sum preservation follows by induction from addition and zero. Applying a function to equal coordinate tuples gives equal complex numbers. \(\square\)
Only sound transport of equalities is needed here. The formal source does not install the tuple type as a global field instance, and it does not need an injectivity theorem for \(\iota\). It proves preservation of the actual operations and explicitly connects the scales and root to their conventional complex formulas.
The matrix interpretation is entrywise. Since multiplication is a finite sum of products and the adjoint uses conjugation, QA17 also transports coordinate matrix multiplication and adjoints. The same argument transports matrix action on vectors and squared norms. This is what closes the gap between an exact coordinate certificate and an identity about an ordinary complex unitary matrix.