ProductMatrixStages.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Deriving the product-state argument from finite matrix data

A remote copy of a finite tensor block has identical matrix moments. Every other finite block embeds in the product of these two blocks and a finite complement. These are finite tensor-product statements; no centralizer irreducibility or crossed-product conclusion is assumed.

structure OAI.KadisonKastler.RemoteProductBlock line 25
Source documentation
Finite data obtained by moving a block to unused sites of the same types. Complements witness the product formula on every finite stage.
```
structure RemoteProductBlock (s : ℕ → ℕ)
    (E : ∀ n, MatrixUnitSystem (Fin (s n)) (H →L[ℂ] H)) (Ω : H) (k n : ℕ) where
…
```
structure OAI.KadisonKastler.ProductMatrixStages line 45
Source documentation
An increasing sequence of finite product matrix algebras, in its cyclic separating product representation. This describes the construction data rather than any of its centralizer or factor consequences.
```
structure ProductMatrixStages where
…
```
def OAI.KadisonKastler.ProductMatrixStages.algebra line 61
theorem OAI.KadisonKastler.ProductMatrixStages.local_le line 64
def OAI.KadisonKastler.ProductMatrixStages.localSwaps line 71
Source documentation
The actual finite swap is assembled from the two matrix systems. Triple product moments put it in the centralizer of the full algebra.
```
def localSwaps : LocalProductSwaps P.algebra P.vector where
…
```
Mentions: OAI.KadisonKastler.LocalProductSwaps

theorem OAI.KadisonKastler.ProductMatrixStages.state_centralizer_irreducible line 97

Source documentation

The finite-product construction implies the irreducibility of its state centralizer.

theorem state_centralizer_irreducible (x : H →L[ℂ] H) (hx : x ∈ P.algebra)
    (hc : ∀ u : unitary (H →L[ℂ] H), (u : H →L[ℂ] H) ∈ P.algebra →
      ProductStateCentralizes P.algebra P.vector u → (u : H →L[ℂ] H) * x = x * u) :
    x = productVectorState P.vector x • (1 : H →L[ℂ] H) :=
…

Mentions: OAI.KadisonKastler.ProductStateCentralizes, OAI.KadisonKastler.productVectorState

theorem OAI.KadisonKastler.ProductMatrixStages.scalarCenter line 103