← All papers
First page of Lieb's Permanental Dominance Conjecture for Ordinary Immanants through Order Fifteen

Lieb's Permanental Dominance Conjecture for Ordinary Immanants through Order Fifteen

Yinjie Li

math.CO Sep 11, 2026 · v1 math.RT
The order-14 bridge inequality for immanant (4,4,3,3) is formalized and kernel-checked in Lean 4 over Hermitian PSD matrices.
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.

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.

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.

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.

np(n)parameter labelsdistinct raysspan rank
1413550953366134
1517681125398175
Central witness cone data at orders 14 and 15