PublishedTwoRatioProduct.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The pointed infinite-product construction used by the application

Blackadar, Operator Algebras, III.3.1.1--3 (pp.293--295), constructs the countable pointed tensor product from the finite-site algebras and product states. For faithful matrix states the local left and right orbits are dense. Disjoint finite blocks have product matrix moments; an unused block with the same site types gives RemoteProductBlock.

The site modular action is conjugation by the diagonal density matrix, and the modular operator of the product is the tensor product of the site operators: III.4.4.7--9 and III.4.5.8 (pp.316--319). Only the two off-diagonal eigenoperators are retained below. No centralizer or core factoriality, type classification, absorption, or stability is assumed.

structure OAI.KadisonKastler.TwoRatioProductModel line 32
Source documentation
Concrete construction data for countably many sites of each of the two fixed matrix-state types. Finite complement moments, rather than irreducibility, are the retained input.
```
structure TwoRatioProductModel where
…
```
def OAI.KadisonKastler.PublishedTwoRatioProduct line 57
Source documentation
Published pointed-product and modular tensor construction, restricted to the concrete data above.
```
def PublishedTwoRatioProduct : Prop := Nonempty TwoRatioProductModel.{u}
…
```