Algebra · Result 210

Foulkes' conjecture for sixth powers and quadratic stabilization

2 papersLean

Proves the sixth case of Foulkes’ conjecture: \(\mathop{\mathrm{Sym}}\nolimits ^6(\mathop{\mathrm{Sym}}\nolimits ^bV)\) embeds equivariantly in \(\mathop{\mathrm{Sym}}\nolimits ^b(\mathop{\mathrm{Sym}}\nolimits ^6V)\) for every b ≥ 6 and finite-dimensional complex V. More generally, the canonical multiplication map \(\mathop{\mathrm{Sym}}\nolimits ^b(\mathop{\mathrm{Sym}}\nolimits ^aV)\to\mathop{\mathrm{Sym}}\nolimits ^a(\mathop{\mathrm{Sym}}\nolimits ^bV)\) is surjective for a ≥ 2 and \(b\ge a(a-1)\), giving dimension-independent quadratic stabilization.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Foulkes' conjecture for the sixth symmetric power

OpenAI · September 25, 2026

We prove the sixth-symmetric-power case of Foulkes' conjecture. For every integer b ≥ 6 and every finite-dimensional complex vector space V, there is a \(\mathop{\mathrm{GL}}\nolimits (V)\)-equivariant injection \(\mathop{\mathrm{Sym}}\nolimits ^6(\mathop{\mathrm{Sym}}\nolimits ^b V)\hookrightarrow\mathop{\mathrm{Sym}}\nolimits ^b(\mathop{\mathrm{Sym}}\nolimits ^6 V)\).

Read PDF Download Source

Cite

@misc{OAI:Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026,
  author = {{OpenAI}},
  title = {{Foulkes' conjecture for the sixth symmetric power}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/main.pdf}{OAI:Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026}},
  year = {2026}
}

Quadratic stabilization of the canonical Foulkes--Howe map

OpenAI · September 25, 2026

For every finite-dimensional complex vector space V, we prove that the canonical Foulkes–Howe map \(\mathop{\mathrm{Sym}}\nolimits ^b(\mathop{\mathrm{Sym}}\nolimits ^a V)\longrightarrow\mathop{\mathrm{Sym}}\nolimits ^a(\mathop{\mathrm{Sym}}\nolimits ^b V)\) is surjective whenever a ≥ 2 and \(b\ge a(a-1)\). This gives a quadratic stabilization bound independent of \(\dim V\).

Read PDF Download Source

Cite

@misc{OAI:Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026,
  author = {{OpenAI}},
  title = {{Quadratic stabilization of the canonical Foulkes--Howe map}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026/paper.pdf}{OAI:Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

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

Quadratic stabilization of the canonical Foulkes–Howe map

Scope

The formalized result proves surjectivity of the canonical averaged Foulkes–Howe map \(\mathrm{Sym}^b(\mathrm{Sym}^a\,V)\to\mathrm{Sym}^a(\mathrm{Sym}^b\,V)\) for every finite-dimensional complex vector space, \(a\ge2\), and \(b\ge a(a-1)\). It also covers the bijective \(a=1\) case, the vanishing-on-products consequence, and the corresponding equivariant embedding in the reverse direction. The sixth-power specialization is covered for \(b\ge30\); the companion's full range \(b\ge6\) is not included.

Comparator links

Result	Comparator statement
Quadratic stabilization of the canonical Foulkes–Howe map	FoulkesHowe.lean

Scope note on GitHub →