Registry · Proposition IV.P18 tau-effective formalized

IV.P18 — Inner Product Uniqueness

The canonical inner product is unique given σ-equivariance, ρ-compatibility, and fiber normalization.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (1)

IV.D61

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.InnerProductUniqueness