# Kaplansky's quasitrace conjecture and failure of tensor-product stable finiteness

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

- [A counterexample to Kaplansky's quasitrace conjecture and failure of tensor-product stable finiteness](../../preprints/A-counterexample-to-Kaplanskys-quasitrace-conjecture-September-23-2026/paper.pdf)

## Scope

Kaplansky's quasitrace conjecture predicts that every $2$-quasitrace on a $C^*$-algebra is a trace. The formalization constructs a separable $C^*$-algebra with normalized $2$-quasitraces and fixed positive contractions $a,b$ for which every such quasitrace satisfies $\mathrm{Re}(\tau(a+b)-\tau(a)-\tau(b))\ge1/144$. Thus none is additive on this pair.

The formalization also gives simple stably finite $C^*$-algebras whose spatial tensor product is properly infinite, a separable stably finite algebra with no tracial state, and a tensor-product example in which normalized $2$-quasitraces are lost. These are the stable-finiteness consequences named in the paper's title.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Nonadditive normalized $2$-quasitraces | [KaplanskyQuasitrace.lean](../ComparatorChallenges/KaplanskyQuasitrace.lean) |
| Tensor-product failure of stable finiteness and quasitrace consequences | [KaplanskyStableFiniteness.lean](../ComparatorChallenges/KaplanskyStableFiniteness.lean) |