A fully Lean-verified quadratic lower bound on the border determinantal complexity of $x_1^n+\cdots +x_n^n$ over $\mathbb{C}$, including the symmetric and exact models

Abstract

We present the first end-to-end Lean-verified superlinear lower bound on border determinantal complexity. Let $F_n=x_1^n+\cdots +x_n^n$. We prove, over $\mathbb{C}$, that the border determinantal complexity of $F_n$ is at least $(n-1{)}^2/(4e)$ and its symmetric border determinantal complexity is at least $(n-1{)}^2/(2e)$; the same bounds therefore hold for exact determinantal complexity. Together with known $O(n^2)$ constructions, both border quantities are $\Theta (n^2)$. The proof compares one enumerative invariant on two sides of a degeneration. On the determinant side, the $(n-2)$nd multidegree of the multiplicity-one Gauss graph of any size-$m$ affine-linear determinant is bounded by an explicit multihomogeneous Bézout number; no smoothness, irreducibility, or squarefreeness is assumed. On the target side, a flat limit of these effective Gauss-graph cycles contains the conormal variety of the projective Fermat cone, whose relevant multidegree is the classical dual degree $n(n-1{)}^{n-2}$. Effectivity gives the inequality in the correct direction, and an $(n-1)$st root yields the quadratic bound. All four bounds are fully verified in Lean 4 with Mathlib. The Lean theorems assume only $n\ge 3$ and a literal determinantal representation or literal border membership, and depend on no axioms beyond Lean's foundational ones. The formal proof follows a localized version of the argument presented here: where the text compares global cycles, it compares local intersection lengths of finite slices of those cycles. Lean sources: https://github.com/karthik202321/power-sum-dc-lean; archived release: https://doi.org/10.5281/zenodo.23274251

arXiv comment50 pages. v3 adds an end-to-end Lean 4 verification of all main bounds (Appendix D; links in abstract); new title and abstract. Mathematical changes since v2: Lemma 7.4 conservation now via Euler characteristics of bidegree twists; Prop. 9.1 cone shift computed away from the vertex; Sec. 4.3 Step 3 ideal statement corrected; Remark 10.1 corrected. Theorem statements unchanged