gpt 6 astra ultra attempt on CS-33

PSPACE versus EXPTIME

Definitions and mathematical statement

In the deterministic multitape model with read-only input, \[ \mathsf{PSPACE}=\bigcup_{k\ge1}\mathsf{DSPACE}(n^k),\qquad \mathsf{EXPTIME}=\bigcup_{k\ge1}\mathsf{DTIME}(2^{n^k}). \] All machines halt on every binary input; constant-factor changes in resource bounds are allowed. Determine whether these full unions are equal. A separation between one fixed space bound and one fixed time bound does not separate the two union classes.

Formulation and concept references: [S1].

Short English statement

Does polynomial working space suffice for every decision problem solvable in exponential time?

Research attempt

Process and first unproved step.

This GPT-6 Astra Ultra attempt was developed on 27 September 2026 by analyzing succinct alternating reachability, proving its fixed-point and certificate properties, and testing cyclic examples. The work gives a concrete sufficient compression statement for equality of the classes, not a proof of that statement. The first gap in this route is a uniform polynomial bound on circuit descriptions of winning regions, strategies, and decreasing ranks for every winning succinct reachability game. There is no argument here establishing that bound.

The hierarchy and machine facts are used with the union quantifiers in the statement. Chandra, Kozen, and Stockmeyer prove the relation between alternating space and deterministic exponential time [E1]; in particular $\mathsf{APSPACE}=\mathsf{EXPTIME}$. The standard space hierarchy theorem and configuration conventions are reviewed in [E2]. The withdrawn manuscript [S2] and its critique [S3] are preserved as catalogue sources and supply no separation theorem for this attempt.

The known containment with constants exposed.

Fix a deterministic machine $M$ that uses at most $c n^k$ work cells. With a fixed alphabet and fixed number of tapes, a configuration records the state, input-head position, work-head positions, and used work cells. Its encoding needs \[ O_M(n^k+\log n) \] bits. There are at most $2^{O_M(n^k+\log n)}$ configurations on an input of length $n$. A deterministic halting computation cannot revisit a configuration: a repeated configuration would repeat the same future indefinitely. Thus direct simulation decides its language in that exponential time, establishing $\mathsf{PSPACE}\subseteq\mathsf{EXPTIME}$. A larger fixed exponent absorbs the machine-dependent constant in the exponential, in agreement with the full-union definition.

The space hierarchy supplies, for each fixed $k$, languages requiring more than $O(n^k)$ space while still using a larger polynomial amount. These languages can all lie in $\mathsf{PSPACE}$. The quantifiers \[ \forall k\ \exists L_k\notin\mathsf{DSPACE}(n^k) \quad\hbox{and}\quad \exists L\ \forall k\ L\notin\mathsf{DSPACE}(n^k) \tag{90.1} \] are different. The former, even with every $L_k$ in exponential time, does not give the latter. We therefore examine one complete problem rather than a succession of unrelated fixed-bound diagonalizations.

A succinct game with exact acceptance semantics.

An instance contains Boolean circuits describing vertices $v\in\{0,1\}^s$, a target predicate $T(v)$, a type predicate designating existential or universal vertices, and two successors $c_0(v),c_1(v)$. Duplicate successors are allowed. There is a distinguished start vertex $a$. The input length $m$ includes these circuits and $s$, so $s\le m$. At an existential vertex the first player chooses a successor; at a universal vertex the opposing player chooses. Reaching a target wins for the first player. An infinite play avoiding targets loses. Targets terminate the play regardless of their encoded successors.

Put $N=2^s$, $W_0=T$, and \[ W_{i+1}=W_i\cup \{v\text{ existential}:\exists j\ c_j(v)\in W_i\} \cup \{v\text{ universal}:\forall j\ c_j(v)\in W_i\}. \tag{90.2} \] Because there are $N$ vertices, the sequence stabilizes by $W_N$.

Lemma. A vertex is winning if and only if it lies in $W_N$.

Proof. A target wins immediately. If a vertex first appears at stage $i+1$, an existential vertex has a successor appearing by stage $i$, while both successors of a universal vertex appear by then. Choose a decreasing-stage successor at existential positions. At each move before a target the least stage strictly decreases, proving a win in finitely many steps.

If $v\notin W_N$, an existential vertex has neither successor in $W_N$, and a universal vertex has at least one successor outside it. The second player chooses such a successor at universal positions. Every resulting play stays outside $W_N$, hence outside $T$, and cannot win for the first player. This proves the converse, including cycles. $\square$

Storing a membership bit for every vertex and scanning all vertices for each round computes $90.2$ in $2^{O(m)}$ times a polynomial in $m$, allowing a second array for simultaneous updates. The storage is exponential in $s$. This is an exponential-time upper bound, not a polynomial-space implementation.

Why this game captures the full question.

For a fixed alternating polynomial-space machine and input $x$, encode its configurations using polynomially many bits. Local transition, state-type, and acceptance tests have polynomial-size circuits constructible in polynomial time from $x$. Branches of degree greater than two can be expanded into a fixed binary branching gadget. Rejecting configurations become non-target self-loops; accepting configurations are targets. Malformed encodings are also made rejecting self-loops. The start configuration is the distinguished vertex.

