SmallFreeCornerTransport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The entire small-corner construction is transported together through the chosen free-position embedding, so the Haar unitary and reflection retain the same support projection as the matrix frame.

def OAI.KadisonSimilarity.MatrixUnitColumnFamily.map line 16
def OAI.KadisonSimilarity.TracialMatrixUnitColumnFamily.map line 32
def OAI.KadisonSimilarity.SmallFreeCornerData.transport line 41
Source documentation
A single embedding carries every piece of the small-corner data, with the original numerical cutoff unchanged.
```
def SmallFreeCornerData.transport (Q : SmallFreeCornerData τA s) :
    SmallFreeCornerData τB s where
…
```
Mentions: OAI.KadisonSimilarity.SmallFreeCornerData