CofinalMatrixTowers.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Word degrees are fixed before the matrix stage is chosen. Cofinal tails let each degree start in its own stable range; no single finite stage must accommodate every number of tensor slots.

theorem OAI.KadisonSimilarity.iUnion_nat_tail line 23
def OAI.KadisonSimilarity.TracialMatrixTower.tail line 33
Source documentation
Discarding finitely many matrix stages preserves every geometric field of the tower and its dense union.
```
def TracialMatrixTower.tail
    (T : TracialMatrixTower (E := E) (F := F) (A := A)) (b : ℕ) :
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower
theorem OAI.KadisonSimilarity.TracialMatrixTower.exists_tail_labels line 69
Source documentation
Every fixed finite set of tensor slots has injective labels at all stages of a sufficiently late tail.
```
theorem TracialMatrixTower.exists_tail_labels
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower
def OAI.KadisonSimilarity.WordLevelMatrixActions.tail line 87
Source documentation
Ambient actions restrict to the same cofinal sequence of matrix stages.
```
def WordLevelMatrixActions.tail
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower
theorem OAI.KadisonSimilarity.cofinal_word_levels_preserved line 115
Source documentation
Each off-diagonal degree pair uses its own cofinal stable range. In particular no fixed finite matrix algebra needs infinitely many labels.
```
theorem cofinal_word_levels_preserved (n : ℕ) :
    Y.comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp (U.block Y n n) := by
…
```
theorem OAI.KadisonSimilarity.cofinal_wordLevelRepeatedOperator_apply line 131
Source documentation
Repeated-word action with the finite-label requirement discharged using the matrix-size limit, separately for each word degree.
```
theorem cofinal_wordLevelRepeatedOperator_apply (n : ℕ) (a : G n) (d : E) (r : F) :
    Y (U.inclusion n (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r)))) =
      U.inclusion n (hilbertTensorInsert (wordLevelRepeatedOperator T U Y n a)
        (endpointWord d (fun _ : Fin n => r))) := by
…
```
Mentions: OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.wordLevelRepeatedOperator