we-solve (beta)

Math-2522 · mathematics · Algebra

Every irreducible occurs in the staircase tensor square

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every $m\geq 1$, put $N=m(m+1)/2$ and $\rho =(m,m-1,\dots ,1)$. Does the tensor square of the complex Specht representation $S^\rho $ contain every irreducible representation of $S_N$; equivalently, is $g(\rho ,\rho ,\lambda )>0$ for every partition $\lambda $ of N?

Short English statement

For every $m\geq 1$, put $N=m(m+1)/2$ and $\rho =(m,m-1,\dots ,1)$. Does the tensor square of the complex Specht representation $S^\rho $ contain every irreducible representation of $S_N$; equivalently, is $g(\rho ,\rho ,\lambda )>0$ for every partition $\lambda $ of N?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2522

The Saxl theorem states g(rho_m,rho_m,lambda)>0 for every m>=1 and every partition lambda of N_m. This exactly matches the complete question. lean/docs/205.md covers staircase positivity but not the stronger cyclic-orbit-span theorem. Within these assumptions, this is a claimed affirmative answer to the stated question.

Every irreducible occurs in the staircase tensor square

OpenAI's claim

OpenAI presents a proof in the selected manuscript. Every irreducible constituent is claimed to occur in the tensor square of the staircase representation of the appropriate symmetric group.

Mathematical statement of the claimed result

Result 1.
Set $\rho_m=(m,m-1,\ldots,1)$ and $N_m=m(m+1)/2$. For every $m\ge1$ and partition $\lambda\vdash N_m$, the source claims \[ g(\rho_m,\rho_m,\lambda)>0, \] where $g$ is the Kronecker coefficient. Equivalently, every irreducible complex $S_{N_m}$-module occurs in the tensor square of the staircase Specht module.

Outline of the argument

Row and column alternation on a triangular set of tensor positions gives one prescribed cyclic vector. Nonzero pairings show that its orbit already supports all required constituents; band decompositions and induction maintain the generator information rather than merely proving positivity somewhere in an ambient tensor product.

Formal verification

For family 205, the Lean scope includes every staircase tensor square and the universal irreducible squares away from degrees $2,4,9$; occurrence inside the orbit of the prescribed cyclic vector is extra manuscript scope. The listed Comparator files are Saxl.lean, UniversalTensorSquares.lean. Named declarations include OAI.Saxl.saxl_conjecture. 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 →