The General Subgroup Permanental-Dominance Conjecture in Order Four

Abstract

The general subgroup permanental-dominance conjecture was previously known only through matrix order three. This paper proves its complete order-four case: for every subgroup $H\le S_4$, every irreducible complex character $\chi$ of $H$, and every $4\times 4$ Hermitian positive-semidefinite matrix $A$, it establishes $d_{\chi }^H(A)/\chi (1)\le \mathrm{per}A$. Unlike the usual immanant specialization, the result covers all thirty-seven irreducible-character cases arising from the eleven conjugacy classes of subgroups of $S_4$. Thirty-five cases follow from general principal-minor, moment, and block-contraction inequalities. The two non-real $A_4$ characters are reduced to polynomial nonnegativity on the cone of $3\times 3$ positive-semidefinite Gram matrices and are resolved by a rank-one sum-of-squares identity, an exact positive-definite interior certificate, rational Gram certificates, and closure of the Gram cone.

21 pages. Accompanying Lean 4 formalization and source code are available at the companion repository