Lieb's Permanental Dominance Conjecture for Ordinary Immanants through Order Fifteen
Yinjie Li
math.CO
Sep 11, 2026 · v1
math.RT
TL;DR
The order-14 bridge inequality for immanant (4,4,3,3) is formalized and kernel-checked in Lean 4 over Hermitian PSD matrices.
Abstract
Pate proved ordinary irreducible-immanant permanental dominance through order $13$ and identified $(4,4,3,3)$ as the sole remaining order-$14$ case, with $(5,4,3,3)$ and $(3^5)$ forming the order-$15$ frontier. These three cases are settled here; consequently $d_λ(A)/f^λ\le \operatorname{per}(A)$ for every partition $λ\vdash n$ with $n\le15$ and every complex Hermitian positive-semidefinite matrix $A$. The argument also yields results beyond this finite frontier: an exact four-term bridge for $(4,4,3,3)$, the uniform family $(m,4,3,3)$, a two-parameter family $(a,b,3,3)$ for $a\ge b\ge4$ and $5a\ge8b$, and a long-first-row criterion for arbitrary fixed tails. These results arise from explicit specializations of Pate's $W$-function positivity framework using partial swaps, Young projectors, Pieri–content identities, and branching data. For $(3^5)$, an exact Farkas certificate shows that the central-projector partial-swap cone is insufficient; a branching-refined one-swap construction escapes this obstruction and yields a positive $106+19$-witness certificate. Boundary-compression and node-moving results further describe the reach and limitations of the local-filter method. All finite certificates are checked by exact integer or rational arithmetic and are supplied as ancillary material. The order-$14$ bridge is additionally formalized and kernel-checked in Lean 4 for all complex Hermitian positive-semidefinite matrices, including the exact coefficient normalization and the deduction of $(4,4,3,3)$ permanental dominance from four explicitly stated Pate inequalities.
Problem
Lieb's permanental dominance conjecture for ordinary irreducible immanants was proven through order 13, leaving (4,4,3,3) at order 14 and (5,4,3,3), (3^5) at order 15 open. The goal is to settle these remaining frontier cases.
Approach
The work uses Pate's W-function positivity framework with partial swaps, Young projectors, Pieri-content identities, and branching data to construct explicit positive linear certificates. For the order-14 bridge, twenty witnesses combine into an exact rational identity. For (3^5), a branching-refined one-swap construction yields a 106+19-witness certificate. The order-14 bridge is additionally formalized in Lean 4, linking tensor/Gram and representation-theoretic constructions and deducing (4,4,3,3) dominance from four stated Pate inequalities.
Results
The three remaining cases are settled, establishing permanental dominance for all partitions with n<=15. The Lean 4 project (pinned 4.19.0) compiles with no sorry/admit and only standard axioms (propext, Classical.choice, Quot.sound). Additional uniform families and an exact Farkas obstruction for the central cone are obtained.
| n | p(n) | parameter labels | distinct rays | span rank |
|---|
| 14 | 135 | 5095 | 3366 | 134 |
| 15 | 176 | 8112 | 5398 | 175 |
Central witness cone data at orders 14 and 15