# Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stability

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

- [Tracial projection methods and uniform property $\Gamma$](../../preprints/Tracial-projection-methods-and-uniform-property-Gamma-September-23-2026/paper.pdf)

## Scope

The formalization proves that real rank zero of the uniform tracial ultrapower of the uniform tracial completion implies uniform property $\Gamma$ for a simple separable unital infinite-dimensional nuclear stably finite $C^*$-algebra with traces. The conclusion holds at every specified free ultrafilter under the corresponding real-rank-zero hypothesis.

The linked comparison results also prove Jiang–Su absorption and uniform property $\Gamma$ for simple separable unital infinite-dimensional nuclear algebras with strict comparison, and for the stated stably projectionless nuclear algebras with bounded densely finite traces, a nonempty compact normalized trace base, and the prescribed finite-target-rank comparison condition.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Uniform property $\Gamma$ from tracial real rank zero | [UniformGamma.lean](../ComparatorChallenges/UniformGamma.lean) |