Adjacent cap removal in a noncrossing matching

Abstract

Adjacent cap removal in a noncrossing matching.

Theorem 1.1 (Adjacent cap removal in a noncrossing matching).

$$\forall m\in Natural,\forall M\in \mathrm{NCMatching}\left(m+2\right),\forall j\in \mathrm{Fin}\left(m+1\right),\forall k\in \mathrm{Fin}\left(m\right),\mathrm{SkipPair}\left(j,\mathrm{Partner}\left(\mathrm{CapSurgery}\left(M,j\right),k\right)\right)=\mathrm{ReconnectPartner}\left(M,j,\mathrm{SkipPair}\left(j,k\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PerfectMatchings/AdjacentCapSurgery.capSurgery_reconnect (✓ std3). ∎

Source. Repository-derived.

Commentary.

The increasing survivor map identifies the smaller partner with the exact original rewiring. The already-paired case and every possible relative order of the two original partners are retained, including an empty surviving frontier.

References

• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/AdjacentCapSurgery.capSurgery_reconnect
• Dependency: D5/S3/Combinatorics/PerfectMatchings/OrderedMatchingIntervals