PromiseBPTIME hierarchy by delayed diagonalization (and the one-bit-advice BPTIME program) #2084

Samuel asked for a BPTIME hierarchy theorem. The advice-free hierarchy for languages, BPTIME(n^a) ⊊ BPTIME(n^b), is open, and this issue does not claim it. The target is the strongest advice-free statement that is known: the hierarchy for promise problems (PromiseBPTIME), proved by Žák's delayed diagonalization. The one-bit-advice hierarchy for languages is the follow-up program.

Owner: worker-claude-e6cf7b0d-bptime-hier (Claude Code, Opus), under coordinator-claude-e6cf7b0d. Branch claude/bptime-hierarchy.

Survey

I checked the first five sources below myself, in the PDFs at the stated ECCC numbers. For the last three I did not have the PDF.

• The advice-free problem is open. van Melkebeek and Pervyshev, ECCC TR05-111 (14 September 2005), §1: "it remains open whether for every constant c there exists a language that can be solved on randomized machines with two-sided error in polynomial time but not in time n^c". The obstacle is that bounded error is a semantic promise: simulating a machine whose acceptance probability is near 1/2 breaks the promise for the diagonalizer.
• Promise problems: known, by delayed diagonalization. S. He, A note on a hierarchy theorem for promise-BPTIME, ECCC TR25-004 (17 January 2025).
  • Theorem 1 (§2.1): pr-BPTIME[t(n)] ⊊ pr-BPTIME[t(n+1) log t(n+1)] for time-constructible increasing t(n) ≥ n. The proof is Žák's lazy diagonalization on unary inputs. Below the end of an interval, the input is a yes- (no-) instance when the simulated machine accepts (rejects) the next input with probability ≥ 2/3. The last input is decided deterministically against the first, so it is always inside the promise. Then the promise propagates down the chain.
  • Theorem 3 (§2.2), credited to Santhanam: BPP/a(n) ⊄ BPTIME[n^c]/b(n) implies pr-BPP ⊄ pr-BPTIME[n^c].
  • Corollary 5: pr-BPTIME[n^d] ⊄ pr-BPTIME[n^c] for d > c ≥ 1, by padding.
  • Appendix A: naive diagonalization, and Barak's argument from a complete problem, do not carry over to promise problems. The negation of an answer outside the promise stays outside it.
• One bit of advice (languages). van Melkebeek–Pervyshev, ECCC TR05-111 (journal version: Computational Complexity 16, 2007, journal pages not checked).
  • Theorem 1: for every reasonable semantic model and constants a, c, some language is in polynomial time with 1 bit of advice but not in time n^c with a bits.
  • Theorem 2: n^c versus n^d with a bits of advice on both sides, for any rationals 1 ≤ c < d.
  • The proof (§4.3, padding §4.4) is delayed diagonalization with a copying tree. It relativizes, and §2 notes that instance checkers are not needed for two-sided error.
• Logarithmic advice, general promise classes. Fortnow, Santhanam and Trevisan, Promise hierarchies, ECCC TR04-098, Theorem 1: CTIME(n^α)/b(n) ⊊ CTIME(n^γ)/b(n) with b(n) = O(log n log log n). Here "promise class" means a semantic class of languages, not a class of promise problems.
• Heuristic hierarchies. Pervyshev, On heuristic time hierarchies, ECCC TR06-131: heuristic hierarchies for NP, AM and MA. Its introduction attributes a (1−1/n^a)-heuristic hierarchy for BPP to Fortnow–Santhanam (FOCS 2004).
• Not accessed; locators not verified:
  • Barak (RANDOM 2002): O(log log n) advice through instance checkers for EXP-complete problems. Also the conditional theorem that a BPP-complete problem gives BPTIME(t) ⊊ BPTIME(t^c); He cites it as Theorem 3.6 of Barak.
  • Fortnow–Santhanam (FOCS 2004): BPP/1 ⊄ BPTIME(n^c)/1.
  • Goldreich–Sudan–Trevisan, ECCC TR04-093: reducing logarithmic advice to one bit. The ECCC PDF's text could not be extracted.

Choice

The target is (a), the PromiseBPTIME hierarchy, by Žák's argument following He's Theorem 1.

• It is the strongest advice-free statement known.

• It uses only diagonalization, which relativizes.

• It maps one-to-one onto the library's nondeterministic lazy-diagonal pipeline:

  • feat(Classes/Time): explicit-time verifier characterization of NTIME #2025: explicit-time verifiers and the pair sampler;
  • feat(Classes/Hierarchy): coarse nondeterministic time hierarchy by lazy diagonalization #2031: the lazy diagonal through the universal function with a clock;
  • feat(Classes/Hierarchy): nondeterministic time hierarchy at every integer degree #2036: padding amplification to every integer degree.

  Guess-and-verify becomes sample-and-verify. The brute-force existential at the end of an interval becomes a brute-force accepting count.

The two alternatives:

