we-solve (beta)

Math-2392-A1 · revision r1 · on Math-2392

OpenAI claim summary for Math-2392

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: partially solved. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

Manuscript 1 (family 291, 2026-09-23): The strict-comparison/Jiang–Su/nuclear-dimension claims do not settle the additional finite-decomposition-rank equivalence for all stably finite algebras requested by this record.

Manuscript 2 (family 291, 2026-09-23): The strict-comparison/Jiang–Su/nuclear-dimension claims do not settle the additional finite-decomposition-rank equivalence for all stably finite algebras requested by this record.

Manuscript 3 (family 291, 2026-09-23): The strict-comparison/Jiang–Su/nuclear-dimension claims do not settle the additional finite-decomposition-rank equivalence for all stably finite algebras requested by this record.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Regularity Properties of Nuclear \$C^*\$-Algebras
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Mathematical claim 2.
  6. Mathematical claim 3.
  7. Outline of the argument
  8. Formal verification
  9. Status caveat
  10. Sources

Regularity Properties of Nuclear \$C^*\$-Algebras

OpenAI's claim

Manuscript 1 (family 291, 2026-09-23): A separable nuclear C*-algebra that is simple and non-elementary is claimed to absorb Jiang--Su under extended-functional strict comparison, including nonunital and unbounded-trace cases; semigroup divisibility also yields a nonsimple criterion. Manuscript 2 (family 291, 2026-09-23): Finite nuclear dimension is claimed to characterize Jiang--Su stability for separable nuclear algebras lacking elementary ideal subquotients; moreover, Jiang--Su stabilization always lowers nuclear dimension to at most one. Manuscript 3 (family 291, 2026-09-23): The paper claims uniform Gamma from real rank zero in the tracial-completion ultrapower for simple unital nuclear stably finite algebras. Comparison gives absorption, also under specified bounded-trace hypotheses in the stably projectionless setting.

Mathematical statement of the claimed result

