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

Abstract

We prove the ordinary irreducible-immanant form of Lieb’s permanental dominance conjecture through order fifteen. Building on Pate’s results through order thirteen, we settle the remaining order-14 case and the two remaining order-15 cases. The argument also yields several infinite families and structural results. All finite certificates are verified by exact integer or rational arithmetic, including an independent reconstruction of the order-15 certificate. The order-14 bridge is additionally formalized and kernel-checked in Lean 4.19.0. The result concerns the ordinary irreducible-immanant specialization and does not claim the full subgroup form of Lieb’s conjecture.