PanSkanderaWangAllSplitsBlock

Abstract

A permutation preserves a block exactly when membership before and after its action agrees at every index.

Definition 1.1 (Preserves).

$$\forall alpha\in Type\ast ,[\mathrm{DecidableEq}\left(alpha\right)]\forall s\in \mathrm{Finset}\left(alpha\right),\forall w\in \mathrm{Perm}\left(alpha\right),(\mathrm{Preserves}\left(s,w\right))\iff (\forall i\in alpha,(w\left(i\right)\in s)\iff (i\in s))$$

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

A permutation preserves a block exactly when membership before and after its action agrees at every index. The anonymous bracket is the Lean DecidableEq instance; alpha is an arbitrary type.

Definition 1.2 (blockEquiv).

$$\forall alpha\in Type\ast ,[\mathrm{DecidableEq}\left(alpha\right)]\forall s\in \mathrm{Finset}\left(alpha\right),(\forall sigma\in \mathrm{Perm}\left(s\right),\forall tau\in \mathrm{Perm}\left(\mathrm{Subtype}\left(alpha,fun(i:alpha)\mapsto \neg (i\in s)\right)\right),\mathrm{val}\left(\mathrm{blockEquiv}\left(s\right)\left(\mathrm{pair}\left(sigma,tau\right)\right)\right)=\mathrm{ofSubtype}\left(sigma\right)\cdot \mathrm{ofSubtype}\left(tau\right))\wedge (\forall w\in \mathrm{Subtype}\left(\mathrm{Perm}\left(alpha\right),fun(w:\mathrm{Perm}\left(alpha\right))\mapsto \mathrm{Preserves}\left(s,w\right)\right),\mathrm{symm}\left(\mathrm{blockEquiv}\left(s\right)\right)\left(w\right)=\mathrm{pair}\left(\mathrm{subtypePerm}\left(\mathrm{val}\left(w\right),\mathrm{property}\left(w\right)\right),\mathrm{subtypePerm}\left(\mathrm{val}\left(w\right),fun(i:alpha)\mapsto \mathrm{notCongr}\left(\mathrm{property}\left(w\right)\left(i\right)\right)\right)\right))$$

Formalization. D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBlock.blockEquiv (✓ 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 forward defining expression extends the two subtype permutations by identity and multiplies them. The inverse defining expression restricts the block-preserving permutation to the block and its complement. val and property are the two subtype projections; the inverse laws are verified in Lean.

Theorem 1.3 (permanent block expansion).

$$\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)\cdot \mathrm{principalPermanent}\left(A,\mathrm{univ}\left(\mathrm{Fin}\left(n\right)\right)\setminus s\right)=\mathrm{sum}\left(fun(w:\mathrm{Subtype}\left(\mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),fun(v:\mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right))\mapsto \mathrm{Preserves}\left(s,v\right)\right))\mapsto \mathrm{monomial}\left(A,\mathrm{val}\left(w\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBlock.permanent_block_expansion (✓ 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 product of the complementary principal permanents equals the sum over all block-preserving permutation monomials. The constructed block equivalence identifies the two independently chosen permutations with a single permutation of the whole index set.

References

• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBlock.Preserves
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBlock.blockEquiv
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsBlock.permanent_block_expansion
• Dependency: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsWord