Spectral Coefficients

Spectral coefficients of a StageFun at input n, stage k: the B-sector and C-sector outputs. Together they fully determine the function value.

Spectral Coefficients

Summary

Spectral coefficients of a StageFun at input n, stage k: the B-sector and C-sector outputs. Together they fully determine the function value.

Statement

%
\label{def:holfun-spectral-coefficients}
Let $f \in \mathrm{Hol}(\mathbb{L})$
(Definition~\ref{def:hol-L}, I.D49).
For each primorial stage $k \geq 1$,
the \textbf{spectral coefficients of $f$ at stage $k$}
are:
\[
    \boxed{%
    (a_k(f),\; b_k(f))
    \;:=\;
    \bigl(\chi_+(f_k),\; \chi_-(f_k)\bigr)
    \;\in\;
    \mathbb{Z}/M_k\mathbb{Z} \times \mathbb{Z}/M_k\mathbb{Z},}
\]
where $f_k$ denotes the action of $f$
at the $k$-th primorial stage
(the reduction of $f(t)$ modulo $M_k$
for any omega-tail $t$ of depth $\geq k$),
and $\chi_\pm$ are the fundamental characters
(Definition~\ref{def:lemniscate-characters}, I.D37).
The full \textbf{spectral coefficient sequence} is
$\hat{f} := \bigl((a_k(f), b_k(f))\bigr)_{k \geq 1}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 148
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part16/ch60-spectral-coefficients.tex lines 61-85

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Holomorphy.SpectralCoefficients
• Name: Tau.Holomorphy.SpectralCoeff

Dependencies

• Canonical: I.D47, I.D37, I.T21

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.