FreePositionMatrices.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The published conjugacy input is used once, for the prescribed irreducible inclusion. Its concrete conjugated copy retains the original matrix tower and real orthonormal sequence.

theorem OAI.KadisonSimilarity.exists_conjugated_free_matrix_copy line 32
Source documentation
Conditional free position with all matrix-density data retained. The only freeness assumption is the stated Popa specialization; none of the operator estimates of the present manuscript occurs in it.
```
theorem exists_conjugated_free_matrix_copy
    (hω : (ω : Filter ℕ) ≤ Filter.cofinite)
    (ρ : R →⋆ₐ[ℂ] A) (hρ : Function.Injective ρ)
    (hρτ : ∀ x, τA (ρ x) = τR x)
    (hfA : ∀ a : A, τA (star a * a) = 0 → a = 0)
    (M : NestedTracialMatrices (A := I) τR.toLinearMap (gnsTracialVector τR))
…
```
Mentions: OAI.KadisonSimilarity.NestedTracialMatrices, OAI.KadisonSimilarity.gnsTracialVector