TwoRatioProductType.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The type III₁ conclusion for the fixed two-ratio product

The local finite-product data supply centralizer irreducibility. The two site eigenoperators then force the regular core to be a factor, before the published core-classification theorem is applied.

theorem OAI.KadisonKastler.ProductMatrixStages.tensor_typeIII1 line 33
Source documentation
All factorial-core conclusions are derived from finite product data and the two explicit site eigenoperators. The given modular resolution is certified by its bounded KMS strip condition.
```
theorem ProductMatrixStages.tensor_typeIII1
    (P : ProductMatrixStages (H := K))
…
```
Mentions: OAI.KadisonKastler.ProductMatrixStages