Insertion of an adjacent labelled detour

Abstract

Insertion of an adjacent labelled detour.

Theorem 1.1 (Insertion of an adjacent labelled detour).

$$\forall L\in Type,\forall m\in Natural,\forall j\in \mathrm{Fin}\left(m+1\right),\forall y\in \mathrm{Function}\left(\mathrm{Fin}\left(m+1\right),L\right),\forall b\in L,\forall k\in \mathrm{Fin}\left(m\right),\mathrm{Apply}\left(\mathrm{DetourLabels}\left(j,y,b\right),\mathrm{CastSucc}\left(\mathrm{SkipPair}\left(j,k\right)\right)\right)=\mathrm{Apply}\left(y,\mathrm{CastSucc}\left(k\right)\right)$$

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

Source. Repository-derived.

Commentary.

Inserting the two cap endpoints leaves the left gap label of every surviving endpoint unchanged under the increasing survivor map.

Theorem 1.2 (Insertion of an adjacent labelled detour).

$$\forall L\in Type,\forall m\in Natural,\forall j\in \mathrm{Fin}\left(m+1\right),\forall y\in \mathrm{Function}\left(\mathrm{Fin}\left(m+1\right),L\right),\forall b\in L,\forall k\in \mathrm{Fin}\left(m\right),\mathrm{Apply}\left(\mathrm{DetourLabels}\left(j,y,b\right),\mathrm{Succ}\left(\mathrm{SkipPair}\left(j,k\right)\right)\right)=\mathrm{Apply}\left(y,\mathrm{Succ}\left(k\right)\right)$$

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

Source. Repository-derived.

Commentary.

The same transport holds for right gap labels. At the cap the three successive labels are the original gap label, the inserted middle label, and the original gap label again.

References

• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/DetourLabels.detour_skip_left
• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/DetourLabels.detour_skip_right
• Dependency: D5/S3/Combinatorics/PerfectMatchings/AdjacentCapSurgery