LEM0012canonicalv1Spectral-Germ Equivalence
Spectral decomposition data is equivalent to germ data: knowing the spectral coefficients of a function at a point determines its omega-germ, and conversely.
Payload
Spectral-Germ Equivalence
Spectral decomposition data is equivalent to germ data: knowing the spectral coefficients of a function at a point determines its omega-germ, and conversely.
Spectral-Germ Equivalence
Summary
Spectral decomposition data is equivalent to germ data: knowing the spectral coefficients of a function at a point determines its omega-germ, and conversely.
Statement
%
\label{lem:spectral-germ}
A stabilized spectral decomposition
with finite support $S_n \subset \widehat{R}_\tau$
determines a unique $\omega$-germ.
Conversely, every $\omega$-germ
arises from a unique stabilized spectral tail.
Proof / Justification
\emph{Forward ($\mathrm{S} \Rightarrow \mathrm{G}$).}
A spectral tail defines a tower-coherent sequence
$(f_k)_{k \geq n}$ by Lemma~\ref{lem:refinement-spectral}.
Two tower-coherent sequences that differ
only at finitely many stages
define the same $\omega$-germ
(they agree eventually).
Since the spectral tail is stabilized,
the induced sequence is eventually constant
in its spectral structure:
the coefficients $(c_\chi)$ do not change
for $k \geq n$.
This determines a unique equivalence class
at the profinite limit---an $\omega$-germ.
The bipolar decomposition ensures uniqueness:
the $e_+$-component and $e_-$-component
of the spectral data
each produce a one-dimensional datum
at the limit,
and the $\omega$-germ is the pair
of these two limiting data.
\emph{Reverse ($\mathrm{G} \Rightarrow \mathrm{S}$).}
An $\omega$-germ is an equivalence class
of tower-coherent sequences
that agree on all sufficiently deep stages.
Pick any representative $(f_k)_{k \geq m}$.
By the compactness of the profinite space
$\tau^3$ (II.T07, Chapter~\ref{ch:stone-space}),
the spectral support of $(f_k)$
stabilizes at some stage~$n \geq m$:
for $k \geq n$, no new characters enter the support.
The resulting spectral tail
is independent of the representative chosen,
since any two representatives agree
for $k$ sufficiently large.
Source Context
- Registry source:
book-02.jsonlline 86 - Manuscript source:
2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part06/ch31-mutual-determination.texlines 294-302
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookII.Hartogs.MutualDetermination - Name:
Tau.BookII.Hartogs.spectral_germ_check
Dependencies
- Canonical: I.D21, II.D14, II.D33, II.L02
Related Results
Generated by later projection phases.
Related Publications
Generated by later projection phases.
Revision Notes
- 2026-04-24: Initial pilot migration.
Identifiers
Aliases & legacy IDs
II.L03spectral-germ-equivalencelem:spectral-germRelease lines
corpus_v3_workingcorpus_v2Relations
Appears in (1)
Sources
Version & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.