# Trace cones and Razak–Jacelon stabilization

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

- [The trace cone classifies Razak–Jacelon stabilizations](../../preprints/The-trace-cone-classifies-Razak-Jacelon-stabilizations-September-25-2026/The-trace-cone-classifies-Razak-Jacelon-stabilizations-September-25-2026.pdf)

## Scope

The paper classifies separable nuclear complex $C^*$-algebras after tensoring with the Razak–Jacelon algebra and the compact operators, using their cones of extended lower-semicontinuous traces. The linked formalization proves the ideal-transport part: a trace-cone equivalence induces an order isomorphism of closed two-sided ideals, carrying the ideals determined by finiteness and vanishing of each trace to those of its image.

For each closed ideal $I$, it also constructs the trace that is zero on positive elements of $I$ and infinite elsewhere. These traces are exactly the additive idempotents, meaning $\tau+\tau=\tau$, and their addition recovers ideal inclusion. Spatial classification, existence of the stabilization models, norm uniqueness, and final intertwining are outside this supporting comparison.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Transport of trace ideals and their additive-idempotent description | [TraceIdealTransportSupport.lean](../ComparatorChallenges/TraceIdealTransportSupport.lean) |