Registry · Proposition III.P33 tau-effective formalized

III.P33 — Spectral Resolution

Spectral resolution: H_L = Σ_n λ_n P_n. The lemniscate operator is recovered from its eigenvalues and projectors. Verified at finite stages N=2,6.

Book III Part 4 Ch. 30

Dependency Graph

Depends on (2)

III.D81 III.T56

Lean Formalization

Module: TauLib.BookIII.Doors.SpectralDecomp

Symbol: spectral_resolution_6