Pate proved ordinary irreducible-immanant permanental dominance through order and identified as the sole remaining order- case, with and forming the order- frontier. These three cases are settled here; consequently for every partition with and every complex Hermitian positive-semidefinite matrix . The argument also yields results beyond this finite frontier: an exact four-term bridge for , the uniform family , a two-parameter family for and , and a long-first-row criterion for arbitrary fixed tails. These results arise from explicit specializations of Pate’s -function positivity framework using partial swaps, Young projectors, Pieri–content identities, and branching data. For , 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 -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- 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 permanental dominance from four explicitly stated Pate inequalities.

生成讲解博客的中文版本

生成AI智能校验的中文版本