# A cubic permanent–determinant lower bound

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

- [A cubic lower bound for border determinantal complexity of the permanent](../../preprints/A-cubic-lower-bound-for-border-determinantal-complexity-of-the-permanent-September-24-2026/A-cubic-lower-bound-for-border-determinantal-complexity-of-the-permanent-September-24-2026.pdf)

## Scope

The formalization proves a cubic lower bound for both exact and border determinantal representations of the complex $m\times m$ permanent. For $m\ge1408$, every affine-linear determinant representation of size $n$, including coefficientwise limits, satisfies $n\ge m^3/(5529600e)$.

A general supporting theorem applies to a polynomial in $d\ge2$ variables whose first nonzero homogeneous Taylor term has degree $r\ge2$ and no nonzero singular zero. Its exact and border determinantal sizes are at least $(r-1)(d-1)/(4e)$. The paper's algebraic-branching-program consequences are outside these statements.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Cubic lower bounds for permanent determinantal complexity | [PermanentCubic.lean](../ComparatorChallenges/PermanentCubic.lean) |
| Determinantal lower bound from a smooth initial form | [SmoothInitialForm.lean](../ComparatorChallenges/SmoothInitialForm.lean) |