PointedMatrixProduct.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite moments below identify the actual matrix-state product. They do not include any assertion about factor type, centralizers or absorption.

structure OAI.KadisonKastler.PointedMatrixSites line 25
Source documentation
A coordinate description of the product of two-dimensional matrix states. Only distinct-site moments are needed: repeated entries at a site are reduced by the matrix-unit identities.
```
structure PointedMatrixSites {I : Type*} (M : VonNeumannAlgebra H) (Ω : H) (ν : I → ℝ) where
…
```
structure OAI.KadisonKastler.PointedMatrixProduct line 40
Source documentation
A concrete pointed matrix product in its faithful product-state representation. This is construction data, not a classification.
```
structure PointedMatrixProduct {I : Type} (ν : I → ℝ) where
…
```