OAI/Analysis/KadisonKastler/PublishedPointedOperations.lean

Pointed-product construction and its canonical identifications

Blackadar, Operator Algebras, III.3.1.1--2 (pp.293--294), defines the pointed Hilbert product as the completion of the finite-support tensors, with their product inner products. A weight-preserving reindexing is therefore an isometry on those tensors and extends to the completion. Splitting the index set into two parts gives the usual Hilbert tensor product and the generated spatial algebra.

These inputs retain only the lambda-only construction and the sum and reindex identifications. The two-ratio absorption statement is proved from the explicit even/odd bijection, rather than included here.