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 $Θ(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

翻译：暂无翻译