# Strong Kadison–Kastler stability and its spatial boundaries

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Universal strong Kadison–Kastler stability](../../preprints/Universal-strong-Kadison-Kastler-stability-September-23-2026/paper.pdf)

## Scope

The formalization proves the strong Kadison–Kastler conjecture uniformly. For every $\varepsilon>0$, there is a $\delta>0$ such that any two unital von Neumann algebras on the same complex Hilbert space at Kadison–Kastler distance below $\delta$ are conjugate by a unitary $u$ with $\lVert u-1\rVert<\varepsilon$. The tolerance depends only on $\varepsilon$, uniformly over the algebras, their representations, and the Hilbert space.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Universal near-identity unitary conjugacy for close von Neumann algebras | [StrongKadisonKastler.lean](../ComparatorChallenges/StrongKadisonKastler.lean) |