OAI/Analysis/KadisonKastler/StrongStability.lean

Strong Kadison–Kastler stability

The theorem KadisonKastler.universal_strong_stability gives one positive tolerance for all complex Hilbert spaces and represented unital von Neumann algebras, in terms of the desired displacement of a conjugating unitary.

The proof combines finite-factor estimates, modular preparation, regular-core descent, two-ratio product absorption, and reduction to arbitrary representations. State homogeneity of the product follows from a uniform projection-gap contraction and positive representatives. Its expected matrix subfactor is constructed in the original representation.