Registry · Proposition IV.P21 tau-effective formalized

IV.P21 — Generic Entanglement

Separable states have measure zero; entangled states are dense and generic. Rank-1 tensors have infinite codimension.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (2)

IV.D64 IV.D62

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.GenericEntanglement