TracialEmbeddedWordStructure.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The actual tracial free-product actions instantiate finite-stage word classification. Both head covariance and matrix-unitary covariance follow from the ordinary reduced-word formula.

def OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixLeftRepresentation line 26
Source documentation
The matrix stage acts by actual ambient left multiplication.
```
def tracialMatrixLeftRepresentation (s : ℕ) : Matrix (I s) (I s) ℂ →⋆ₐ[ℂ] (H →L[ℂ] H) :=
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryRepresentation line 33
Source documentation
The finite matrix group acts by its constructed free-product automorphisms.
```
def tracialMatrixUnitaryRepresentation (s : ℕ) :
    Matrix.unitaryGroup (I s) ℂ →* unitary (H →L[ℂ] H) :=
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.baseTracialMatrixTower line 41
Source documentation
The finite matrix tower constructed from its actual tracial embeddings.
```
def baseTracialMatrixTower :=
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixLeftRepresentation_inclusion line 58

Source documentation

The left matrix covariance is the derived tracial head formula.

theorem tracialMatrixLeftRepresentation_inclusion (s : ℕ) (a : Matrix (I s) (I s) ℂ)
    (n : ℕ) :
    (G.tracialMatrixLeftRepresentation D M s a).comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp
        (hilbertTensorLift (endpointHeadAction (n := n)
…

Mentions: OAI.KadisonSimilarity.hilbertTensorLift, OAI.KadisonSimilarity.endpointHeadAction

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialMatrixUnitaryRepresentation_inclusion line 70

Source documentation

The unitary covariance is derived from the published algebraic extension and the completed bounded-word identity.

theorem tracialMatrixUnitaryRepresentation_inclusion (s : ℕ)
    (u : Matrix.unitaryGroup (I s) ℂ) (n : ℕ) :
    (G.tracialMatrixUnitaryRepresentation A D M hgen hfaithful hext s u : H →L[ℂ] H).comp
        (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp
        (hilbertTensorLift (tracialMatrixWordAction (G.baseGeometry D).trace
          (G.baseGeometry D).vector (G.baseGeometry D).left (M.embedding s)
          (G.baseGeometry D).inner_vector (G.baseGeometry D).left_vector
          (G.baseGeometry D).tracial
          (NestedTracialMatrices.denseRange_vector (G.baseGeometry D).trace
            (G.baseGeometry D).vector M) u n).toContinuousLinearMap) := by
…

Mentions: OAI.KadisonSimilarity.hilbertTensorLift, OAI.KadisonSimilarity.tracialMatrixWordAction, OAI.KadisonSimilarity.NestedTracialMatrices.denseRange_vector

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracial_word_levels_preserved line 92
Source documentation
Actual free-product symmetries force preservation of every word level.
```
theorem tracial_word_levels_preserved (n : ℕ) :
    Y.comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp (U.block Y n n) :=
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.tracialWordRepeatedOperator line 105
Source documentation
The canonical multiplicity compression for the actual matrix tower.
```
def tracialWordRepeatedOperator (n : ℕ) :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_tracialWordRepeatedOperator_le line 110
Source documentation
The actual repeated coefficient is a contraction of the ambient operator.
```
theorem norm_tracialWordRepeatedOperator_le (n : ℕ) :
    ‖G.tracialWordRepeatedOperator A D M S hsize U Y n‖ ≤ ‖Y‖ :=
…
```

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialWordRepeatedOperator_adjoint line 116

Source documentation

Its adjoint is the coefficient obtained from the ambient adjoint.

theorem tracialWordRepeatedOperator_adjoint (n : ℕ) :
    G.tracialWordRepeatedOperator A D M S hsize U Y.adjoint n =
      (G.tracialWordRepeatedOperator A D M S hsize U Y n).adjoint :=
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracial_repeated_word line 124
Source documentation
Every repeated-letter word transforms by the canonical bounded multiplicity operator; its action is independent of the repeated letter.
```
theorem tracial_repeated_word (n : ℕ) (a : WordMultiplicity (G.baseVector A 1) n)
    (d : G.baseSpace D) (r : centeredSubspace (G.baseVector D 1)) :
    Y (U.inclusion n (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r)))) =
      U.inclusion n (hilbertTensorInsert
        (G.tracialWordRepeatedOperator A D M S hsize U Y n a)
        (endpointWord d (fun _ : Fin n => r))) :=
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord

theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracial_adjoint_repeated_word line 141

Source documentation

The adjoint transforms by the adjoint of the same canonical coefficient.

theorem tracial_adjoint_repeated_word (n : ℕ) (a : WordMultiplicity (G.baseVector A 1) n)
    (d : G.baseSpace D) (r : centeredSubspace (G.baseVector D 1)) :
    Y.adjoint (U.inclusion n (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r)))) =
      U.inclusion n (hilbertTensorInsert
        ((G.tracialWordRepeatedOperator A D M S hsize U Y n).adjoint a)
        (endpointWord d (fun _ : Fin n => r))) :=
…

Mentions: OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord