Documentation

LeanPool.RegtsSevenster.RS.Novel.Coordinates.SlotPairing

The slot pairing #

The flag enumeration sends the fragment pairing to the straight cap matching: the two flags of the i-th canonical edge sit at slots i and edgeCount + i. The general-flag glue for the Eulerian reindex.

source
theorem RS.starFlagEnum_symm_castAdd (W : ClosedFragment) (i : Fin (edgeCount W)) :
(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) = (canonicalReps W)[↑i]

The rep slot carries the canonical representative.

source
theorem RS.starFlagEnum_symm_natAdd (W : ClosedFragment) (i : Fin (edgeCount W)) :
(starFlagEnum W).symm (Fin.natAdd (edgeCount W) i) = W.pairing (canonicalReps W)[↑i]

The partner slot carries the paired flag.

source
theorem RS.pairing_starFlagEnum_symm (W : ClosedFragment) (i : Fin (edgeCount W)) :
W.pairing ((starFlagEnum W).symm (Fin.castAdd (edgeCount W) i)) = (starFlagEnum W).symm (Fin.natAdd (edgeCount W) i)

The slot pairing: the fragment pairing links slot i to slot edgeCount + i.