we-solve (beta)

Math-2520 · mathematics · Algebra

Finite torsion-class support for traces over l1 group algebras

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every discrete group G and idempotent $e\in M_q(\ell ^{1}(G))$, $q\geq 1$, is there a finite set F of finite-order conjugacy classes such that the diagonal coefficient sum of e over every conjugacy class outside F is zero?

Short English statement

For every discrete group G and idempotent $e\in M_q(\ell ^{1}(G))$, $q\geq 1$, is there a finite set F of finite-order conjugacy classes such that the diagonal coefficient sum of e over every conjugacy class outside F is zero?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2520

The main theorem supplies a finite F subset of finite-order conjugacy classes and zero class sums outside F for every idempotent matrix over l^1(G). lean/docs/207.md only documents the complex group-ring companion, so the l^1 completion assertion is not documented as formalized. Within these assumptions, this is a claimed affirmative answer to the stated question.

Finite torsion-class support for traces over l1 group algebras

OpenAI's claim

OpenAI presents a proof in the selected manuscript. For every discrete group, the trace of an idempotent matrix over $\ell^1(G;\mathbb C)$ is claimed to vanish outside a finite collection of finite-order conjugacy classes.

Mathematical statement of the claimed result

Result 1.
For any discrete group $G$, any integer $q\ge1$, and any idempotent matrix $e\in M_q(\ell^1(G))$, write $\tau_C(e)$ for the sum, on a conjugacy class $C$, of the coefficients of its diagonal trace. The claim is that some finite set $F$ of finite-order conjugacy classes satisfies \[ C\notin F\quad\Longrightarrow\quad\tau_C(e)=0. \] Equivalently, the $\ell^1$ Hattori--Stallings trace has image in the algebraic direct sum on torsion conjugacy classes. No claim about arbitrary positive-characteristic fields follows from this complex Banach-algebra statement.

Outline of the argument

Analytic idempotent correction first replaces the matrix, up to similarity, by one with exponential decay. Weighted cyclic configurations are then treated with smooth spatial summaries, multiscale time averages, and an ordered-kernel estimate; one class-independent cutoff proves actual finite support rather than only absolute summability.

Formal verification

For family 207, the documented Lean statements give complex group-ring Bass trace support and characteristic-zero torsion-free trace rank and idempotent triviality. The separate $\ell^1$ theorem is not selected. No Comparator is assigned to the selected manuscript here; the family page selects other papers or supporting statements. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →