# The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability

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

- [The Kirchberg–Rørdam character criterion](../../preprints/The-Kirchberg-Rordam-character-criterion-September-25-2026/paper.pdf)

## Scope

The Kirchberg–Rørdam criterion relates Jiang–Su absorption to characters of the central-sequence algebra. The formalized result proves that, for every nonzero unital separable complex $C^*$-algebra $A$ and every free ultrafilter on $\mathbb N$, the norm central-sequence algebra has no nonzero character exactly when $A\cong A\otimes_{\min}\mathcal Z$. No nuclearity, simplicity, trace, or comparison hypothesis is imposed.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Kirchberg–Rørdam character criterion | [CharacterCriterion.lean](../ComparatorChallenges/CharacterCriterion.lean) |