Synchronization of active characteristic heads

The hard direction in the characteristic-grammar proof is reverse-edge uniqueness. This file isolates the semantic synchronization facts used by the paired-spine inversion. Reading heads are the first case: two globally reachable normalized-DPDA configurations at the same input cut which can both read the next symbol must coincide.

theorem DPDA_to_LR.activeSingle_simulation_cuts_comparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {suffix₁ suffix₂ w : List T} {q₁ q₂ : Q × Bool} {Z₁ Z₂ : S} {target₁ target₂ : State M} (hspine₁ : ActiveSpine M p (PDA_to_CFG.N.single (Sum.inl q₁) (some Z₁) target₁) suffix₁) (hspine₂ : ActiveSpine M p (PDA_to_CFG.N.single (Sum.inl q₂) (some Z₂) target₂) suffix₂) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal w)) : ∃ (rest₁ : List S) (rest₂ : List S), PDA.Reaches { state := M.firstFinal.initial_state, input := w, stack := [M.firstFinal.start_symbol] } { state := q₁, input := [], stack := Z₁ :: rest₁ } ∧ PDA.Reaches { state := M.firstFinal.initial_state, input := w, stack := [M.firstFinal.start_symbol] } { state := q₂, input := [], stack := Z₂ :: rest₂ } ∧ (PDA.Reaches { state := q₁, input := [], stack := Z₁ :: rest₁ } { state := q₂, input := [], stack := Z₂ :: rest₂ } ∨ PDA.Reaches { state := q₂, input := [], stack := Z₂ :: rest₂ } { state := q₁, input := [], stack := Z₁ :: rest₁ })

Completing a shared visible prefix in the same way places two active simulation-state single heads on comparable cuts of the normalized DPDA run. The returned stacks include the aligned physical contexts reconstructed from the FS-to-empty-stack bottom-marker invariant.

theorem DPDA_to_LR.activeSingle_read_heads_unique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {suffix₁ suffix₂ : List T} {q₁ q₂ target₁ target₂ next₁ next₂ : State M} {a : T} {Z₁ Z₂ : StackSymbol M} {gamma₁ gamma₂ : List (StackSymbol M)} (hspine₁ : ActiveSpine M p (PDA_to_CFG.N.single q₁ Z₁ target₁) suffix₁) (hspine₂ : ActiveSpine M p (PDA_to_CFG.N.single q₂ Z₂ target₂) suffix₂) (hread₁ : (next₁, gamma₁) ∈ (emptyStackPDA M).transition_fun q₁ a Z₁) (hread₂ : (next₂, gamma₂) ∈ (emptyStackPDA M).transition_fun q₂ a Z₂) (hrule₁ : (PDA_to_CFG.N.single q₁ Z₁ target₁, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next₁ gamma₁ target₁)]) ∈ (characteristicGrammar M).rules) : q₁ = q₂ ∧ Z₁ = Z₂

Two active single nodes at the same characteristic prefix which can both read the same next terminal have the same physical state and exposed stack symbol. The terminal suffixes and return targets may differ; neither is needed for this stable-cut synchronization.