# Weak pure infiniteness and Cuntz-algebra absorption

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

- [Weak pure infiniteness and $\mathcal O_\infty$ absorption](../../preprints/Weak-pure-infiniteness-and-O-infinity-absorption-September-25-2026/paper.pdf)

## Scope

The formalization proves that a complex $C^*$-algebra in which every positive element is properly infinite is strongly purely infinite, with the full positive-element diagonalization property. No exactness, nuclearity, unitality, or simplicity assumption is needed for this implication.

For exact algebras, proper infiniteness of one fixed finite amplification of every positive element already implies individual proper infiniteness and strong pure infiniteness.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Fixed-amplification pure infiniteness for exact algebras | [ExactInfiniteness.lean](../ComparatorChallenges/ExactInfiniteness.lean) |
| Individual proper infiniteness implies strong pure infiniteness | [IndividualStrongInfiniteness.lean](../ComparatorChallenges/IndividualStrongInfiniteness.lean) |