HomogeneityStability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Universal strong stability from faithful-state homogeneity alone

The concrete two-ratio product has a scalar bicentralizer and an expected matrix subfactor in every required representation. Faithful-state homogeneity supplies the state comparisons needed for the stability bound.

theorem OAI.KadisonKastler.constructedStabilityCoreInputs line 18
Source documentation
Modular core estimates independent of expected subfactors.
```
theorem constructedStabilityCoreInputs : ModularCorePublishedInputs.{u} := {
…
```
theorem OAI.KadisonKastler.universal_strong_stability_of_state_homogeneity line 37
Source documentation
Connes--Størmer faithful-state homogeneity implies universal strong stability, with one tolerance for all algebras and represented Hilbert spaces.
```
theorem universal_strong_stability_of_state_homogeneity
    (hhom : PublishedTypeIII1StateHomogeneity.{u}) : UniversalStrongStability.{u} := by
…
```