∑math20

Operator algebras · Result 301

Trace cones and Razak–Jacelon stabilization

1 paperLean

Classifies separable nuclear complex C∗-algebras after tensoring with the Razak–Jacelon algebra and the compact operators, using their full topological cones of extended lower-semicontinuous tracial weights. This answers Robert’s trace-cone question, including algebras with arbitrary ideal structure and both finite and infinite subquotients.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of The trace cone classifies Razak–Jacelon stabilizations

The trace cone classifies Razak–Jacelon stabilizations

OpenAI · September 25, 2026

We prove that the canonical topological cone of all extended lower-semicontinuous tracial weights determines a separable nuclear C∗-algebra after tensoring with the Razak–Jacelon algebra and the compact operators, answering Robert's trace-cone classification question positively. The isomorphism realizes the prescribed cone map, with arbitrary ideal structure and without a density assumption on the finite domains of the weights.

Read PDF Download Source

Cite
@misc{OAI:The-trace-cone-classifies-Razak-Jacelon-stabilizations-September-25-2026,
  author = {{OpenAI}},
  title = {{The trace cone classifies Razak--Jacelon stabilizations}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-trace-cone-classifies-Razak-Jacelon-stabilizations-September-25-2026/The-trace-cone-classifies-Razak-Jacelon-stabilizations-September-25-2026.pdf}{OAI:The-trace-cone-classifies-Razak-Jacelon-stabilizations-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

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

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

ResultComparator statement
Transport of trace ideals and their additive-idempotent descriptionTraceIdealTransportSupport.lean

Scope note on GitHub →