Label transport across closed matching intervals

Abstract

Label transport across closed matching intervals.

Theorem 1.1 (Label transport across closed matching intervals).

$$\forall L\in Type,\forall n\in Natural,\forall M\in \mathrm{NCMatching}\left(n\right),\forall y\in \mathrm{Function}\left(\mathrm{Fin}\left(n+1\right),L\right),\forall l\in \mathrm{Fin}\left(n+1\right),\forall r\in \mathrm{Fin}\left(n+1\right),\mathrm{Compatible}\left(M,y\right)\Rightarrow \left(l\le r\Rightarrow \left(\mathrm{IntervalClosed}\left(M,l,r\right)\Rightarrow \mathrm{Apply}\left(y,l\right)=\mathrm{Apply}\left(y,r\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

A partner-closed interval has equal boundary labels under every compatible labelling. Strong induction removes its first matched block and retains a closed suffix. The interval may contain any number of nested or disjoint arcs, and zero length is included.

References

• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/OrderedMatchingIntervals.closed_interval_gap
• Dependency: D5/S3/Combinatorics/PerfectMatchings/OrderedMatchingCore