Registry · Theorem I.T29 tau-effective formalized

I.T29 — Spectral Determination

Spectral Determination: two StageFuns with identical spectral coefficients at all inputs and stages are equal. The spectral decomposition is faithful.

Book I Part 16 Ch. 60

Dependency Graph

Depends on (2)

I.D65 I.D66

Depended on by (1)

I.T31

Lean Formalization

Module: TauLib.BookI.Holomorphy.SpectralCoefficients

Symbol: Tau.Holomorphy.spectral_determines