Elliptic Complex Field

TauComplex = TauReal[i]/(i^2+1): the elliptic complex field. Pairs (re, im) of TauReal values with multiplication (ac-bd, ad+bc). The imaginary unit i satisfies i^2 = -1.

Elliptic Complex Field

Summary

TauComplex = TauReal[i]/(i^2+1): the elliptic complex field. Pairs (re, im) of TauReal values with multiplication (ac-bd, ad+bc). The imaginary unit i satisfies i^2 = -1.

Statement

%
\label{def:tau-complex-field}
The \textbf{$\tau$-complex field} is the quotient ring:
\[
    \boxed{%
    \mathbb{C}_\tau := \mathbb{R}_\tau[x] \,/\, (x^2 + 1).}
\]
We write $i$ for the image of $x$ in the quotient,
so that $i^2 = -1$.
Every element of $\mathbb{C}_\tau$ has a unique representation
as an ordered pair:
\[
    z = a + bi, \quad a, b \in \mathbb{R}_\tau.
\]
The component $a = \operatorname{Re}(z)$ is the \textbf{real part}
and $b = \operatorname{Im}(z)$ is the \textbf{imaginary part}.
The operations are:
\begin{align*}
    (a + bi) + (c + di) &= (a + c) + (b + d)i, \\
    (a + bi)(c + di)    &= (ac - bd) + (ad + bc)i,
\end{align*}
the second rule following from the distributive law and $i^2 = -1$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 190
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part17/ch77-elliptic-complex-field.tex lines 51-74

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.ComplexField
• Name: Tau.Boundary.TauComplex

Dependencies

• Canonical: I.D84, I.P39

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.