PublishedIncreasingMatrixInjectivity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of the increasing matrix construction

The input retains only approximately finite-dimensional implies injective. An explicit primary statement is Connes, Von Neumann algebras, Proceedings ICM (Helsinki, 1978), Acad. Sci. Fennica (1980), 97--109: p. 105 gives the norm-one projection definition and closure under ascending weakly closed unions, and p. 106 displays AFD implies property P implies injectivity.

Primary published volume: https://www.mathunion.org/fileadmin/ICM/Proceedings/ICM1978.1/ICM1978.1.ocr.pdf

The stage sequence and irreducibility are constructed in the existing formalization. Only the ambient contractive projection is retained as a published input; the reverse classification implication is not used.

def OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity line 35
Source documentation
The AFD-to-injective implication specialized to the actual increasing full-matrix stages used in the irreducible subfactor construction.
```
def PublishedIncreasingMatrixInjectivity : Prop :=
…
```
theorem OAI.KadisonKastler.exists_irreducible_injective_subfactor line 43
Source documentation
The constructed irreducible matrix-generated subfactor is injective conditionally only on the indicated published AFD implication.
```
theorem exists_irreducible_injective_subfactor
    (hpub : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity