Split-Complex Scalars

Split-complex unit j with j^2 = +1 (not i^2 = -1). Earned from boundary ring structure. The foundational scalar field for tau-holomorphy.

Split-Complex Scalars

Summary

Split-complex unit j with j^2 = +1 (not i^2 = -1). Earned from boundary ring structure. The foundational scalar field for tau-holomorphy.

Statement

%
\label{def:split-complex}
The \textbf{split-complex scalar ring}
$\hat{\mathbb{Z}}_\tau[j]$ is the free $\hat{\mathbb{Z}}_\tau$-module
of rank 2, with basis $\{1, j\}$,
equipped with the multiplication rule:
\[
    \boxed{%
    j^2 = +1.}
\]
Every element of $\hat{\mathbb{Z}}_\tau[j]$
has a unique representation:
\[
    x = a + bj,
    \quad a, b \in \hat{\mathbb{Z}}_\tau.
\]
Multiplication is defined by:
\[
    (a + bj)(c + dj)
    = (ac + bd) + (ad + bc)j,
\]
using the distributive law and $j^2 = +1$.
Addition is componentwise:
\[
    (a + bj) + (c + dj) = (a + c) + (b + d)j.
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 38
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part10/ch40-split-complex-scalars.tex lines 55-82

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.SplitComplex
• Name: Tau.Boundary.SplitComplex

Dependencies

• Canonical: I.D19

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.