Pan-Skandera-Wang Bruhat Definitions

Abstract

Definitions of the Pan-Skandera-Wang map, its source family, and its Bruhat claim.

Definition 1.1 (Rank tableau count).

$$\forall x\in \mathrm{List}\left(\mathbb{N}\right),p\in \mathbb{N},q\in \mathbb{N},\mathrm{rank}\left(x,p,q\right)=\mathrm{countGE}\left(q,\mathrm{take}\left(x,p\right)\right)$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.rank (✓ 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.

The rank counts entries at least q among the first p positions.

Definition 1.2 (Permutation predicate).

$$\forall n\in \mathbb{N},x\in \mathrm{List}\left(\mathbb{N}\right),(\mathrm{IsPerm}\left(n,x\right))\iff (\mathrm{Perm}\left(x,\mathrm{rangePrime}\left(1,n\right)\right))$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.IsPerm (✓ 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.

A word is a permutation when it is a rearrangement of the interval from one through n.

Definition 1.3 (Bruhat tableau order).

$$\forall n\in \mathbb{N},x\in \mathrm{List}\left(\mathbb{N}\right),y\in \mathrm{List}\left(\mathbb{N}\right),(\mathrm{BruhatLE}\left(n,x,y\right))\iff ((\mathrm{IsPerm}\left(n,x\right))\wedge \left((\mathrm{IsPerm}\left(n,y\right))\wedge (\forall p\in \mathbb{N},q\in \mathbb{N},\mathrm{rank}\left(x,p,q\right)\le \mathrm{rank}\left(y,p,q\right))\right))$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.BruhatLE (✓ 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.

The strong Bruhat order is given by the tableau criterion of Björner and Brenti, Theorem 2.1.5.

Definition 1.4 (The source family A).

$$\forall n\in \mathbb{N},w\in \mathrm{List}\left(\mathbb{N}\right),(A\left(n,w\right))\iff ((\mathrm{IsPerm}\left(n,w\right))\wedge (\mathrm{Perm}\left(\mathrm{take}\left(w,\mathrm{floorHalf}\left(n\right)\right),\mathrm{rangePrime}\left(1,\mathrm{floorHalf}\left(n\right)\right)\right)))$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.A (✓ 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.

The first half of the word permutes the initial interval while the whole word is a permutation.

Definition 1.5 (Reverse-complement map).

$$\forall n\in \mathbb{N},w\in \mathrm{List}\left(\mathbb{N}\right),\mathrm{RU}\left(n,w\right)=\mathrm{map}\left(\Lambda v\mapsto n+1-v,\mathrm{reverse}\left(w\right)\right)$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.RU (✓ 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.

The reverse-complement map reverses a word and replaces each value v by n plus one minus v.

Definition 1.6 (Pair swapping).

$$(\mathrm{swapPairs}\left(\mathrm{nil}\left(\right)\right)=\mathrm{nil}\left(\right))\wedge \left((\mathrm{swapPairs}\left(\mathrm{singleton}\left(a\right)\right)=\mathrm{singleton}\left(a\right))\wedge (\forall a\in \mathbb{N},b\in \mathbb{N},t\in \mathrm{List}\left(\mathbb{N}\right),\mathrm{swapPairs}\left(\mathrm{cons}\left(a,\mathrm{cons}\left(b,t\right)\right)\right)=\mathrm{cons}\left(b,\mathrm{cons}\left(a,\mathrm{swapPairs}\left(t\right)\right)\right))\right)$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.swapPairs (✓ 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.

Pair swapping exchanges adjacent entries and leaves a final unpaired entry fixed.

Definition 1.7 (Suffix-swapping insertion).

$$\forall q\in \mathbb{N},w\in \mathrm{List}\left(\mathbb{N}\right),\mathrm{inss}\left(q,w\right)=\mathrm{append}\left(\mathrm{take}\left(w,q-1\right),\mathrm{cons}\left(\mathrm{length}\left(w\right)+1,\mathrm{swapPairs}\left(\mathrm{drop}\left(w,q-1\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.inss (✓ 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.

The operation inserts the new maximum at position q and swaps successive pairs in the suffix.

Definition 1.8 (Base map).

$$\forall w\in \mathrm{List}\left(\mathbb{N}\right),f4\left(w\right)=\mathrm{if}\left(w=\mathrm{list}\left(1,2,3,4\right),\mathrm{list}\left(1,2,3,4\right),\mathrm{if}\left(w=\mathrm{list}\left(1,2,4,3\right),\mathrm{list}\left(1,4,3,2\right),\mathrm{if}\left(w=\mathrm{list}\left(2,1,3,4\right),\mathrm{list}\left(3,2,1,4\right),\mathrm{if}\left(w=\mathrm{list}\left(2,1,4,3\right),\mathrm{list}\left(3,4,1,2\right),w\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.f4 (✓ 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.

The base map is specified on the four words of size four and fixes every other input at that size.

Definition 1.9 (Recursive Pan-Skandera-Wang map).

$$(\forall w\in \mathrm{List}\left(\mathbb{N}\right),f\left(0,w\right)=w)\wedge (\forall m\in \mathbb{N},w\in \mathrm{List}\left(\mathbb{N}\right),f\left(m+1,w\right)=\mathrm{if}\left(m+1\le 4,f4\left(w\right),\mathrm{if}\left(\mathrm{mod}\left(m,2\right)=0,\mathrm{inss}\left(2\cdot \left(\mathrm{idxOf}\left(w,m+1\right)+1-\mathrm{floorHalf}\left(m\right)\right)-1,f\left(m,\mathrm{eraseIdx}\left(w,\mathrm{idxOf}\left(w,m+1\right)\right)\right)\right),\mathrm{inss}\left(2\cdot \left(\mathrm{idxOf}\left(w,m+1\right)+1-\mathrm{floorHalf}\left(m\right)-1\right),\mathrm{RU}\left(m,f\left(m,\mathrm{RU}\left(m,\mathrm{eraseIdx}\left(w,\mathrm{idxOf}\left(w,m+1\right)\right)\right)\right)\right)\right)\right)\right))$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.f (✓ 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.

The recursive map uses the base cases, the position of the maximum, insertion, and reverse-complementation according to parity.

Definition 1.10 (Bruhat monotonicity claim).

$$\forall n\in \mathbb{N},(4\le n)\Rightarrow (\forall w\in \mathrm{List}\left(\mathbb{N}\right),(A\left(n,w\right))\Rightarrow (\mathrm{BruhatLE}\left(n,w,f\left(n,w\right)\right)))$$

Formalization. D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.claim (✓ 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.

For every size at least four, each source word is below its image in the strong Bruhat order.

References

• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.A
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.BruhatLE
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.IsPerm
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.RU
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.claim
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.f
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.f4
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.inss
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.rank
• Truth anchor: D5/S3/Combinatorics/PanSkanderaWangBruhatDefs.swapPairs