ScalarKaplansky.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The two-test-vector specialization of matrix Kaplansky density and C*-quotient norm lifting is enough for the scalar commutator closure used in the final derivation and separability reductions.

def OAI.KadisonSimilarity.TwoVectorKaplanskyInput line 17
Source documentation
Blackadar, I.9.1.3, specialized to two vectors, followed by quotient norm lifting. This precise published input contains no commutator estimate.
```
def TwoVectorKaplanskyInput (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (P : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonSimilarity.scalarKaplanskyClosure_of_twoVector line 23
Source documentation
A bound on the original algebra extends to its von Neumann closure using only the two vectors needed for each commutator test.
```
theorem scalarKaplanskyClosure_of_twoVector
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (P : VonNeumannAlgebra H)
    (kaplansky : TwoVectorKaplanskyInput σ P) : ScalarKaplanskyClosure σ P := by
…
```
Mentions: OAI.KadisonSimilarity.TwoVectorKaplanskyInput, OAI.KadisonSimilarity.ScalarKaplanskyClosure