Mathematical claim 1.
Let $\operatorname{Cu}(A)$ be the ordered Cuntz semigroup of positive elements of $A\otimes\mathcal K$, modulo mutual norm-approximation comparison. For separable simple nuclear non-elementary $A$, OpenAI claims $A\simeq A\otimes_{\min}\mathcal Z$ if, for every $x,y\in\operatorname{Cu}(A)$, inequalities $\varphi(x)\le\varphi(y)$ for all additive order/supremum-preserving functionals $\varphi:\operatorname{Cu}(A)\to[0,\infty]$, strict whenever $0<\varphi(y)<\infty$, imply $x\le y$. It further claims absorption for every nonzero separable nuclear $A$ whose Cuntz semigroup satisfies both \[ (l+1)x\le ly\ \Longrightarrow\ x\le y\quad(l\ge1),\qquad \forall x,\ N\ge1\ \exists u:\ Nu\le x\le(N+1)u. \] In that case a unital $\mathcal Z\to (A_\omega\cap A')/\operatorname{Ann}(A)$ is asserted for every free ultrafilter, where $A_\omega$ is the norm ultrapower and $\operatorname{Ann}(A)=\{z:zA=Az=0\}$. Finally it claims \[ A\simeq A\otimes_{\min}\mathcal Z\quad\Longleftrightarrow\quad \operatorname{Cu}(A)\simeq\operatorname{Cu}(A\otimes_{\min}\mathcal Z) \] for all separable nuclear $A$, allowing an abstract ordered-semigroup isomorphism rather than only the canonical first-factor map. Here $\mathcal Z$ is the Jiang--Su algebra, and non-elementary excludes compact-operator algebras.
Mathematical claim 2.
For a separable nuclear complex $C^*$-algebra $A$ with no ideal subquotient that is nonzero and elementary $I/J\simeq\mathcal K(H)$, OpenAI claims \[ \dim_{\mathrm{nuc}}A<\infty\quad\Longleftrightarrow\quad A\simeq A\otimes_{\min}\mathcal Z\quad\Longleftrightarrow\quad\dim_{\mathrm{nuc}}A\le1. \] Nuclear dimension is defined by finite-dimensional completely positive approximations with order-zero color decomposition; $\mathcal Z$ is the Jiang--Su algebra. The conditions are also claimed equivalent to either a canonical or an abstract isomorphism of $\operatorname{Cu}(A)$ with $\operatorname{Cu}(A\otimes_{\min}\mathcal Z)$. Without the subquotient restriction it asserts $\dim_{\mathrm{nuc}}(A_0\otimes_{\min}\mathcal Z)\le1$ for every separable nuclear $A_0$. Separately, for every nonzero unital characterless $D$ it claims a finite maximal tensor power containing two full orthogonal positive elements; full means generating the whole algebra as a closed ideal.
Mathematical claim 3.
Let $A$ be unital, separable, simple, infinite-dimensional, nuclear and stably finite, with nonempty tracial state space $T(A)$. Let $B=\overline A^{T(A)}$ be its completion on the norm-bounded unit ball for $\|a\|_{2,T(A)}=\sup_\tau\tau(a^*a)^{1/2}$, and $B^\omega$ its uniform-tracial ultrapower for a free ultrafilter. If $B^\omega$ has real rank equal to zero when given the quotient $C^*$-norm, OpenAI claims a central projection $p$ satisfying \[ \lambda(px)=\tfrac12\lambda(x)\qquad(x\in B,\ \lambda\in\Lambda_\omega), \] where $\Lambda_\omega$ consists of ultralimits of sequences of designated trace extensions. It also claims every tracial state on $B$ is the unique extension of a trace of $A$, with $|\sigma(b)|\le\|b\|_{2,T(A)}$. For a unital nuclear inclusion $A\subset D$ with $D$ real rank zero and nonempty traces, assume arbitrarily small uniformly tracial full projections in $D$. It claims finite-set approximate central halving projections: given finite $K\subset\mathcal U(A)$ and $\varepsilon>0$, some projection $P\in D$ satisfies $\sup_\tau\|[P,x]\|_{2,\tau}<\varepsilon$ and $\sup_\tau|\tau(Px)-\tau(x)/2|<\varepsilon$ for $x\in K$. The independent unital result takes an infinite-dimensional nuclear complex $C^*$-algebra $A$, assumed simple, separable and unital. For positive $a,b\in A\otimes\mathcal K$, define $d_\tau(a)=\lim_{n\to\infty}(\tau\otimes\operatorname{Tr})(a^{1/n})$, using the unnormalized matrix trace. Assume \[ b\ne0,\quad d_\tau(a)<d_\tau(b)\quad(\tau\in T(A))\quad\Longrightarrow\quad a\precsim b. \] When $T(A)$ is empty, this premise still requires $a\precsim b$ for every positive $a$ and every nonzero positive $b$. OpenAI claims $A\simeq A\otimes\mathcal Z$; when traces exist it also constructs uniform property $\Gamma$. The separate nonunital theorem starts with a nonzero nuclear complex $C^*$-algebra $A$ that is simple and separable, with no nonzero projection in $A\otimes\mathcal K$. Write $T_{\mathrm{lsc}}(A)$ for densely finite lower-semicontinuous traces, and $T_1(A)$ for those bounded traces having norm one. Require every trace in $T_{\mathrm{lsc}}(A)$ to be bounded on the positive unit ball, and require $T_1(A)$ to be nonempty and weak-$*$ compact. The precise comparison premise is \[ \forall a,b\in(A\otimes\mathcal K)_+,\quad b\ne0,\quad \left[d_\tau(a)<1\text{ for every }\tau\in T_{\mathrm{lsc}}(A)\text{ with }d_\tau(b)=1\right] \ \Longrightarrow\ a\precsim b. \] Under these hypotheses it claims uniform property $\Gamma$ and $A\simeq A\otimes\mathcal Z$. Here $a\precsim b$ means $x_n^*bx_n\to a$ in norm for stabilized elements $x_n$, and $\mathcal Z$ is the Jiang--Su algebra.

Outline of the argument

Manuscript 1 (family 291, 2026-09-23): Trace transfer into small hereditary supports followed by spectral rounding establishes full Cuntz-semigroup divisibility. Pure-state compression produces norm-visible matrix cones, while localized nuclear approximations produce trace-visible ones. Comparison packs their defects into a central corner, constructing dimension-drop maps whose lifted intertwining relations give Jiang--Su absorption.

Manuscript 2 (family 291, 2026-09-23): Localized order-zero approximations control ranks even when traces are infinite on some ideals. A supporting map and comparison yield two-color approximations that survive stabilization and hereditary passage. Conversely, Gaussian sign tensors and pure-state excision construct two full orthogonal central elements from the absence of characters, supplying the absorption criterion.

Manuscript 3 (family 291, 2026-09-23): Nuclear averaging and scalar block compressions preserve coefficient traces while packing small projections with controlled commutators. A separate comparison construction rounds ranks, forms clipped sums of centered symmetries, and extracts Gaussian trace partitions. In the projectionless case, a combined overlap-and-model cost controls small splittings before reindexing amplifies them to exact central partitions.

Formal verification

For family 291, the scope page documents the following selections. The selection gives uniform Gamma from real rank zero of the designated tracial ultrapower. The documented comparison scope also treats Jiang--Su absorption and Gamma under strict comparison, with additional trace and target-rank conditions in the projectionless case. Manuscript 1 is not among the papers selected by that page, so the family link does not formalize its main conclusion. It does not establish formal coverage of the complete problem clause. Manuscript 2 is not among the papers selected by that page, so the family link does not formalize its main conclusion. It does not establish formal coverage of the complete problem clause. The documented statement covers the main claim of manuscript 3. It does not establish formal coverage of the complete problem clause. Comparator files: UniformGamma.lean. Declarations: OAI.ComparatorModel.CurrentMain.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