An accepting alternating computation corresponds exactly to the least winning region in $90.2$. Thus alternating polynomial-space acceptance reduces to this succinct game. With the cited equality $\mathsf{APSPACE}=\mathsf{EXPTIME}$ and the explicit upper bound, the game language is $\mathsf{EXPTIME}$-complete under polynomial-time many-one reductions. Consequently a deterministic polynomial-space algorithm for all these games would prove equality of the two classes. Ordinary explicitly listed games have polynomial-time fixed-point algorithms; the exponentially larger implicit state set is what changes the resource accounting here.

A compression lemma with a completely checkable hypothesis.

A certificate for a winning start consists of functions \[ B:\{0,1\}^s\to\{0,1\},\qquad \sigma:\{0,1\}^s\to\{0,1\},\qquad r:\{0,1\}^s\to\{0,\ldots,N\}. \] Require $B(a)=1$. For every $v$ with $B(v)=1$ that is not a target, require the following local conditions. If $v$ is existential, its chosen successor $u=c_{\sigma(v)}(v)$ has $B(u)=1$ and $r(u)<r(v)$. If $v$ is universal, both successors have these properties. Values at targets and outside $B$ are unrestricted; ranks use $s+1$ output bits and must be at most $N$ on $B$.

These conditions are sound: starting in $B$, every play consistent with $\sigma$ remains there and strictly decreases a nonnegative integer until a target is reached. They are also complete without a size restriction: take $B=W_N$, take $r(v)$ to be the first stage containing $v$, and choose a suitable decreasing-stage successor at each existential vertex. Truth tables always describe these functions, but can use exponentially many bits.

Conditional compression lemma. If there is a fixed polynomial $p$ such that every winning instance of length $m$ has such a certificate with $B,\sigma,r$ computed by circuits of total size at most $p(m)$, then $\mathsf{PSPACE}=\mathsf{EXPTIME}$.

Proof. Enumerate every circuit triple up to the specified size bound. A triple and its evaluation workspace occupy polynomial space. For each triple, check the start condition and enumerate all $s$-bit vertices, evaluating the required local inequalities. The vertex counter uses $s+1$ bits, not $N$ bits. Reject invalid triples and accept when a valid one is found. Enumeration is finite. Soundness excludes acceptance on losing instances; the hypothesized size bound guarantees a triple on every winning instance. This is a deterministic polynomial-space decision procedure for the complete game language. Polynomial-time reductions preserve polynomial space, proving the claim. $\square$

The polynomial must be independent of the instance. Saying that each finite instance has a finite certificate, or allowing its exponent to depend on the instance, supplies no such algorithm. The compression hypothesis is sufficient; no converse or equivalence to the original question is claimed.

Two failed shortcuts.

First, treating the equations for acceptance as arbitrary Boolean fixed-point equations is unsound. One non-target existential vertex whose two successors are itself satisfies $b=b$. Both $b=0$ and $b=1$ solve the equation, but only $b=0$ has the required least-fixed-point semantics. A candidate strategy that simply remains on this loop is not a winning certificate; a strict integer rank cannot exist around the cycle. This is why ranks cannot be removed from the local test.

Second, polynomial-size transition circuits do not by themselves imply polynomial-size circuits for the iterated fixed point. Writing a separate circuit for each of the up to $2^s$ rounds can already introduce exponentially many layers. Unrolling the entire tree of choices is even larger. Recomputing values instead of storing them requires an analysis of the recursion stack; a path may have exponential length, so the obvious depth-first implementation has no polynomial-space guarantee. None of these observations proves a circuit lower bound: they locate the failure of these particular constructions.

Verification and outcome.

The local certificate conditions and increasing-stage construction were checked on all games with three labelled vertices, two ordered successors per vertex, arbitrary target sets, and arbitrary vertex types. The accompanying exact script checks every vertex, losing-region closure, decreasing-rank certificates, and the self-loop countertest. These finite tests examine the lemmas; they provide no evidence for a uniform polynomial compression theorem.

UNRESOLVED. The game reduction, least-fixed-point proof, and conditional compression lemma are established with the stated literature input. The first missing theorem is the polynomial circuit bound on the certificates. A separation would instead need one exponential-time language outside every polynomial space bound; neither direction is achieved by this attempt.

Sources

• S1 Alberto Pettorossi, Elements of Computability, Decidability, and Complexity, Third Edition, printed115, item(iii); Arora–Barak Chapter4 machine conventions. https://art.torvergata.it/bitstream/2108/32769/60437/ComputabilityDecidabilityComplexity.pdf. Formulation source.
• S2 Separation of PSPACE and EXP (withdrawn). https://arxiv.org/abs/2104.14316. Further reference; not a proof endorsement.
• S3 A Critique of Czerwinski's Separation of PSPACE and EXP. https://arxiv.org/abs/2304.14575. Further reference; not a proof endorsement.
• E1 A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer, Alternation, Journal of the ACM 28 $1981$, 114--133, DOI 10.1145/322234.322243. https://www.cs.cornell.edu/kozen/Papers/papers_by_year.htm. Author's publication record; alternating polynomial space equals exponential time.
• E2 S. Arora and B. Barak, Computational Complexity: A Modern Approach, author-hosted draft, Chapters 3--5, especially Chapter 5, Exercise 6 and the discussion preceding it. https://theory.cs.princeton.edu/complexity/book.pdf. Configuration, hierarchy, and alternation conventions; consulted 27 September 2026.