EndpointClassification.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Completed invariant intertwiners from matrix-stage geometry

Finite-dimensional Schur--Weyl spanning is the only invariant-theory input. The remaining assumptions describe a nested dense tracial matrix realization, its conjugation, and the operator's actual left and conjugation intertwinings. The coefficient identity and completed permutation classification are derived.

def OAI.KadisonSimilarity.fullMatrixStage line 25
def OAI.KadisonSimilarity.centeredMatrixStage line 28
structure OAI.KadisonSimilarity.TracialMatrixTower line 33
Source documentation
Local tracial realization data for the nested matrix stages. In particular, there is no invariant coefficient formula or intertwiner classification here.
```
structure TracialMatrixTower where
…
```
theorem OAI.KadisonSimilarity.exists_endpoint_pairing_expansion_of_schurWeyl line 64
Source documentation
The full completed coefficient formula is derived from stage geometry, left intertwining, and finite Schur--Weyl, rather than assumed.
```
theorem exists_endpoint_pairing_expansion_of_schurWeyl
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower

theorem OAI.KadisonSimilarity.endpoint_reconstruct_from_pairing line 100

Source documentation

A full endpoint pairing formula reconstructs the identity on the endpoint factor and the compression to the normalized trace vector.

theorem endpoint_reconstruct_from_pairing
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l)
    (Ω : E) (hΩ : ‖Ω‖ = 1) (J : F → F) (hJJ : Function.Involutive J)
    (B : F →L[ℂ] F →L[ℂ] ℂ) (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
    (hfull : ∀ d a v,
      inner ℂ (endpointWord a (fun j => J (v (.inr j))))
        (Y (endpointWord d (fun i => v (.inl i)))) =
      inner ℂ a d * ∑ P, c P * pairingPolynomial sourceFirstRank B P v) :
    Y = endpointAmplification (endpointCompression Ω Y) ∧
      (∀ v, tracialWordCoefficient (endpointCompression Ω Y) J v =
        ∑ P, c P * pairingPolynomial sourceFirstRank B P v) := by
…

Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.pairingPolynomial, OAI.KadisonSimilarity.sourceFirstRank, OAI.KadisonSimilarity.endpointAmplification, OAI.KadisonSimilarity.endpointCompression, OAI.KadisonSimilarity.tracialWordCoefficient

theorem OAI.KadisonSimilarity.endpoint_zero_from_pairing line 129

Source documentation

Unequal degrees force the full endpoint operator to vanish.

theorem endpoint_zero_from_pairing
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l)
    (Ω : E) (hΩ : ‖Ω‖ = 1) (J : F → F) (hJ : Continuous J)
    (hJJ : Function.Involutive J) (B : F →L[ℂ] F →L[ℂ] ℂ)
    (hB : ∀ x y, B x (J y) = inner ℂ y x)
    (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
    (h : ℕ → F) (hh : Orthonormal ℂ h) (hfix : ∀ m, J (h m) = h m)
    (hfull : ∀ d a v,
      inner ℂ (endpointWord a (fun j => J (v (.inr j))))
        (Y (endpointWord d (fun i => v (.inl i)))) =
      inner ℂ a d * ∑ P, c P * pairingPolynomial sourceFirstRank B P v)
    (hkl : k ≠ l) : Y = 0 := by
…

theorem OAI.KadisonSimilarity.endpoint_permutations_from_pairing line 159

Source documentation

Equal degrees give an actual finite sum of position permutations, with identity on the unrestricted endpoint.

theorem endpoint_permutations_from_pairing {n : ℕ}
    (Y : EndpointTensor E F n →L[ℂ] EndpointTensor E F n)
    (Ω : E) (hΩ : ‖Ω‖ = 1) (J : F → F) (hJ : Continuous J)
    (hJJ : Function.Involutive J) (B : F →L[ℂ] F →L[ℂ] ℂ)
    (hB : ∀ x y, B x (J y) = inner ℂ y x)
    (c : PerfectMatching (Fin n ⊕ Fin n) → ℂ)
    (h : ℕ → F) (hh : Orthonormal ℂ h) (hfix : ∀ m, J (h m) = h m)
    (hfull : ∀ d a v,
      inner ℂ (endpointWord a (fun j => J (v (.inr j))))
        (Y (endpointWord d (fun i => v (.inl i)))) =
      inner ℂ a d * ∑ P, c P * pairingPolynomial sourceFirstRank B P v) :
    Y = endpointAmplification (crossPairingOperator c) := by
…

theorem OAI.KadisonSimilarity.endpoint_intertwiner_zero_of_schurWeyl line 180
Source documentation
The unequal-degree invariant-intertwiner theorem, conditional only on finite Schur--Weyl and explicit tracial matrix realization data.
```
theorem endpoint_intertwiner_zero_of_schurWeyl
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower
theorem OAI.KadisonSimilarity.endpoint_intertwiner_permutations_of_schurWeyl line 200
Source documentation
The equal-degree invariant-intertwiner theorem on the completed endpoint Hilbert tensor space; the coefficient expansion is a proved conclusion.
```
theorem endpoint_intertwiner_permutations_of_schurWeyl {n : ℕ}
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower