TheoremStatement: Literature-sourcedProof: AI-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Savitch's theorem: $N S P A C E (s (n))$ is contained in $D S P A C E (s (n)^{2})$

Statement

For every function $s : N \to N$ , every language in $N S P A C E (s (n))$ also lies in $D S P A C E (s (n)^{2})$ .

Facts & Assumptions

Given: a language $L \in N S P A C E (s (n))$ .

[L1]

By definition, $L \in N S P A C E (s (n))$ means that some fixed nondeterministic multitape machine decides $L$ while every branch uses $O (s (n))$ space (The classes DTIME, NTIME, DSPACE, and NSPACE).

[L2]

Such a machine has at most exponentially many configurations in its space bound (A machine using space s(n) has at most exponentially many configurations).

[L3]

The bounded reachability recursion is correct for paths of length at most $2^{i}$ (The bounded reachability recursion is correct).

[L4]

When a digraph has $N$ vertices, the recursion needs only $O (\log^{2} N)$ space, hence $O (s (n)^{2})$ space when $N \leq 2^{O (s (n))}$ (The bounded reachability recursion uses logarithmic recursion depth).

Proof

technique · direct

1.1L1construct

Let $M$ be the machine from [L1], and fix an input $x$ of length $n$ . Form the directed configuration graph $G_{x}$ : its vertices are the configurations of $M$ on $x$ , and there is an arc $C \to C^{'}$ exactly when one legal transition of $M$ moves from $C$ to $C^{'}$ . Let $C_{s t a r t} (x)$ be the start configuration. Then $x \in L$ if and only if some accepting configuration is reachable from $C_{s t a r t} (x)$ in $G_{x}$ .

2.1L2step 1.1algebra

By [L2], $G_{x}$ has at most $N_{x} \leq 2^{c s (n)}$ vertices for some constant $c$ depending only on $M$ . Any directed path with repeated vertices can be shortened by deleting directed cycles, so $x \in L$ if and only if $C_{s t a r t} (x)$ reaches some accepting configuration by a path of length at most $N_{x} - 1$ .

3.1L3step 2.1construct

A deterministic simulator can enumerate candidate accepting configurations $C$ one at a time and run the bounded reachability procedure on the triple $(G_{x}, C_{s t a r t} (x), C)$ with an index large enough to cover $N_{x} - 1$ . By [L3], that test answers the reachability question correctly for each candidate $C$ .

4.1L4step 3.1algebra

By [L4], each such reachability test uses $O (s (n)^{2})$ space. The simulator never stores the whole graph: it keeps only the current input, one or two configurations, the midpoint candidate, and the recursion stack; adjacency in $G_{x}$ is recomputed from the transition function of $M$ when needed. The outer loop over candidate accepting configurations adds only $O (s (n))$ more space. Hence the overall deterministic decider uses $O (s (n)^{2})$ space.

5.1step 4.1∎

Since the input $x$ was arbitrary, $L \in D S P A C E (s (n)^{2})$ . This proves $N S P A C E (s (n)) \subseteq D S P A C E (s (n)^{2})$ .

Depends on

Used by

PSPACE equals NPSPACE and is closed under complement Corollary

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach (standard reference, not scraped)
Eric Blais, Models of Computation, 17. Space Complexity (standard reference, not scraped)

Savitch's theorem: NSPACE(s(n))NSPACE(s(n)) is contained in DSPACE(s(n)2)DSPACE(s(n)2)