EmbeddedWordClassification.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The cofinal invariant-word classification for actual tracial matrix embeddings. Finite labels and contraction compatibility are both derived.

theorem OAI.KadisonSimilarity.embedded_word_contractions line 29

Source documentation

Raw compatible matrix inclusions supply the contractions on every cofinal tail and for every fixed pair of word degrees.

theorem embedded_word_contractions
    (k l b s : ℕ) (p : Equiv.Perm (Option (Fin k ⊕ Fin l)))
    (a : Option (Fin k ⊕ Fin l) → Matrix (A b) (A b) ℂ) :
    normalizedPermutationContraction p
      (fun i => (tracialMatrixTowerOfEmbeddings τ V L hinner hmul M htrace S hsize).transition b (b + s) (Nat.le_add_right b s) (a i)) =
      normalizedPermutationContraction p a :=
…

Mentions: OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.tracialMatrixTowerOfEmbeddings

theorem OAI.KadisonSimilarity.embedded_word_levels_preserved line 49
Source documentation
Actual tracial matrix embeddings imply preservation of every word degree, using the proved stable Schur--Weyl theorem on each cofinal tail.
```
theorem embedded_word_levels_preserved (n : ℕ) :
    Y.comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp (U.block Y n n) :=
…
```

theorem OAI.KadisonSimilarity.embedded_wordLevelRepeatedOperator_apply line 57

Source documentation

The canonical bounded multiplicity operator acts on all repeated words.

theorem embedded_wordLevelRepeatedOperator_apply (n : ℕ) (a : G 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 hmul 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_wordLevelRepeatedOperator_adjoint_apply line 68

Source documentation

Bundled star and unitary representations give the adjoint repeated-word identity, with the adjoint of the same canonical multiplicity operator.

theorem embedded_wordLevelRepeatedOperator_adjoint_apply
    (leftRep : ∀ s, Matrix (A s) (A s) ℂ →⋆ₐ[ℂ] (H →L[ℂ] H))
    (left_eq : ∀ s a, C.leftAction s a = leftRep s a)
    (unitaryRep : ∀ s, Matrix.unitaryGroup (A s) ℂ →* unitary (H →L[ℂ] H))
    (unitary_eq : ∀ s a, C.unitaryAction s a = (unitaryRep s a : H →L[ℂ] H))
    (n : ℕ) (a : G 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 hmul M htrace S hsize) U Y n).adjoint a)
        (endpointWord d (fun _ : Fin n => r))) := by
…