Registry · Definition IV.D67 tau-effective formalized

IV.D67 — Observable

Self-adjoint operator Â: H_τ → H_τ with ⟨f, Âg⟩ = ⟨Âf, g⟩. Guarantees real eigenvalues, orthogonal eigenstates, spectral completeness.

Book IV Part 3 Ch. 19

Dependency Graph

Depends on (2)

IV.D66 IV.D62

Depended on by (1)

IV.P24

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.Quantization

Symbol: Tau.BookIV.QuantumMechanics.Observable