PP ⊆ PSPACE — removing the rational threshold

⚠️ Unreviewed by Bolton

Membership in PP is stated as acceptProb > 1/2, a comparison of rationals. A machine has no rationals; it has a counter. Since acceptProb x T is acceptCount x T / 2 ^ T by definition, the threshold is equivalent to the integer comparison 2 ^ T < 2 · acceptCount x T, and both sides of that are things a machine can hold: the count needs T + 1 bits and the choice sequences it ranges over are T bits each.

What remains for the containment is the enumeration itself — a counter over the 2 ^ T choice sequences, one simulation per sequence, and a running tally — with the space reused between sequences.

Main results

• NTM.acceptProb_gt_half_iff — the threshold as an integer comparison
• PP_integer_characterization_internal — PP with no rational arithmetic left in it
• PP_subset_PSPACE_of_counter_internal — the containment, modulo one machine
• PP_subset_PSPACE_of_tallyMachine_internal — the same, with the obligation reduced to a machine deciding one arithmetic predicate
• PP_subset_PSPACE_of_iterateMachine_internal — and reduced further, to realising one iterated step function
• PP_subset_PSPACE_internal — the containment itself

theorem Complexity.NTM.acceptProb_gt_half_iff {k : ℕ} (tm : NTM k) (x : List Bool) (T : ℕ) : tm.acceptProb x T > 1 / 2 ↔ 2 ^ T < 2 * tm.acceptCount x T

The PP threshold is an integer comparison. More than half of the 2 ^ T choice sequences accept exactly when twice the accepting count exceeds 2 ^ T.

theorem Complexity.PP_integer_characterization_internal {L : Language} (hL : L ∈ PP) : ∃ (k : ℕ) (tm : NTM k) (f : ℕ → ℕ) (m : ℕ), tm.AllPathsHaltIn f ∧ (BigO f fun (x : ℕ) => x ^ m) ∧ ∀ (x : List Bool), x ∈ L ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)

PP with no rational arithmetic left. A language of PP is decided by comparing twice the number of accepting choice sequences against their total count — a comparison of two naturals of polynomially many bits.

theorem Complexity.PP_subset_PSPACE_of_counter_internal (h : ∀ (k : ℕ) (tm : NTM k) (f : ℕ → ℕ), tm.AllPathsHaltIn f → (∃ (m : ℕ), BigO f fun (x : ℕ) => x ^ m) → ∃ (k' : ℕ) (M : TM k') (q : Polynomial ℕ), (∀ (x : List Bool) (c' : Cfg k' M.Q), M.reaches (M.initCfg x) c' → c'.WithinDecisionSpace x.length (Polynomial.eval x.length q)) ∧ ∀ (x : List Bool), ∃ (c' : Cfg k' M.Q), M.reaches (M.initCfg x) c' ∧ M.halted c' ∧ (2 ^ f x.length < 2 * tm.acceptCount x (f x.length) → c'.output.cells 1 = Γ.one) ∧ (¬2 ^ f x.length < 2 * tm.acceptCount x (f x.length) → c'.output.cells 1 = Γ.zero)) : PP ⊆ PSPACE

PP ⊆ PSPACE, reduced to the existence of one machine. For each probabilistic machine and time bound, exhibit a deterministic machine that keeps a polynomial window and decides the integer comparison 2 ^ T < 2 · acceptCount — the rational threshold having already been eliminated. No probability, and no asymptotics, survive in the obligation.

theorem Complexity.PP_subset_PSPACE_of_tallyMachine_internal (h : ∀ (k : ℕ) (tm : NTM k) (f : ℕ → ℕ) (p : Polynomial ℕ), tm.AllPathsHaltIn f → (∀ (n : ℕ), f n ≤ Polynomial.eval n p) → ∃ (k' : ℕ) (M : TM k') (q : Polynomial ℕ), (∀ (x : List Bool) (c' : Cfg k' M.Q), M.reaches (M.initCfg x) c' → c'.WithinDecisionSpace x.length (Polynomial.eval x.length q)) ∧ ∀ (x : List Bool), ∃ (c' : Cfg k' M.Q), M.reaches (M.initCfg x) c' ∧ M.halted c' ∧ (NTM.tally (fun (v : ℕ) => !tm.acceptsAt x (Polynomial.eval x.length p) v) (2 ^ Polynomial.eval x.length p) < NTM.tally (fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v) (2 ^ Polynomial.eval x.length p) → c'.output.cells 1 = Γ.one) ∧ (¬NTM.tally (fun (v : ℕ) => !tm.acceptsAt x (Polynomial.eval x.length p) v) (2 ^ Polynomial.eval x.length p) < NTM.tally (fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v) (2 ^ Polynomial.eval x.length p) → c'.output.cells 1 = Γ.zero)) : PP ⊆ PSPACE

PP ⊆ PSPACE, reduced to a machine deciding one arithmetic predicate. The obligation no longer mentions probability, rationals, the function space Fin T → Bool, or the protocol's own time function: exhibit a machine keeping a polynomial window that decides whether the accepting tally exceeds the rejecting one over a computable horizon.

theorem Complexity.PP_subset_PSPACE_of_iterateMachine_internal (h : ∀ (k : ℕ) (tm : NTM k) (f : ℕ → ℕ) (p : Polynomial ℕ), tm.AllPathsHaltIn f → (∀ (n : ℕ), f n ≤ Polynomial.eval n p) → ∃ (k' : ℕ) (M : TM k') (q : Polynomial ℕ), (∀ (x : List Bool) (c' : Cfg k' M.Q), M.reaches (M.initCfg x) c' → c'.WithinDecisionSpace x.length (Polynomial.eval x.length q)) ∧ ∀ (x : List Bool), ∃ (c' : Cfg k' M.Q), M.reaches (M.initCfg x) c' ∧ M.halted c' ∧ (((NTM.tallyStep fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v)^[2 ^ Polynomial.eval x.length p] (0, 0, 0)).2.2 < ((NTM.tallyStep fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v)^[2 ^ Polynomial.eval x.length p] (0, 0, 0)).2.1 → c'.output.cells 1 = Γ.one) ∧ (¬((NTM.tallyStep fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v)^[2 ^ Polynomial.eval x.length p] (0, 0, 0)).2.2 < ((NTM.tallyStep fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v)^[2 ^ Polynomial.eval x.length p] (0, 0, 0)).2.1 → c'.output.cells 1 = Γ.zero)) : PP ⊆ PSPACE

PP ⊆ PSPACE, reduced to realising one iterated step function. The obligation is now as small as it can be made without building the machine: exhibit a machine keeping a polynomial window that decides whether, after 2 ^ p |x| iterations of NTM.tallyStep from the zero state, the accepting component exceeds the rejecting one. The machine's correctness proof therefore has to reason only about a single loop body, not about counting.

theorem Complexity.PP_subset_PSPACE_internal : PP ⊆ PSPACE

PP ⊆ PSPACE. The obligation of PP_subset_PSPACE_of_iterateMachine_internal is met by NTM.ppMachine: park, evaluate the horizon, then loop one simulation per counter value, keeping two tallies, and compare them. A source machine that starts halted has no accepting path at all, so that case is decided by NTM.zeroTM, which publishes 0 and stops.