we-solve (beta)

Math-2818 · mathematics · Analysis

Removing a fixed amplification in exact C*-algebras

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
If C is an exact complex C*-algebra and one fixed integer $n\geq 1$ makes $h^{\oplus n}$ properly infinite for every $h\in C_+$, must each h itself be properly infinite and C strongly purely infinite? Consequently, in the separable nuclear setting does this fixed-amplification hypothesis imply absorption of $O\infty $?

Short English statement

If C is an exact complex C*-algebra and one fixed integer $n\geq 1$ makes $h^{\oplus n}$ properly infinite for every $h\in C_+$, must each h itself be properly infinite and C strongly purely infinite? Consequently, in the separable nuclear setting does this fixed-amplification hypothesis imply absorption of $O\infty $?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2818

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.

Removing a fixed amplification in exact C*-algebras

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. It does not establish formal coverage of the complete problem clause. 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 →