TracialEmbeddingTransport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A trace-preserving embedding transports the completed tracial space, the dense matrix tower, and its real orthonormal sequence to its actual range. No normal-form or matrix-density assumption is added at the target.

theorem OAI.KadisonSimilarity.tracialRangeVector_norm line 22
def OAI.KadisonSimilarity.tracialRangeIsometry line 31
Source documentation
The completed trace-preserving map lands in the actual closed range space.
```
def tracialRangeIsometry : τ.GNS →ₗᵢ[ℂ] G.baseSpace φ.range :=
…
```
theorem OAI.KadisonSimilarity.tracialRangeIsometry_vector line 35
theorem OAI.KadisonSimilarity.tracialRangeIsometry_surjective line 41
def OAI.KadisonSimilarity.tracialRangeUnitary line 52
Source documentation
The range completion is unitarily the original tracial GNS space.
```
def tracialRangeUnitary : τ.GNS ≃ₗᵢ[ℂ] G.baseSpace φ.range :=
…
```
theorem OAI.KadisonSimilarity.tracialRangeUnitary_vector line 56
def OAI.KadisonSimilarity.transportTracialMatrices line 65
Source documentation
A concrete matrix tower stays dense after a trace-preserving embedding.
```
def transportTracialMatrices
    (M : NestedTracialMatrices (A := I) τ.toLinearMap (gnsTracialVector τ)) :
…
```
Mentions: OAI.KadisonSimilarity.NestedTracialMatrices, OAI.KadisonSimilarity.gnsTracialVector
def OAI.KadisonSimilarity.transportRealTracialSequence line 89
Source documentation
The real trace-orthonormal sequence is transported algebraically.
```
def transportRealTracialSequence (S : RealTracialSequence τ.toLinearMap) :
    RealTracialSequence (G.trace.comp φ.range.subtype.toLinearMap) where
…
```
Mentions: OAI.KadisonSimilarity.RealTracialSequence