# Foulkes' conjecture for sixth powers and quadratic stabilization

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

- [Quadratic stabilization of the canonical Foulkes–Howe map](../../preprints/Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026/paper.pdf)

## 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](../ComparatorChallenges/FoulkesHowe.lean) |