PanSkanderaWangAllSplitsWord

Abstract

ListOfFn lists the function values in increasing Fin order.

Definition 1.1 (word).

$$\forall n\in \mathbb{N},\forall w\in \mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\mathrm{word}\left(w\right)=\mathrm{ListOfFn}\left(fun(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{val}\left(w\left(i\right)\right)+1\right)$$

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

ListOfFn lists the function values in increasing Fin order. Adding one converts the zero-based permutation to the paper’s one-based word.

Definition 1.2 (ofWord).

$$\forall n\in \mathbb{N},\forall x\in \mathrm{List}\left(\mathbb{N}\right),\forall hx\in \mathrm{IsPerm}\left(n,x\right),\forall i\in \mathrm{Fin}\left(n\right),\mathrm{val}\left(\mathrm{ofWord}\left(x,hx\right)\left(i\right)\right)=\mathrm{getElem}\left(x,\mathrm{val}\left(i\right)\right)-1$$

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

ofWord is Equiv.ofBijective of the function i mapped to the Fin n value x[val i] - 1. The displayed equation is its defining value expression; getElem uses the index bound obtained from hx. Permutation membership gives positive bounded entries and verifies injectivity and surjectivity. Subtraction on natural numbers is truncated.

References

• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsWord.ofWord
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsWord.word
• Dependency: D5/S3/Combinatorics/PanSkanderaWangBruhat
• Dependency: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBruhat