Registry · Definition III.D81 tau-effective formalized

III.D81 — Spectral Projector

Spectral projector P_n for the n-th eigenspace of H_L. Idempotent (P_n² = P_n) and mutually orthogonal (P_n·P_m = 0 for n ≠ m). Verified at finite stages.

Book III Part 4 Ch. 30

Dependency Graph

Depends on (1)

III.D28

Depended on by (4)

III.D82 III.D93 III.P33 III.T56

Lean Formalization

Module: TauLib.BookIII.Doors.SpectralDecomp

Symbol: spectral_projector