PanSkanderaWangAllSplitsPermanentPadding

Abstract

The defining filter pulls an index set back along Fin.succ, extracting precisely its old matrix indices..

Definition 1.1 (oldIndices).

$$\forall n\in \mathbb{N},\forall s\in \mathrm{Finset}\left(\mathrm{Fin}\left(n+1\right)\right),\mathrm{oldIndices}\left(s\right)=\mathrm{filter}\left(\mathrm{univ}\left(\mathrm{Fin}\left(n\right)\right),fun(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{succ}\left(i\right)\in s\right)$$

Formalization. D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.oldIndices (✓ 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 defining filter pulls an index set back along Fin.succ, extracting precisely its old matrix indices.

Theorem 1.2 (principal padOne).

$$\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+1\right)\right),\mathrm{principalPermanent}\left(\mathrm{padOne}\left(A\right),s\right)=\mathrm{principalPermanent}\left(A,\mathrm{oldIndices}\left(s\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.principal_padOne (✓ 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.

Every selected principal permanent loses only the newly adjoined identity coordinate. If that coordinate is present, decomposing permutations of an Option type leaves precisely the permutations that fix it; all other summands contain a zero entry.

Definition 1.3 (splitProduct).

$$\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 h\in \mathbb{N},\mathrm{splitProduct}\left(A,h\right)=\mathrm{principalPermanent}\left(A,\mathrm{prefixIndices}\left(n,h\right)\right)\cdot \mathrm{principalPermanent}\left(A,\mathrm{univ}\left(\mathrm{Fin}\left(n\right)\right)\setminus \mathrm{prefixIndices}\left(n,h\right)\right)$$

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

This is the product of the two complementary principal permanents for the literal initial split.

Definition 1.4 (parityProduct).

$$\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{parityProduct}\left(A\right)=\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)$$

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

This is the product of the principal permanents on the even and odd one-based indices.

Theorem 1.5 (split padLeft).

$$\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 d\in \mathbb{N},\forall h\in \mathbb{N},\mathrm{splitProduct}\left(\mathrm{padLeft}\left(A,d\right),h+d\right)=\mathrm{splitProduct}\left(A,h\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.split_padLeft (✓ 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.

After d left identity coordinates, the split at h+d has the same permanent product as the original split at h. Induction tracks the literal initial index set through each padding step.

Theorem 1.6 (parity padLeft).

$$\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 d\in \mathbb{N},\mathrm{parityProduct}\left(\mathrm{padLeft}\left(A,d\right)\right)=\mathrm{parityProduct}\left(A\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.parity_padLeft (✓ 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.

Left identity padding preserves the alternating permanent product. Each step swaps the two old parity classes, and multiplication makes the product invariant under that swap.

References

• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.oldIndices
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.parityProduct
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.parity_padLeft
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.principal_padOne
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.splitProduct
• Truth anchor: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPermanentPadding.split_padLeft
• Dependency: D5/S3/Combinatorics/Permanental/PanSkanderaWangAllSplitsPadding