Bipolar Fourier Transform

Formal transform on L using the character group. Expresses functions on L as sums over characters. Feeds into the Central Theorem: O(tau^3) = A_spec(L).

Bipolar Fourier Transform

Summary

Formal transform on L using the character group. Expresses functions on L as sums over characters. Feeds into the Central Theorem: O(tau^3) = A_spec(L).

Statement

%
\label{def:bipolar-fourier}
The \textbf{bipolar Fourier transform} on the algebraic lemniscate
$\mathbb{L} = \hat{\mathbb{Z}}_\tau[j]$
is the ring homomorphism:
\[
    \boxed{%
    \mathcal{F} : \mathbb{L} \to \hat{\mathbb{Z}}_\tau \times \hat{\mathbb{Z}}_\tau,
    \quad
    \mathcal{F}(x) := (\chi_+(x),\; \chi_-(x)).}
\]
For $x = a + bj$:
\[
    \mathcal{F}(a + bj) = (a + b,\; a - b).
\]
The \textbf{inverse bipolar Fourier transform} is:
\[
    \mathcal{F}^{-1}(\alpha, \beta)
    = \alpha e_+ + \beta e_-
    = \frac{\alpha + \beta}{2} + \frac{\alpha - \beta}{2}\, j.
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 91
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part11/ch45-crossing-point.tex lines 291-313

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Boundary.Fourier
• Name: Tau.Boundary.fourier

Dependencies

• Canonical: I.D38, I.D39

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.