Counted retained-frame intervals for characteristic spines

This file records the exact counted intervals which are still implicit in zero-visible spine tails and concrete empty-return edges. In both cases the selected run stays strictly above a named outer stack context, so that later comparison arguments may split or reframe the interval without reconstructing an existential reachability witness.

theorem DPDA_to_LR.ZeroVisibleTail.exists_retainedFrameRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord : List T} {anchor current : Nonterminal M} {anchorSuffix currentSuffix : List T} {anchorContext currentContext : List (StackSymbol M)} (hanchor : VisibleSpineAnchor M p anchor anchorSuffix preWord anchorContext) (htail : ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext current currentSuffix currentContext) : ∃ (n : ℕ), (emptyStackPDA M).RetainedFrameRun anchorContext n { state := spineCutState M anchor, input := [], stack := spineCutStack M anchor anchorContext } { state := spineCutState M current, input := [], stack := spineCutStack M current currentContext }

A zero-visible tail is a counted run which retains the complete hidden context of its visible anchor. Structural start and splitLeft steps cost zero PDA steps; every epsilon constructor contributes exactly one step.

theorem DPDA_to_LR.VisibleSpineAnchor.exists_countedZeroVisibleInterval {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord : List T} {anchor current : Nonterminal M} {anchorSuffix currentSuffix : List T} {anchorContext currentContext : List (StackSymbol M)} (hanchor : VisibleSpineAnchor M p anchor anchorSuffix preWord anchorContext) (htail : ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext current currentSuffix currentContext) : ∃ (prefixSteps : ℕ) (tailSteps : ℕ), PDA.ReachesIn prefixSteps { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := spineCutState M anchor, input := [], stack := spineCutStack M anchor anchorContext } ∧ (emptyStackPDA M).RetainedFrameRun anchorContext tailSteps { state := spineCutState M anchor, input := [], stack := spineCutStack M anchor anchorContext } { state := spineCutState M current, input := [], stack := spineCutStack M current currentContext } ∧ PDA.ReachesIn (prefixSteps + tailSteps) { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := spineCutState M current, input := [], stack := spineCutStack M current currentContext }

Counted global position of a zero-visible interval, together with its retained-frame subrun.

def DPDA_to_LR.CountedConcreteEmptyReturnInterval {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (completion suffix : List T) (q : State M) : Prop

Counted factorization of a concrete empty return. prefixSteps locates the parent cut globally, while the positive returnSteps interval pops the selected top symbol without touching context.

Equations

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

theorem DPDA_to_LR.ConcreteEmptyEdge.countedReturnIntervalAtCompletion {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 completion : List T} (edge : ConcreteEmptyEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)) : CountedConcreteEmptyReturnInterval M completion suffix q

Every concrete empty edge exposes a counted positive retained-frame return interval at any chosen completion of its visible prefix.

theorem DPDA_to_LR.CountedConcreteEmptyReturnInterval.exists_globalRunIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {completion suffix : List T} {q : State M} (h : CountedConcreteEmptyReturnInterval M completion suffix q) : ∃ (context : List (StackSymbol M)) (final : State M) (prefixSteps : ℕ) (returnSteps : ℕ), 0 < returnSteps ∧ PDA.ReachesIn (prefixSteps + returnSteps) { state := (emptyStackPDA M).initial_state, input := completion, stack := [(emptyStackPDA M).start_symbol] } { state := q, input := [], stack := context } ∧ PDA.Reaches { state := q, input := suffix, stack := context } { state := final, input := [], stack := [] }

Concatenating the counted prefix and retained return locates the empty child cut after exactly prefixSteps + returnSteps PDA steps.