TwoRatioPointedConstruction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The concrete pointed product for the two fixed ratios

The constant matrix-state products are placed in the two spatial tensor legs. Their finite moments, cyclicity and separation give the exact two-family coordinate system used by the application. Its finite stages include remote copies and finite complements.

def OAI.KadisonKastler.twoRatioPointedProduct line 25
Source documentation
The two prescribed site families with their actual product-state representation.
```
def twoRatioPointedProduct : PointedMatrixProduct.{u} twoRatioSiteParameter := by
…
```
Mentions: OAI.KadisonKastler.twoRatioSiteParameter
def OAI.KadisonKastler.twoRatioConcreteStages line 36
Source documentation
Increasing full matrix stages with the required remote-copy moments.
```
def twoRatioConcreteStages : ProductMatrixStages (H := twoRatioPointedProduct.{u}.K) :=
…
```
Mentions: OAI.KadisonKastler.ProductMatrixStages
def OAI.KadisonKastler.twoRatioConcreteCoordinates line 40
Source documentation
The original site coordinates generate the constructed stage closure.
```
def twoRatioConcreteCoordinates : PointedMatrixSites twoRatioConcreteStages.{u}.algebra
    twoRatioConcreteStages.vector twoRatioSiteParameter :=
…
```
Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.twoRatioSiteParameter