# Saxl’s conjecture and universal tensor squares

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Universal Tensor Squares for Symmetric Groups](../../preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/main.pdf)
- [A Cyclic Polytabloid Proof of Saxl's Conjecture](../../preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf)

## Scope

The formalization proves the universal tensor-square conjecture for symmetric groups in the stated range. For every positive integer $n\notin\{2,4,9\}$, it constructs an irreducible complex representation of $S_n$ whose tensor square contains every irreducible complex representation of $S_n$. Equivalently, all corresponding Kronecker coefficients are positive. The statement also supplies injective intertwining maps for arbitrary finite-dimensional irreducible representations.

Saxl's conjecture asserts that the tensor square of each staircase Specht module contains every irreducible representation of the corresponding symmetric group. The formalization establishes this for every $m\ge1$: if $\rho_m=(m,m-1,\ldots,1)$, then $g(\rho_m,\rho_m,\mu)>0$ for every partition $\mu$ of $m(m+1)/2$.

The stronger claim that every constituent appears in the orbit span of one prescribed tensor is not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Universal irreducible tensor squares for symmetric groups | [UniversalTensorSquares.lean](../ComparatorChallenges/UniversalTensorSquares.lean) |
| Saxl's conjecture | [Saxl.lean](../ComparatorChallenges/Saxl.lean) |