Registry · Proposition IV.P24 tau-effective formalized

IV.P24 — X and P Are Self-Adjoint

X̂ = -iℏ_τ ∂/∂θ_γ and P̂ = -iℏ_τ ∂/∂θ_η are self-adjoint. Boundary terms vanish because T² is compact.

Book IV Part 3 Ch. 19

Dependency Graph

Depends on (3)

IV.D67 IV.D66 IV.D61

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.Quantization

Symbol: Tau.BookIV.QuantumMechanics.XAndPAreSelfadjoint