WordBaseCoordinates.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Identify the degree-zero multiplicity operator with the actual compression to the base algebra's tracial Hilbert space.

def OAI.KadisonSimilarity.emptyEndpoint line 21
Source documentation
The first endpoint with no centered tail letters.
```
def emptyEndpoint (Ω : E) : EndpointTensor E F 0 :=
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor
theorem OAI.KadisonSimilarity.norm_emptyEndpoint line 24
def OAI.KadisonSimilarity.baseWordInclusion line 33
Source documentation
The base Hilbert space embeds as the scalar first endpoint in degree zero.
```
def baseWordInclusion : B →ₗᵢ[ℂ] H where
…
```
theorem OAI.KadisonSimilarity.baseWordInclusion_apply line 44
theorem OAI.KadisonSimilarity.baseWordInclusion_intertwines line 51
Source documentation
The degree-zero repeated-word identity determines the base operator.
```
theorem baseWordInclusion_intertwines (Y : H →L[ℂ] H)
    (T : WordMultiplicity ΩA 0 →L[ℂ] WordMultiplicity ΩA 0)
    (hY : ∀ v, Y (U.inclusion 0 (hilbertTensorInsert v (emptyEndpoint (F := F) ΩD))) =
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.emptyEndpoint
theorem OAI.KadisonSimilarity.baseWordInclusion_compression line 68
Source documentation
Compressing to the base-word inclusion recovers precisely the transported canonical degree-zero operator.
```
theorem baseWordInclusion_compression (Y : H →L[ℂ] H)
    (T : WordMultiplicity ΩA 0 →L[ℂ] WordMultiplicity ΩA 0)
    (hY : ∀ v, Y (U.inclusion 0 (hilbertTensorInsert v (emptyEndpoint (F := F) ΩD))) =
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.emptyEndpoint
theorem OAI.KadisonSimilarity.baseWordInclusion_eq_baseInclusion line 87
Source documentation
Equality on algebra vectors identifies the abstract degree-zero inclusion with the actual closed base subspace. The extension follows from density.
```
theorem baseWordInclusion_eq_baseInclusion
    (hword : ∀ a : A,
      baseWordInclusion (G.baseVector A 1) U ΩD hΩD (G.baseVector A a) = G.vector (a : P)) :
    baseWordInclusion (G.baseVector A 1) U ΩD hΩD = G.baseInclusion A := by
…
```
Mentions: OAI.KadisonSimilarity.baseWordInclusion

theorem OAI.KadisonSimilarity.baseOperator_eq_zeroMultiplicityOperator line 97

Source documentation

The degree-zero operator is the actual tracial compression, rather than an unrelated multiplicity coefficient.

theorem baseOperator_eq_zeroMultiplicityOperator (Y : H →L[ℂ] H)
    (T : WordMultiplicity (G.baseVector A 1) 0 →L[ℂ] WordMultiplicity (G.baseVector A 1) 0)
    (hword : ∀ a : A,
      baseWordInclusion (G.baseVector A 1) U ΩD hΩD (G.baseVector A a) = G.vector (a : P))
    (hY : ∀ v, Y (U.inclusion 0 (hilbertTensorInsert v (emptyEndpoint (F := F) ΩD))) =
…

Mentions: OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.baseWordInclusion, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.emptyEndpoint