# Homogeneous depth-five lower bounds for iterated matrix multiplication

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

- [Homogeneous depth-five lower bounds for iterated matrix multiplication](../../preprints/Homogeneous-depth-five-lower-bounds-for-iterated-matrix-multiplication-September-25-2026/Homogeneous-depth-five-lower-bounds-for-iterated-matrix-multiplication-September-25-2026.pdf)

## Scope

Let $\mathrm{IMM}_{n,n}$ be the $(1,1)$ entry of the product of $n$ independent $n\times n$ variable matrices. The formalization proves that, over every characteristic-zero field, syntactically homogeneous depth-five $\Sigma\Pi\Sigma\Pi\Sigma$ circuits computing this polynomial require at least $n^{\sqrt n/400}$ gates for all sufficiently large $n$, with a threshold independent of the field. Arbitrary bottom support, finite fan-in and fan-out, and sharing are allowed.

It also gives, over every field and for $n\ge2$, circuits with at most $n^{\sqrt n+4}$ gates. These are the lower and upper bounds selected from the paper.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Homogeneous depth-five bounds for iterated matrix multiplication | [DepthFive.lean](../ComparatorChallenges/DepthFive.lean) |