The unique middle label of a reconnected cap

Abstract

The unique middle label of a reconnected cap.

Theorem 1.1 (The unique middle label of a reconnected cap).

$$\forall L\in Type,\forall m\in Natural,\forall M\in \mathrm{NCMatching}\left(m+2\right),\forall j\in \mathrm{Fin}\left(m+1\right),\forall y\in \mathrm{Function}\left(\mathrm{Fin}\left(m+1\right),L\right),\mathrm{Partner}\left(M,\mathrm{CastSucc}\left(j\right)\right)\ne \mathrm{Succ}\left(j\right)\Rightarrow \left(\mathrm{Compatible}\left(\mathrm{CapSurgery}\left(M,j\right),y\right)\Rightarrow \mathrm{Apply}\left(y,j\right)=\mathrm{Apply}\left(y,\mathrm{Succ}\left(\mathrm{CapU}\left(M,j\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Partner-closed intervals transport the labels through all intervening arcs in every relative-order case of a nonclosed cap.

Theorem 1.2 (The unique middle label of a reconnected cap).

$$\forall L\in Type,\forall m\in Natural,\forall M\in \mathrm{NCMatching}\left(m+2\right),\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,\mathrm{Partner}\left(M,\mathrm{CastSucc}\left(j\right)\right)\ne \mathrm{Succ}\left(j\right)\Rightarrow \left(\mathrm{Compatible}\left(M,\mathrm{DetourLabels}\left(j,y,b\right)\right)\iff \left(\mathrm{Compatible}\left(\mathrm{CapSurgery}\left(M,j\right),y\right)\wedge b=\mathrm{Apply}\left(y,\mathrm{CastSucc}\left(\mathrm{CapU}\left(M,j\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Compatibility after reconnecting the two original partners is equivalent to compatibility before surgery with exactly the prescribed middle label. Both side equations and every surviving endpoint are retained.

References

• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/NonclosedCapLabels.cap_outer_label
• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/NonclosedCapLabels.nonclose_compatible_iff
• Dependency: D5/S3/Combinatorics/PerfectMatchings/ClosedCapFiber