Registry · Theorem III.T14 tau-effective formalized

III.T14 — Spectral Trichotomy Lemma

Every boundary character at level n decomposes uniquely into B-supported, C-supported, and X-mixing components. The decomposition is exact, orthogonal, and functorial (commutes with level change).

Book III Part 3 Ch. 19

Dependency Graph

Depends on (2)

III.D23 III.T10

Depended on by (16)

III.D24 III.D26 III.D47 III.P10 III.P14 III.P18 III.P19 III.P20 III.R09 III.T15 III.T16 III.T19 III.T20 III.T26 III.T28 III.T54

Lean Formalization

Module: TauLib.BookIII.Spectral.Trichotomy

Symbol: trichotomy_check