The GNS representation of the target trace extension

Let be the completed CAR algebra and its normalized trace. Fix a representative shell family and its chosen unitary links in the selected atomic representation . Write for the resulting concrete target and , , for its faithful unital source map. This fixes one target and one source map throughout. Let be the chosen state extension of to . Define to be its GNS representation.

Choose from exists_state_extension_trace and regard that same functional as a positive linear map. Form the GNS completion of modulo its null vectors, set to that Hilbert space, and let . The induced left action is

The right-hand side of the definition is exactly the GNS star homomorphism of traceExtensionPositive family. This positive-map bundle has the same values as ; it is not another state. Normalization gives , so and is nonzero. The GNS construction gives the dense -orbit. Its restriction realizes because . The actual-representation source-cyclicity theorem applies to these two facts and proves the source orbit dense; it is not an assumption smuggled into the definition.

A representative shell family is fixed first. The chosen extension is positive and normalized; its traciality is not needed to perform the GNS construction.

With its canonical unit vector , this representation realizes and has dense target orbit. The separately proved source-cyclicity result also gives

Consequently is separable, since is separable and the displayed orbit map is continuous.

Separability here is a conclusion about the Hilbert space. The algebra is not assumed norm separable. Injectivity of is a separate theorem; irreducibility or purity of is not asserted.