QSAT is PSPACE-hard

The reduction of SUCCINCT-REACH to QSAT is correct (DescriptiveComplexity.qsatHolds_iff), so the interpretation of DescriptiveComplexity.Problems.Qsat.Interp is an ordered first-order reduction (DescriptiveComplexity.succinctReach_ordered_fo_reduction_qsat) and QSAT is PSPACE-complete (DescriptiveComplexity.QSAT_PSPACE_complete).

Peeling the first block – the two endpoints of the walk – opens the position of the first level, which DescriptiveComplexity.game_level says computes reachability in at most 2 ^ m moves for m the number of state variables; and that is reachability, by DescriptiveComplexity.succinctReachable_iff_savPow. An instance with no state variable has no level at all: the first block and every level block are empty, so the initial position is the position of the last block, and DescriptiveComplexity.game_aux answers directly.

theorem DescriptiveComplexity.qsatHolds_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : QsatHolds (QM A) ↔ SuccinctReachable A

Correctness of the Savitch reduction.

theorem DescriptiveComplexity.qsat_PSPACE_hard : PSPACE.Hard QSAT

QSAT is PSPACE-hard, by Savitch's recursive doubling from SUCCINCT-REACH.

theorem DescriptiveComplexity.QSAT_PSPACE_complete : PSPACE.Complete QSAT

QSAT is PSPACE-complete (Stockmeyer–Meyer 1973).