# The ℓ¹-Bass conjecture for all discrete groups

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

- [The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture](../../preprints/The-Bass-trace-conjecture-for-complex-group-rings-September-24-2026/The-Bass-trace-conjecture-for-complex-group-rings-September-24-2026.pdf)

## Scope

The formalization proves the complex Bass trace conjecture for every group: the Hattori–Stallings trace of each virtual class of finitely generated projective right $\mathbb C[G]$-modules vanishes on conjugacy classes of infinite-order elements. No finiteness, countability, or geometric hypothesis on $G$ is imposed.

For torsion-free $G$, it identifies the trace on $K_0(\mathbb C[G])$ with the integral augmentation rank and proves the characteristic-zero Kaplansky idempotent conjecture: for every commutative unital domain $R$ of characteristic zero, an idempotent in $R[G]$ is $0$ or $1$.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Complex Bass trace vanishing and support | [BassTrace.lean](../ComparatorChallenges/BassTrace.lean) |
| Trace rank and characteristic-zero Kaplansky idempotents for torsion-free groups | [BassTorsionFree.lean](../ComparatorChallenges/BassTorsionFree.lean) |