Residue

The split-complex residue extracted from the n = -1 Laurent coefficients. The bipolar residue decomposes into independent +/- channel contributions.

Residue

Summary

The split-complex residue extracted from the n = -1 Laurent coefficients. The bipolar residue decomposes into independent +/- channel contributions.

Statement

%
\label{def:residue}
Let $f$ be an $\omega$-germ transformer
with Laurent expansion
$\sum_n a_n^{(+)} e_+ \phi_n^{(+)}
+ \sum_n a_n^{(-)} e_- \phi_n^{(-)}$.
The \textbf{residue} of~$f$ at a $\tau$-admissible
point~$x$ is the split-complex number:
\[
    \boxed{%
    \mathrm{Res}_x(f)
    \;:=\;
    a_{-1}^{(+)}\, e_+
    \;+\;
    a_{-1}^{(-)}\, e_-
    \;\;\in\;\;
    H_\tau.}
\]
The residue is the \textbf{spectral coefficient
at frequency $n = -1$},
extracted independently
from the B-channel and C-channel.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 98
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part06/ch34-laurent-residues.tex lines 306-329

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Hartogs.LaurentResidue
• Name: tau_residue

Dependencies

• Canonical: II.D42, I.D21, I.T10, II.D35

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.