LR(1) assembly from productive anchor synchronization

Both semantic obligations for the productive characteristic grammar reduce to one boundary-sensitive fact about paired last-visible anchors. This file keeps that dependency explicit: the same synchronization theorem determines epsilon-bearing introducing heads and classifies productive empty returns.

theorem DPDA_to_LR.characteristicGrammar_isLR1_of_productivePositions {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hpositions : ProductivePairedVisibleAnchorPositionsEqual M) : (characteristicGrammar M).IsLRk 1

Boundary-sensitive synchronization of productive paired anchors is the single semantic input needed for the characteristic grammar's LR(1) proof.