EmbeddedWordStructure.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Word-level structure from actual tracial matrix actions. The application interface has no abstract covariance record: it contains only represented matrix actions, their raw word formulas, and commutation.

theorem OAI.KadisonSimilarity.embedded_actions_word_levels_preserved line 47
Source documentation
Actual represented matrix symmetries force preservation of every word level; the covariance and finite labels are derived in the proof.
```
theorem embedded_actions_word_levels_preserved (n : ℕ) :
    Y.comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp (U.block Y n n) :=
…
```

theorem OAI.KadisonSimilarity.embedded_actions_repeated_word line 56

Source documentation

The canonical multiplicity compression acts on every repeated word.

theorem embedded_actions_repeated_word (n : ℕ) (a : J n) (d : E)
    (r : centeredSubspace (V 1)) :
    Y (U.inclusion n (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r)))) =
      U.inclusion n (hilbertTensorInsert
        (wordLevelRepeatedOperator (tracialMatrixTowerOfEmbeddings τ V L hinner hleft M htrace S hsize)
          U Y n a) (endpointWord d (fun _ : Fin n => r))) :=
…

Mentions: OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.wordLevelRepeatedOperator, OAI.KadisonSimilarity.tracialMatrixTowerOfEmbeddings

theorem OAI.KadisonSimilarity.embedded_actions_adjoint_repeated_word line 69
Source documentation
Taking adjoints gives the same repeated-word action with the adjoint of the canonical multiplicity operator; no second covariance input is needed.
```
theorem embedded_actions_adjoint_repeated_word (n : ℕ) (a : J n) (d : E)
    (r : centeredSubspace (V 1)) :
    Y.adjoint (U.inclusion n (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r)))) =
      U.inclusion n (hilbertTensorInsert
        ((wordLevelRepeatedOperator (tracialMatrixTowerOfEmbeddings τ V L hinner hleft M htrace S hsize)
          U Y n).adjoint a) (endpointWord d (fun _ : Fin n => r))) :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.wordLevelRepeatedOperator, OAI.KadisonSimilarity.tracialMatrixTowerOfEmbeddings