Assembly of the concrete empty-return classifier

Equality of the two terminally completed sentential forms leaves only two shapes: the visible prefixes agree, or one is a strict terminal extension of the other. Same-prefix transition returns are handled by the structural epsilon-return uniqueness theorem. This module isolates the one remaining ancestry statement for strict terminal extensions and proves all downstream classifier assembly from those two inputs.

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

Generic semantic interface expected from the paired-anchor interval argument. The two anchors represent the same visible frontier and completed word. If both physical cuts have useful futures with the same one-symbol lookahead, their control states and complete stacks agree.

Equations

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

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

Boundary-sensitive strengthening of physical cut equality. This is the form consumed directly by the existing leftmost-epsilon comparison API.

Equations

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

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

Equality of the boundary-sensitive anchor positions implies equality of their physical cuts.

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

The boundary-sensitive paired-anchor theorem is sufficient for the full same-prefix epsilon-return uniqueness property.

theorem DPDA_to_LR.zeroVisibleEmptyList_read_false_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} {emptyAnchor readAnchor : Nonterminal M} {emptyAnchorSuffix readAnchorSuffix emptySuffix readNodeSuffix readFutureSuffix : List T} {emptyAnchorContext readAnchorContext emptyContext readContext : List (StackSymbol M)} {emptyState source target next emptyFinal readFinal : State M} {a : T} {top : StackSymbol M} {replacement : List (StackSymbol M)} (emptyAnchorWitness : VisibleSpineAnchor M p emptyAnchor emptyAnchorSuffix completion emptyAnchorContext) (readAnchorWitness : VisibleSpineAnchor M p readAnchor readAnchorSuffix completion readAnchorContext) (emptyTail : ZeroVisibleTail M p completion emptyAnchor emptyAnchorSuffix emptyAnchorContext (PDA_to_CFG.N.list emptyState [] emptyState) emptySuffix emptyContext) (readTail : ZeroVisibleTail M p completion readAnchor readAnchorSuffix readAnchorContext (PDA_to_CFG.N.single source top target) readNodeSuffix readContext) (hposition : leftmostEpsilonPositionOf M emptyAnchor emptyAnchorContext = leftmostEpsilonPositionOf M readAnchor readAnchorContext) (readTransition : (next, replacement) ∈ (emptyStackPDA M).transition_fun source a top) (emptyUseful : PDA.Reaches { state := emptyState, input := emptySuffix, stack := emptyContext } { state := emptyFinal, input := [], stack := [] }) (readUseful : PDA.Reaches { state := source, input := a :: readFutureSuffix, stack := top :: readContext } { state := readFinal, input := [], stack := [] }) (hlook : List.take 1 emptySuffix = List.take 1 (a :: readFutureSuffix)) : False

From one physical zero-visible anchor, an empty-list endpoint cannot coexist productively with a single endpoint that has a useful read on the same lookahead.

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

The exact strict-prefix ancestry obligation left by the concrete empty-return classifier. The later visible prefix differs only by a nonempty terminal block. Such a pair must expose one of the useful cycle/growth obstructions.

The statement deliberately does not ask which edge is transition-generated: ConcreteEmptyEdge.transitionEdge_of_strictTerminalExtension already shows that the later edge is transition-generated.

Equations

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

inductive DPDA_to_LR.ConcreteNonreadEmptyEdge {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : List (symbol T (Nonterminal M)) → State M → List T → Prop

The non-read fragment of a concrete empty edge. A read-generated early edge is already incompatible with every strict terminal extension, so only epsilon and structural split-right introductions survive in the strict classifier.

• epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix preWord : List T} {context : List (StackSymbol M)} {source : State M} {Z : StackSymbol M} {q : State M} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.single source Z q) suffix preWord context) (transition : (q, []) ∈ (emptyStackPDA M).transition_fun' source Z) (rule : (PDA_to_CFG.N.single source Z q, [symbol.nonterminal (PDA_to_CFG.N.list q [] q)]) ∈ (characteristicGrammar M).rules) : ConcreteNonreadEmptyEdge M p q suffix
• split {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix preWord leftWord : List T} {context : List (StackSymbol M)} {source : State M} {Z : StackSymbol M} {q : State M} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.list source [Z] q) suffix preWord context) (length : ↑[Z].length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (rule : (PDA_to_CFG.N.list source [Z] q, [symbol.nonterminal (PDA_to_CFG.N.single source Z q), symbol.nonterminal (PDA_to_CFG.N.list q [] q)]) ∈ (characteristicGrammar M).rules) (left : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source Z q)] (List.map symbol.terminal leftWord)) : ConcreteNonreadEmptyEdge M (p ++ [symbol.nonterminal (PDA_to_CFG.N.single source Z q)]) q suffix

theorem DPDA_to_LR.ConcreteNonreadEmptyEdge.edge {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {q : State M} {suffix : List T} (edge : ConcreteNonreadEmptyEdge M p q suffix) : ConcreteEmptyEdge M p q suffix

Forget the non-read tag.

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

The actual strict-prefix residual after disposing of read-generated early edges.

Equations

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

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

Boundary-sensitive paired-anchor synchronization rules out every epsilon/split early return followed by a later transition return. Walking the later terminal block back to its first read produces a readable single at the early frontier; the earlier empty child and that single then descend from one structural epsilon position, contradicting useful determinism.

theorem DPDA_to_LR.strictTerminalEmptyReturnPairsClassified_of_nonread {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hnonread : StrictTerminalNonreadEmptyReturnPairsClassified M) : StrictTerminalEmptyReturnPairsClassified M

Read-generated early returns admit no strict terminal extension at all; hence the full strict classifier reduces to its epsilon/split fragment.

theorem DPDA_to_LR.concreteLeftTransitionReturnPairsClassified_of_structural {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hsame : SamePrefixEpsilonReturnsStateUnique M) (hstrict : StrictTerminalEmptyReturnPairsClassified M) : ConcreteLeftTransitionReturnPairsClassified M

The left-transition directional classifier follows from same-prefix epsilon-return uniqueness and the single strict-terminal ancestry property.

theorem DPDA_to_LR.concreteRightTransitionReturnPairsClassified_of_structural {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hsame : SamePrefixEpsilonReturnsStateUnique M) (hstrict : StrictTerminalEmptyReturnPairsClassified M) : ConcreteRightTransitionReturnPairsClassified M

The right-transition directional classifier has the same strict branch; only the same-prefix lookahead must be reversed before applying the structural transition-vs-return theorem.

theorem DPDA_to_LR.concreteEmptyReturnPairsClassified_of_structural {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hsame : SamePrefixEpsilonReturnsStateUnique M) (hstrict : StrictTerminalEmptyReturnPairsClassified M) : ConcreteEmptyReturnPairsClassified M

Complete concrete pair classification once the same-prefix and strict terminal ancestry statements have been supplied.

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

One boundary-sensitive paired-anchor synchronization theorem discharges both the same-prefix epsilon branch and every strict terminal displacement, and therefore supplies the complete concrete empty-return classifier.