Factoring global paths through the FS-to-ES drain

A global computation which reaches the fresh drain state has a unique semantic phase boundary: immediately before its first drain transition it is the lift of a final configuration of the normalized DPDA. This file retains both sides of that boundary—the normalized prefix and the literal FS-to-ES suffix—for later cut-comparison arguments.

theorem DPDA_to_LR.emptyStack_global_drain_factorization {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w input : List T} {drainStack : List (Option S)} (h : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inr 1, input := input, stack := drainStack }) : ∃ (p : Q × Bool) (delta : List S) (entryStack : List (Option S)), p ∈ M.firstFinal.final_states ∧ PDA.Reaches { state := M.firstFinal.initial_state, input := w, stack := [M.firstFinal.start_symbol] } { state := p, input := input, stack := delta } ∧ PDA.Reaches₁ (liftConf M.firstFinal.toPDA { state := p, input := input, stack := delta }) { state := Sum.inr 1, input := input, stack := entryStack } ∧ PDA.Reaches { state := Sum.inr 1, input := input, stack := entryStack } { state := Sum.inr 1, input := input, stack := drainStack }

A global path to an exact drain cut factors at its first drain entry into a normalized first-final computation and the literal remaining FS-to-ES path.