PanSkanderaWangAllSplitsChain

Abstract

TNN means that every square submatrix selected by increasing row and column embeddings has nonnegative determinant.

Definition 1.1 (TNN).

$$\forall n\in \mathbb{N},\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{R}\right),(\mathrm{TNN}\left(A\right))\iff (\forall k\in \mathbb{N},\forall r\in \mathrm{OrderEmbedding}\left(\mathrm{Fin}\left(k\right),\mathrm{Fin}\left(n\right)\right),\forall c\in \mathrm{OrderEmbedding}\left(\mathrm{Fin}\left(k\right),\mathrm{Fin}\left(n\right)\right),0\le \det \left(\mathrm{submatrix}\left(A,r,c\right)\right))$$

Formalization. D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.TNN (✓ std3).

Citation. 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.

Source, Section 1 (p. 139): “We call A ∈ Matₙ×ₙ(ℝ) totally nonnegative if each of its minors is negative.” The next sentence specifies the defining inequalities det(Aᵢ,ⱼ) ≥ 0. The word negative in the first sentence conflicts with those displayed inequalities; TNN uses the displayed nonnegative inequalities. Every square submatrix selected by increasing row and column embeddings has nonnegative determinant. OrderEmbedding denotes the increasing order embeddings in the Lean statement, including the empty minor.

Definition 1.2 (principalPermanent).

$$\forall n\in \mathbb{N},\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{R}\right),\forall s\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\mathrm{principalPermanent}\left(A,s\right)=\mathrm{permanent}\left(\mathrm{submatrix}\left(A,fun(i:s)\mapsto \mathrm{val}\left(i\right),fun(j:s)\mapsto \mathrm{val}\left(j\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.principalPermanent (✓ 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.

The principal permanent uses Matrix.permanent on the literal subtype of indices belonging to s. Here val on a subtype is its underlying Fin n index; an empty principal permanent is one.

Definition 1.3 (evenIndices).

$$\forall n\in \mathbb{N},\mathrm{evenIndices}\left(n\right)=\mathrm{filter}\left(\mathrm{univ}\left(\mathrm{Fin}\left(n\right)\right),fun(i:\mathrm{Fin}\left(n\right))\mapsto \left(\mathrm{val}\left(i\right)+1\right)\mathrm{mod}2=0\right)$$

Formalization. D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.evenIndices (✓ 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.

Lean indices start at zero. Filtering by (val i + 1) mod 2 = 0 therefore selects the even indices printed in the paper.

Definition 1.4 (prefixIndices).

$$\forall n\in \mathbb{N},\forall h\in \mathbb{N},\mathrm{prefixIndices}\left(n,h\right)=\mathrm{filter}\left(\mathrm{univ}\left(\mathrm{Fin}\left(n\right)\right),fun(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{val}\left(i\right)<h\right)$$

Formalization. D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.prefixIndices (✓ 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.

The initial h indices are selected by val i < h, with no restriction on h in this definition.

Definition 1.5 (monomial).

$$\forall n\in \mathbb{N},\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{R}\right),\forall w\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\mathrm{monomial}\left(A,w\right)=\mathrm{prod}\left(fun(k:\mathrm{Fin}\left(n\right))\mapsto A\left(k,w\left(k\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.monomial (✓ 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.

The operator prod multiplies its function over every element of the finite domain. The monomial places the permutation value in the column index.

References

• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.TNN
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.evenIndices
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.monomial
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.prefixIndices
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsChain.principalPermanent