Structural residual for same-prefix epsilon returns

The read-generated part of same-prefix empty-return synchronization is already settled by concreteReadEmptyReturn_samePrefix_state_eq. This file records all of the ancestry which remains when the transition-generated edge is an epsilon edge. In particular, it does not identify the two empty-list children: their return states are deliberately kept distinct.

The resulting proposition is the narrow structural theorem still needed by the concrete empty-return classifier. It retains a common terminal completion, the paired last-visible anchors, both zero-visible tails, the genuinely epsilon-bearing left tail, and both useful continuations.

def DPDA_to_LR.SamePrefixEpsilonReturnData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (p : List (symbol T (Nonterminal M))) (q₁ q₂ : State M) (suffix₁ suffix₂ : List T) : Prop

Complete ancestry and productivity data for an epsilon-generated empty return compared with an arbitrary empty return at the same visible prefix.

The two child indices remain list q₁ [] q₁ and list q₂ [] q₂; assuming them equal here would be circular.

Equations

• One or more equations did not get rendered due to their size.

def DPDA_to_LR.SamePrefixEpsilonReturnsStateUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Prop

The exact remaining semantic statement. Unlike the earlier SamePrefixEpsilonReturnResidual, this property exposes the paired structural history required by an interval/ancestry proof.

Equations

• One or more equations did not get rendered due to their size.

theorem DPDA_to_LR.zeroVisibleEmptyList_state_eq_of_anchor_position_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {completion : List T} {anchor₁ anchor₂ : Nonterminal M} {anchorSuffix₁ anchorSuffix₂ suffix₁ suffix₂ : List T} {anchorContext₁ anchorContext₂ context₁ context₂ : List (StackSymbol M)} {q₁ q₂ final₁ final₂ : State M} (leftAnchor : VisibleSpineAnchor M p anchor₁ anchorSuffix₁ completion anchorContext₁) (rightAnchor : VisibleSpineAnchor M p anchor₂ anchorSuffix₂ completion anchorContext₂) (leftTail : ZeroVisibleTail M p completion anchor₁ anchorSuffix₁ anchorContext₁ (PDA_to_CFG.N.list q₁ [] q₁) suffix₁ context₁) (rightTail : ZeroVisibleTail M p completion anchor₂ anchorSuffix₂ anchorContext₂ (PDA_to_CFG.N.list q₂ [] q₂) suffix₂ context₂) (hposition : leftmostEpsilonPositionOf M anchor₁ anchorContext₁ = leftmostEpsilonPositionOf M anchor₂ anchorContext₂) (useful₁ : PDA.Reaches { state := q₁, input := suffix₁, stack := context₁ } { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches { state := q₂, input := suffix₂, stack := context₂ } { state := final₂, input := [], stack := [] }) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂

Two productive zero-visible tails whose anchors denote the same physical displayed-stack position have the same empty-list return state. This is the forward synchronization principle used for root/root and read/read paired anchors; it does not assume equal operational step counts.

def DPDA_to_LR.UnequalCountSamePrefixEpsilonReturnData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (p : List (symbol T (Nonterminal M))) (q₁ q₂ : State M) (suffix₁ suffix₂ : List T) : Prop

The exact counted residual after useful cross-input determinism has disposed of equal-length computations. Keeping the structural datum in the proposition prevents the unequal-count branch from discarding its grammar ancestry.

Equations

• One or more equations did not get rendered due to their size.

theorem DPDA_to_LR.samePrefixEmptyListCuts_state_eq_of_equal_steps {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {completion suffix₁ suffix₂ : List T} {steps : ℕ} {q₁ q₂ final₁ final₂ : State M} {context₁ context₂ : List (StackSymbol M)} (run₁ : PDA.ReachesIn steps { state := (emptyStackPDA M).initial_state, input := completion, stack := [(emptyStackPDA M).start_symbol] } { state := q₁, input := [], stack := context₁ }) (run₂ : PDA.ReachesIn steps { state := (emptyStackPDA M).initial_state, input := completion, stack := [(emptyStackPDA M).start_symbol] } { state := q₂, input := [], stack := context₂ }) (useful₁ : PDA.Reaches { state := q₁, input := suffix₁, stack := context₁ } { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches { state := q₂, input := suffix₂, stack := context₂ } { state := final₂, input := [], stack := [] }) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂

Equal-length globally useful cuts at a common completed prefix have the same state even when their untouched suffixes differ.

theorem DPDA_to_LR.SamePrefixEpsilonReturnData.state_eq_or_unequal_counts {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {q₁ q₂ : State M} {suffix₁ suffix₂ : List T} (data : SamePrefixEpsilonReturnData M p q₁ q₂ suffix₁ suffix₂) : q₁ = q₂ ∨ UnequalCountSamePrefixEpsilonReturnData M p q₁ q₂ suffix₁ suffix₂

Cross-input determinism closes the equal-count branch of the structural residual. Hence a genuinely distinct return pair has unequal global step counts; all of its paired-anchor ancestry is retained for the subsequent interval-order argument.

theorem DPDA_to_LR.samePrefixEpsilonReturnData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {q₁ q₂ : State M} {suffix₁ suffix₂ : List T} (edge₁ : ConcreteEpsilonEmptyEdge M p q₁ suffix₁) (edge₂ : ConcreteEmptyEdge M p q₂ suffix₂) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : SamePrefixEpsilonReturnData M p q₁ q₂ suffix₁ suffix₂

Build the full paired-anchor/two-tail residual directly from the constructor-exact epsilon edge and the other concrete empty edge.

theorem DPDA_to_LR.concreteTransitionEmptyReturn_samePrefix_state_eq_of_structural {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hstructural : SamePrefixEpsilonReturnsStateUnique M) {p : List (symbol T (Nonterminal M))} {q₁ q₂ : State M} {suffix₁ suffix₂ : List T} (edge₁ : ConcreteEmptyTransitionEdge M p q₁ suffix₁) (edge₂ : ConcreteEmptyEdge M p q₂ suffix₂) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂

Once the paired structural residual is discharged, every transition-generated empty return is synchronized with an arbitrary empty return at the same visible prefix.