TracialMatrixTower.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Tracial matrix towers from actual embedded matrix algebras

The matrix-stage geometry is constructed from nested trace-preserving matrix embeddings in a tracial Hilbert representation. Density of centered trace-zero stages is derived by orthogonal projection from density of the full stages.

structure OAI.KadisonSimilarity.NestedTracialMatrices line 26
Source documentation
Raw nested matrix embeddings, with density stated for their represented algebra vectors. No Hilbert coefficient identity is part of this data.
```
structure NestedTracialMatrices (τ : R →ₗ[ℂ] ℂ) (V : R →ₗ[ℂ] E) where
…
```
structure OAI.KadisonSimilarity.RealTracialSequence line 36
Source documentation
A real orthonormal sequence expressed entirely in the tracial algebra. Its Hilbert realization is derived below.
```
structure RealTracialSequence (τ : R →ₗ[ℂ] ℂ) where
…
```
theorem OAI.KadisonSimilarity.NestedTracialMatrices.denseRange_vector line 51
Source documentation
Density of the matrix union already implies density of the represented algebra, so no separate cyclic-density assumption is needed by the tower.
```
theorem NestedTracialMatrices.denseRange_vector : DenseRange V := by
…
```
theorem OAI.KadisonSimilarity.NestedTracialMatrices.trace_one line 61
Source documentation
A unital trace-preserving nonempty matrix stage normalizes the ambient trace automatically.
```
theorem NestedTracialMatrices.trace_one : τ 1 = 1 := by
…
```
def OAI.KadisonSimilarity.embeddedMatrixStage line 66
Source documentation
The stage of a nested embedded matrix algebra.
```
def embeddedMatrixStage (s : ℕ) :
    MatrixHilbertStage (E := E) (F := centeredSubspace (V 1)) (α := A s) :=
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage, OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.embeddedMatrixStage_full line 71
theorem OAI.KadisonSimilarity.embeddedMatrixStage_center line 75
theorem OAI.KadisonSimilarity.embeddedMatrixStage_full_mono line 80
theorem OAI.KadisonSimilarity.NestedTracialMatrices.trace_zero_inclusion line 90
Source documentation
Trace preservation forces every compatible matrix inclusion to preserve trace-zero matrices, regardless of the change in matrix size.
```
theorem NestedTracialMatrices.trace_zero_inclusion (s t : ℕ) (h : s ≤ t)
    (a : Matrix (A s) (A s) ℂ) (ha : Matrix.trace a = 0) :
    Matrix.trace (M.inclusion s t h a) = 0 := by
…
```
theorem OAI.KadisonSimilarity.embeddedMatrixStage_center_mono line 99

theorem OAI.KadisonSimilarity.embeddedMatrixStage_center_trace_zero line 109

Source documentation

Any centered matrix vector is represented by a trace-zero matrix in the same stage.

theorem embeddedMatrixStage_center_trace_zero (s : ℕ) (a : Matrix (A s) (A s) ℂ) :
    ∃ b : Matrix (A s) (A s) ℂ, Matrix.trace b = 0 ∧
      (embeddedMatrixStage τ V L hinner hleft M s).center b =
        (embeddedMatrixStage τ V L hinner hleft M s).center a := by
…

Mentions: OAI.KadisonSimilarity.embeddedMatrixStage

theorem OAI.KadisonSimilarity.embeddedMatrixStage_center_dense line 127
Source documentation
Centered-stage density follows from full-stage density and the actual orthogonal projection; it is not an extra tower hypothesis.
```
theorem embeddedMatrixStage_center_dense :
    Dense (⋃ s, centeredMatrixStage (embeddedMatrixStage τ V L hinner hleft M) s) := by
…
```
Mentions: OAI.KadisonSimilarity.centeredMatrixStage, OAI.KadisonSimilarity.embeddedMatrixStage
def OAI.KadisonSimilarity.realTracialHilbertSequence line 146
Source documentation
Real algebra vectors give the actual fixed orthonormal sequence in the centered tracial Hilbert space.
```
def realTracialHilbertSequence (n : ℕ) : centeredSubspace (V 1) :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.coe_realTracialHilbertSequence line 151
theorem OAI.KadisonSimilarity.realTracialHilbertSequence_orthonormal line 157
theorem OAI.KadisonSimilarity.realTracialHilbertSequence_fixed line 166
def OAI.KadisonSimilarity.tracialMatrixTowerOfEmbeddings line 178
Source documentation
Every scalar geometric field of the invariant-theory tower is now derived from the actual tracial representation and raw matrix embeddings. The only remaining sequence data is an algebraic real orthonormal sequence.
```
def tracialMatrixTowerOfEmbeddings
    (hsize : Filter.Tendsto (fun s => (Fintype.card (A s) : ℝ)) Filter.atTop Filter.atTop) :
    TracialMatrixTower (E := E) (F := centeredSubspace (V 1)) (A := A) where
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower, OAI.KadisonSimilarity.centeredSubspace