Boundary Normal Form

Every element of ℤ/Prim(k)ℤ[j] has unique normal form a·e₊ + b·e₋ where a is B-supported and b is C-supported. Computable, respects ring operations.

Boundary Normal Form

Summary

Every element of ℤ/Prim(k)ℤ[j] has unique normal form a·e₊ + b·e₋ where a is B-supported and b is C-supported. Computable, respects ring operations.

Statement

%
\label{def:boundary-normal-form}
Let $z = x + y\jj \in R_k^{\jj}$.
The \textbf{boundary normal form} of~$z$ is
\begin{equation}\label{eq:ch19-bnf}
    z \;=\; a \cdot e_+ \;+\; b \cdot e_-,
    \qquad
    a = x + y,\quad b = x - y,
\end{equation}
computed in $\Z / \mathrm{Prim}(k)\Z$.
The coefficient $a$ is the \textbf{$B$-sector coordinate}
and $b$ is the \textbf{$C$-sector coordinate}.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 54
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part03/ch19-the-spectral-trichotomy.tex lines 262-275

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Spectral.Trichotomy
• Name: boundary_normal_form

Dependencies

• Canonical: III.T14

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.