Registry · Definition II.D60 established formalized

II.D60 — Spectral Algebra

The algebra A_spec(L) of idempotent-supported characters on L = S^1 v S^1 valued in calibrated H_tau, with bipolar decomposition and ring structure from pointwise operations.

Book II Part 9 Ch. 51

Dependency Graph

Depends on (6)

I.D18 I.D19 I.D21 II.D35 II.D59 II.P13

Depended on by (8)

II.C01 II.D65 II.D72 II.D77 II.R18 II.R28 II.T42 II.T49

Lean Formalization

Module: TauLib.BookII.CentralTheorem.CentralTheorem

Symbol: Tau.BookII.CentralTheorem.SpectralAlgebraElement