we-solve (beta)

Math-2820 · mathematics · Analysis

Individual and strong pure infiniteness

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
If every positive element of a complex C*-algebra is properly infinite in Cuntz comparison, must the algebra be strongly purely infinite, with simultaneous two-element diagonalization, without exactness, nuclearity, unitality or simplicity assumptions?

Short English statement

If every positive element of a complex C*-algebra is properly infinite in Cuntz comparison, must the algebra be strongly purely infinite, with simultaneous two-element diagonalization, without exactness, nuclearity, unitality or simplicity assumptions?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2820-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2820

Manuscript 1 (family 303, 2026-09-25): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed proof of that assertion in full.

Individual and strong pure infiniteness

OpenAI's claim

Proper infiniteness of all positive elements is claimed to imply strong pure infiniteness; under exactness a uniform finite-amplification version suffices, and separable nuclear algebras with that property absorb O_infinity. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
For an exact complex $C^*$-algebra $C$, assume one fixed $n\ge1$ makes every amplified positive element $h^{\oplus n}$ properly infinite, meaning $h^{\oplus n}\oplus h^{\oplus n}\precsim h^{\oplus n}$ in Cuntz comparison. OpenAI claims every positive $h\in C$ is itself properly infinite and $C$ is strongly purely infinite. Its other theorem omits exactness but assumes every positive element already properly infinite. For all $a,b\ge0$, arbitrary $c\in C$ and $\varepsilon>0$, it claims $s,t\in C$ with \[ \|s^*as-a\|<\varepsilon,\qquad\|t^*bt-b\|<\varepsilon,\qquad\|s^*ct\|<\varepsilon. \] These are simultaneous diagonalization inequalities, not only individual positive-element comparison.

Outline of the argument

Manuscript 1 (family 303, 2026-09-25): Graph shrinking and polar deformation merge hereditary positive elements while retaining norm signals in all required quotients. Exactness rules out persistent amplification obstructions, while a separate nuclear argument uses matrix norms forbidden in exact targets. Controlled comparison coefficients then eliminate arbitrary mixed entries, establishing strong diagonalization and the central-sequence absorption conclusion.

Formal verification

For family 303, the scope page documents the following selections. One selection derives strong pure infiniteness directly from proper infiniteness of each positive element. The fixed-amplification variant assumes exactness; no general absorption conclusion is selected without its additional hypotheses. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: ExactInfiniteness.lean, IndividualStrongInfiniteness.lean. Declarations: OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_individuallyProperlyInfinite_any, OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_stronglyPurelyInfinite, OAI.MainGap.Manuscript.individual_to_strong_main.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

Go to contribution →