Cancellation in the enveloping monoid of Hilbert subspaces

The closed subspaces of a real or complex Hilbert space form a partial commutative monoid under orthogonal direct sum. We prove that its enveloping commutative monoid is cancellative exactly when the Hilbert space has dimension at most two. This gives a negative answer in every higher dimension to a question of Friedrich Wehrung appearing in his 2015 preprint on refinement monoids. The obstruction is an explicit configuration of sixteen integer directions and eight orthogonal bases in dimension three. Its basis relations yield u + c = v + c, whereas a rank-one rigidity argument gives u ≠ v. The same configuration works over both scalar fields and in arbitrary ambient dimension. We include the known small-dimensional cases. The universal-group measure is injective on individual subspaces in every dimension. Code and verification data: https://github.com/eulogica/cancellation-hilbert-subspaces