• (c) One bit of advice, vMP Theorem 2 with a = 1. This is the follow-on program. It needs the same toolkit plus advice classes and the copying tree. Instance checkers, which the library lacks, are not required.
• (b) The conditional "BPP-complete ⇒ hierarchy". It is recorded here but not planned. Its hypothesis is open.

Lean statements

M1. Definitions and explicit-time verifier characterization. This is the analogue of #2025. The new module is Classes/Promise/Time.lean.

def Turing.MultiTapePTM.SolvesWithBoundedErrorInTime (machine : MultiTapePTM k Bool State)
    (enc : α ↪ List Bool) (Q : PromiseProblem α) (t : α → ℕ) : Prop :=
  ∀ a, (∀ final ∈ (ProbComp.eval (machine.runClosedConfigFrom (t a)
      (machine.initialConfig (enc a)))).support, final.tapes.state = none) ∧
    (a ∈ Q.yes → 2 / 3 ≤ ProbComp.eval (machine.runClosed (t a) (enc a)) [true]) ∧
    (a ∈ Q.no → 2 / 3 ≤ ProbComp.eval (machine.runClosed (t a) (enc a)) [false])

def PromiseBPTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (PromiseProblem α) :=
  {Q | ∃ c₁ c₂ : ℕ, ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State),
    machine.SolvesWithBoundedErrorInTime enc Q fun a => c₁ * t (enc a).length + c₂}

theorem ofSet_mem_PromiseBPTIME_iff : ofSet A ∈ PromiseBPTIME enc t ↔ A ∈ BPTIME enc t
-- sample and verify (yes: 2·2^ℓ ≤ 3·acceptCount V a ℓ; no: the same for `!V`)
theorem mem_PromiseBPTIME_of_verifier ... : Q ∈ PromiseBPTIME enc t
-- coin replay: a linear-time verifier, valid for every coin length L ≥ c * t n + c
theorem exists_verifier_of_mem_PromiseBPTIME (hQ : Q ∈ PromiseBPTIME enc t) : ∃ V c, ...

Halting is required on every instance, as in BPTIME and PromiseBPP; correctness only on the promise. The time bounds are explicit up to the class's constants, and no existential absorbs the bound.

M2. Coarse hierarchy. This is the analogue of #2031.

def promiseLazyDiagonal (d : ℕ) : PromiseProblem (List Bool)
theorem promiseLazyDiagonal_mem_PromiseBPTIME (d : ℕ) :
    promiseLazyDiagonal d ∈ PromiseBPTIME encBits fun n => (n + 1) ^ e(d)   -- explicit e(d)
theorem promiseLazyDiagonal_notMem_PromiseBPTIME (d : ℕ) :
    promiseLazyDiagonal d ∉ PromiseBPTIME encBits fun n => (n + 1) ^ d
theorem PromiseBPTIME_succ_pow_ssubset_PromiseBPTIME_succ_pow_of_le (h : e(d) ≤ e') : ...

The diagonal works as follows.

• Below the end of the interval of a padded description, an input is a yes- (no-) instance when at least 2/3 of the coin strings make the described verifier accept (reject) the input one bit longer, with a clock.
• At the end of the interval, the input is a yes-instance exactly when fewer than half of the coin strings make the described verifier accept the first input. The diagonal counts this deterministically by brute force (ComputableInO.iterate over acceptCountStep), so the last input is always inside the promise.

M3. Every integer degree. This is the analogue of #2036 (He's Corollary 5, at integer degrees).

theorem PromiseBPTIME_pow_ssubset_PromiseBPTIME_pow {a b : ℕ} (ha : 1 ≤ a) (hab : a < b) :
    PromiseBPTIME encBits (· ^ a) ⊂ PromiseBPTIME encBits (· ^ b)

M4 (program). One bit of advice. This is vMP Theorem 2 with a = 1. It needs a semantic advice class BPTIME enc t / 1, where the machine must keep the promise only with the correct advice (vMP §4.1). The copying tree of §4.3 reuses the M1–M3 toolkit.

Optional small corollary. DTIME ⊆ BPTIME together with BPTIME_ssubset_DTIME_two_pow (#2054) gives the language-level BPTIME[T] ⊊ BPTIME[2^T]. That is an honest exponential-gap hierarchy, not the open polynomial one.

Missing from the library

• Promise problems of bounded-error time classes: only PromiseBPP exists.
• An explicit-time sample-and-verify characterization of BPTIME. Only the polynomial PPT compiler exists, and it loses the degree.
• A brute-force accepting count in time 2^O(n + ℓ). computableInPolySpace_acceptCount bounds only space.
• Advice classes for semantic models (needed for M4).
• Not needed: instance checkers, IP = PSPACE (already on main), and a probabilistic universal machine. The diagonal samples coins and runs the deterministic universal function on coin-replay verifiers.

Dependencies: M1 stacks on #2025 (approved), and M2 on #2031.