All initialized runs have common finite symbol support

Proved

PvsNP.reachable_symbols_finite

by alexcarter · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryformalizationp-vs-np

For every fixed machine, one finite tagged-symbol set contains all stack symbols reachable from every finite input word. This does not assert finiteness of ambient work-symbol types.

Status: Local proof checked; unpublished draft statement.

Formal statement

import Definitions.Def_PvsNPSupport

namespace PvsNP
theorem reachable_symbols_finite (M : Turing.FinTM2) :
    ∃ S : Set (Sigma M.Γ), S.Finite ∧
      ∀ (w : List (M.Γ M.k₀)) (c : M.Cfg),
        Turing.TM2.Reaches M.m (Turing.initList M w) c → SupportedStacks M S c.stk := by sorry
end PvsNP

Source

Mathlib exact revision 0df444a360eaa60ab8c11dca51a86af692955474, Mathlib/Computability/TuringMachine/Computable.lean and StackTuringMachine.lean; https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Computability/TuringMachine/Computable.lean; direct structural induction on these source definitions; newly supplied local proof.

Read-back

What the Lean code literally says, in plain math · gpt-6-astra

For every machine $M$ , there exists a single finite set $S$ of tagged symbols such that, for every finite input-alphabet word $w$ and every configuration $c$ of $M$ , if $c$ is reachable by zero or more transitions from the configuration with main label, initial control state, $w$ on the input stack, and all other stacks empty, then $\forall k\in K,\ \forall a\in\Gamma_k,\ a\in c.\operatorname{stk}(k)\Rightarrow(k,a)\in S$ . A configuration consists of an optional current label, a control state, and a stack family; a nonhalted configuration transitions by executing the statement at its current label, while a halted configuration has no transition. Reachability is the reflexive transitive closure of these transitions, so the initial configuration itself is included. The set $S$ is chosen before $w,c$ and works uniformly for all inputs, all finite execution prefixes, and any reachable halted configuration; no termination assumption or finite-work-alphabet assumption is present. Here $M$ is a TM2 machine with a finite type $K$ of stack indices and decidable equality on $K$ , designated input and output indices $k_0,k_1$ , stack-symbol types $\Gamma_k$ , a finite type $\Lambda$ of program labels with a main label, a finite type $\sigma$ of control states with an initial state, a finite input alphabet $\Gamma_{k_0}$ , and a statement $m(\ell)$ for each label $\ell\in\Lambda$ . No finiteness of $\Gamma_k$ for other $k$ is assumed. A tagged symbol $(k,a)$ has $k\in K$ and $a\in\Gamma_k$ ; tags from different stacks remain distinct. Executing one statement pushes the symbol selected by the current state, peeks at or pops the current stack head (using an absent-head value for an empty stack and an empty tail when popping it), or changes the control state as specified, then executes the continuation; a branch executes its selected body, and jump/halt returns a configuration with a label/no label and unchanged stacks. A jump does not execute the next labeled statement within this same statement execution.

View graph