InvariantIntertwiners.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Matrix realization of the invariant-intertwiner argument

Finite coefficient forms are constructed from explicit Hilbert-space matrix realizations. Normalized Hilbert--Schmidt inner products supply the matrix-unit norms, while left matrix actions supply endpoint transfer. The sole invariant theory input remains finite-dimensional Schur--Weyl spanning.

structure OAI.KadisonSimilarity.MatrixHilbertStage line 28
Source documentation
Local geometric data of one full matrix stage in a tracial Hilbert space. The maps and identities describe its normalized Hilbert--Schmidt realization; no coefficient expansion or intertwiner classification is included.
```
structure MatrixHilbertStage where
…
```
theorem OAI.KadisonSimilarity.tensorMatrixUnit_eq_single line 39
theorem OAI.KadisonSimilarity.star_tensorMatrixUnit line 46
theorem OAI.KadisonSimilarity.tensorMatrixUnit_mul line 53
theorem OAI.KadisonSimilarity.trace_tensorMatrixUnit line 57
theorem OAI.KadisonSimilarity.MatrixHilbertStage.norm_full_matrixUnit line 62
Source documentation
Every realized matrix unit has the normalized Hilbert--Schmidt norm.
```
theorem MatrixHilbertStage.norm_full_matrixUnit [Nonempty α]
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) (a b : α) :
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
theorem OAI.KadisonSimilarity.MatrixHilbertStage.norm_center_matrixUnit_le line 76
Source documentation
Centering is contractive on the normalized matrix units.
```
theorem MatrixHilbertStage.norm_center_matrixUnit_le [Nonempty α]
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) (a b : α) :
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
def OAI.KadisonSimilarity.MatrixHilbertStage.testEndpoint line 82
Source documentation
The test endpoint map is conjugate-linear because matrix star is.
```
def MatrixHilbertStage.testEndpoint
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) : Matrix α α ℂ →ₗ⋆[ℂ] E :=
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
def OAI.KadisonSimilarity.MatrixHilbertStage.testLetter line 86
def OAI.KadisonSimilarity.MatrixHilbertStage.form line 92
theorem OAI.KadisonSimilarity.MatrixHilbertStage.form_apply line 99
theorem OAI.KadisonSimilarity.MatrixHilbertStage.form_invariant_of_word_covariance line 110
Source documentation
Isometric word covariance gives precisely the finite conjugation invariance required by Schur--Weyl, with no invariance of the coefficient form assumed.
```
theorem MatrixHilbertStage.form_invariant_of_word_covariance
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) (J : F →ₗᵢ⋆[ℂ] F)
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
theorem OAI.KadisonSimilarity.MatrixHilbertStage.form_matrixUnit_bound line 135
Source documentation
The matrix-unit endpoint estimate follows from the actual left matrix projection and normalized Hilbert--Schmidt norms.
```
theorem MatrixHilbertStage.form_matrixUnit_bound [Nonempty α]
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) (J : F →ₗᵢ⋆[ℂ] F)
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
structure OAI.KadisonSimilarity.MatrixWordCovariance line 190
Source documentation
Isometric simultaneous-conjugation covariance on source and test words. These are local actions on the realized tensor words, not coefficient formulas.
```
structure MatrixWordCovariance
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) (J : F →ₗᵢ⋆[ℂ] F)
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
theorem OAI.KadisonSimilarity.MatrixWordCovariance.form_invariant line 206
theorem OAI.KadisonSimilarity.MatrixHilbertStage.form_compatible line 218
Source documentation
The coefficient forms agree under an inclusion agreeing on the full and centered Hilbert realizations. Star compatibility is supplied by the actual matrix star-algebra inclusion.
```
theorem MatrixHilbertStage.form_compatible
    (R : MatrixHilbertStage (E := E) (F := F) (α := α))
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
theorem OAI.KadisonSimilarity.MatrixHilbertStage.endpoint_pairing_of_form line 232
Source documentation
Moving a general source endpoint across the intertwiner turns the endpoint trace into the full Hilbert inner product. The centered matrix pairing is the ordinary normalized trace pairing on this local stage.
```
theorem MatrixHilbertStage.endpoint_pairing_of_form
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) (J : F →ₗᵢ⋆[ℂ] F)
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
theorem OAI.KadisonSimilarity.exists_realized_matrix_pairing_expansion line 287
Source documentation
Assemble the actual stage forms, their covariance, their left-matrix test estimate, and the finite invariant theory. The only published assumption is spanning; every other premise is explicit local realization data.
```
theorem exists_realized_matrix_pairing_expansion
    (R : ∀ s, MatrixHilbertStage (E := E) (F := F) (α := A s))
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage