Productive paired-anchor position synchronization

Counted pending-frontier rigidity identifies how much input two aligned parent spines have consumed. In the split-right case this identifies their selected single completion words. Recursing on the shorter parent frontier then synchronizes the exact parent positions, after which the boundary- sensitive split-right theorem identifies the two child positions.

theorem DPDA_to_LR.productivePairedVisibleAnchorPositionsEqual {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : ProductivePairedVisibleAnchorPositionsEqual M

Productive paired visible anchors have the same exact structural position, including the displayed-list/hidden-context boundary.