Polynomial-space ordered folds over bitstrings

SpaceIter.mem_PSPACE_of_bitstring_fold folds over exponentially many fixed-width candidates using a polynomial-time update and a polynomial-size accumulator. Every prefix accumulator, including the seed and final value, must satisfy the stated bound. A polynomial-time test of the result defines a language in PSPACE.

Candidates have exactly w.eval x.length bits and are visited in increasing little-endian numeric order. There is one candidate even at width zero. Empty accumulators are allowed, and no algebraic laws on the update are required.

The proof uses initializedStep and SpaceIter.mem_PSPACE_of_iterate. Its packed states have length at most 4*W + 2*V + |x| + 22, and completion is signalled at iteration 2^W + 1. This is a depth-one exponential fold; a polynomial-depth game-tree evaluator still requires a stack construction.

theorem Complexity.SpaceIter.mem_PSPACE_of_bitstring_fold {seed : List Bool → List Bool} {update : List Bool → List Bool → List Bool → List Bool} {accept : List Bool → List Bool → Bool} (w v : Polynomial ℕ) (hs : seed ∈ FP) (hu : (fun (z : List Bool) => update (pairFst z) (pairFst (pairSnd z)) (pairSnd (pairSnd z))) ∈ FP) (ha : (fun (z : List Bool) => [accept (pairFst z) (pairSnd z)]) ∈ FP) (hbound : ∀ (x : List Bool), ∀ i ≤ 2 ^ Polynomial.eval x.length w, (bitstringFoldPrefix (update x) (seed x) (Polynomial.eval x.length w) i).length ≤ Polynomial.eval x.length v) : {x : List Bool | accept x (bitstringFold (update x) (seed x) (Polynomial.eval x.length w)) = true} ∈ PSPACE

An ordered fold over all polynomial-width bitstrings is computable for decision purposes in polynomial space. The update receives pair x (pair c a); the final test receives pair x a. All accumulator prefixes must be short.

theorem Complexity.SpaceIter.mem_PSPACE_of_exists_bitstring {p : List Bool → List Bool → Bool} (w : Polynomial ℕ) (hp : (fun (z : List Bool) => [p (pairFst z) (pairSnd z)]) ∈ FP) : {x : List Bool | ∃ (c : List Bool), c.length = Polynomial.eval x.length w ∧ p x c = true} ∈ PSPACE

Fixed-width witness search is the Boolean-OR instance of the ordered fold. The polynomial-time predicate receives pair x candidate; width zero tests [].

Small kernel-checked examples fix the order and boundary conventions.