PanSkanderaWangAllSplitsBalanced

Abstract

For every order at least four, the alternating principal permanent product is at most the product for the balanced initial split.

Theorem 1.1 (balanced).

$$\forall n\in \mathbb{N},(4\le n)\Rightarrow (\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{R}\right),(\mathrm{TNN}\left(A\right))\Rightarrow (\mathrm{principalPermanent}\left(A,\mathrm{evenIndices}\left(n\right)\right)\cdot \mathrm{principalPermanent}\left(A,\mathrm{univ}\left(\mathrm{Fin}\left(n\right)\right)\setminus \mathrm{evenIndices}\left(n\right)\right)\le \mathrm{principalPermanent}\left(A,\mathrm{prefixIndices}\left(n,\mathrm{natDiv}\left(n,2\right)\right)\right)\cdot \mathrm{principalPermanent}\left(A,\mathrm{univ}\left(\mathrm{Fin}\left(n\right)\right)\setminus \mathrm{prefixIndices}\left(n,\mathrm{natDiv}\left(n,2\right)\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBalanced.balanced (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Sihong Pan, Mark Skandera, Jiayuan Wang (2026). Permanental Inequalities and Unit Interval Orders. DOI: 10.4204/EPTCS.445.17. URL: https://arxiv.org/abs/2606.13162v1.

Commentary.

For every order at least four, the alternating principal permanent product is at most the product for the balanced initial split. natDiv is natural-number division, so natDiv(n,2) is the floor of n/2. The recursive bijection pairs the terms, and the rank-to-chain construction proves each paired monomial inequality.

References

• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBalanced.balanced
• Dependency: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBijection
• Dependency: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBlock