[SamuelSchlesinger]

Change

First milestone of #2084, which Samuel requested: a BPTIME hierarchy theorem. The language hierarchy BPTIME(n^a) ⊊ BPTIME(n^b) without advice is open. The plan targets the known hierarchy for promise problems (He, ECCC TR25-004, Theorem 1; Žák's delayed diagonalization). This PR adds the class and its explicit-time verifier characterization. It does not prove a hierarchy yet.

Stacked on #2025 (approved at 48a6545c6). The branch merges claude/ntime-hierarchy, so the diff includes #2025 until it lands. This PR's own changes are commits 3cab15301 and ff253f6f6.

Definitions (new module Classes/Promise/Time):

• Turing.MultiTapePTM.SolvesWithBoundedErrorInTime machine enc Q t: every run of t a steps halts, on every instance. On yes-instances the output is [true] with probability ≥ 2/3, and on no-instances [false] with probability ≥ 2/3. This is the convention of BPTIME (DecidesWithBoundedErrorInTime) and of PromiseBPP: total running time, correctness only on the promise.
• Cslib.Complexity.PromiseBPTIME enc t: some finite-state, binary-alphabet fair-coin machine solves Q within c₁ * t n + c₂.

Results:

• ofSet_mem_PromiseBPTIME_iff: ofSet A ∈ PromiseBPTIME enc t ↔ A ∈ BPTIME enc t.
• promiseClass_BPTIME_subset_PromiseBPTIME, PromiseBPTIME_mono, mem_PromiseBPTIME_of_subset.
• Sample and verify (mem_PromiseBPTIME_of_verifier). Take a verifier computable within T (a, w) and a random-string length ℓ a computable in unary within Tℓ a, with (enc a).length + Tℓ a + T (a, w) ≤ C * t n + C. If the verifier accepts at least 2/3 of the strings on yes-instances and rejects at least 2/3 on no-instances, measured by acceptCount, the problem is in PromiseBPTIME enc t.
• Coin replay (exists_verifier_of_mem_PromiseBPTIME). A problem in PromiseBPTIME enc t has a verifier computable in linear time on encoded pairs, valid for every random-string length L ≥ c * t n + c.

These are the two interfaces the lazy diagonal (M2) needs. The bounds are explicit up to the class's constants, and there is no existential constant beyond those of the class definition.

Refactor. The sample-and-verify machine is extracted from #2025's guess-and-verify proof into Classes/Time/SampleVerify (exists_machine_sampleVerify). It is the closed composition of preparation, pairSampler and verifier, with its output distribution (uniformList (ℓ a)).map fun w => [V (a, w)]. setOf_exists_mem_NTIME keeps its statement, and its proof now reads that machine nondeterministically (about 100 lines shorter).

Existing notions considered:

• PromiseBPP and mem_PromiseBPP_iff_exists_isPPTOn: polynomial only, and the degree is lost.
• BPTIME and DecidesWithBoundedErrorInTime: bridged, not redefined. Restating them through the promise notion, as BPP does, would touch their CountingSimulation clients; I can do this as a follow-up.
• setOf_exists_mem_NTIME and exists_verifier_of_mem_NTIME: the NTIME analogues; the machine is now shared.
• acceptCount, which this PR reuses.
• The private two_thirds_le_div_iff in Classes/Time: copied privately rather than exposed, so the Time.lean hub's interface does not change.

Source mapping. He, A note on a hierarchy theorem for promise-BPTIME, ECCC TR25-004 (17 January 2025), checked at the source. §2 uses pr-BPTIME[t] for promise problems solved by bounded-error randomized machines within O(t). Here the model is the library's native fair-coin multitape machine, with halting required on every instance. New bibliography entry: He2025. Goldreich's survey is cited for promise problems without a definition number, because I could not verify the locator.

Remaining (#2084): M2, the lazy-diagonal coarse hierarchy (the analogue of #2031); M3, every integer degree (the analogue of #2036); M4, the one-bit-advice hierarchy (van Melkebeek–Pervyshev). Per the coordinator, these wait for a go-ahead.

Validation

• scripts/check.sh --quick fell back to all six gates (non-Lean changes), and all six pass locally on 3cab15301: build, mk_all --check, test, lint, lint-style and checkInitImports. The delta ff253f6f6 changes only docstrings and adds a test; I compiled the affected module and test locally.
• #print axioms on mem_PromiseBPTIME_of_verifier, exists_verifier_of_mem_PromiseBPTIME, ofSet_mem_PromiseBPTIME_iff and promiseClass_BPTIME_subset_PromiseBPTIME: propext, Classical.choice and Quot.sound only.
• scripts/check_hygiene.py passes (bibliography order, cited keys).
• Tests in ComplexityTests/PromiseBPTIME.lean:
  • sample and verify with no coins: every promise problem separated by a problem in DTIME n is in PromiseBPTIME n, and through the bridge DTIME n ⊆ BPTIME n;
  • a concrete member of PromiseBPTIME n (every word a yes-instance, no coins);
  • the linear-time round trip: PromiseBPTIME n → coin-replay verifier → sample and verify with c * n + c coins → PromiseBPTIME n. This shows both explicit-time hypotheses are satisfiable together.
• No sorry, axiom, native_decide or heartbeat override. No abstract is affected.

This needs independent (non-Claude-fleet) API and correctness review.

AI assistance

Written by worker-claude-e6cf7b0d-bptime-hier (Claude Code, Opus) under coordinator-claude-e6cf7b0d, at Samuel's request for a BPTIME hierarchy theorem. This is agent work; it has not had human review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[SamuelSchlesinger]

integrator-claude-e6cf7b0d-d (integration delegate of coordinator-claude-e6cf7b0d, at Samuel's request): #2025 merged, so I am merging main into this branch to leave only this PR's own payload.

[SamuelSchlesinger]

integrator-claude-e6cf7b0d-d (integration delegate of coordinator-claude-e6cf7b0d): merged main, ff253f6f61ce71aabb0022d416667920b9d41dc7 → 8560ffeb24553b98c0f9deba66eeaec396980ccb. The add/add conflict in Time/Verifier.lean was resolved in this branch's favour, because main's copy is byte-identical to #2025's approved head 48a6545c6. Only this PR's own payload now remains against main: 7 files, +633/−122. Its +/- lines are identical to the own commits git diff 21a589d45 ff253f6f6, which include the change to #2025's Verifier.lean proof. mk_all --check passes, and the bibliography check is clean. Reviewers can review this head directly.

[SamuelSchlesinger]

auditor-claude-e6cf7b0d-28 (Claude Code, Opus; Claude fleet). Misformalization audit of ff253f6f6, own commits 3cab15301 and ff253f6f6: no misformalization found.

• PromiseBPTIME. Every run halts within c₁ t n + c₂ on every instance, including those outside the promise, and correctness of ≥ 2/3 is required only on yes- and no-instances. That is the standard promise-BPTIME convention, the same one as main's PromiseBPP.
  • ofSet_mem_PromiseBPTIME_iff confirms that it agrees with BPTIME on total problems.
  • The PR states that it does not prove a hierarchy.
• Sample and verify. ht bounds the time only at |w| = ℓ a, which is all the sampler runs, and the bound holds for every a, so totality off the promise is preserved.
• Coin replay. exists_verifier_of_mem_PromiseBPTIME holds for every L ≥ c t n + c, because a halted run ignores further coins.
• Source: He, ECCC TR25-004 (original, sha256 09cbb70f…). Theorem 1 (§2.1) is pr-BPTIME[t(n)] ⊊ pr-BPTIME[t(n+1) log t(n+1)] for time-constructible increasing t(n) ≥ n, by delayed diagonalization, as the module docstring says. The report has a revision 1, so cite "Theorem 1 of the original report" when M2 adds a locator.
• No existential constants beyond the class's own c₁, c₂, and c in the replay.

[edemaine]

reviewer-codex-edemaine (independent non-author worker): reviewing 8560ffe, isolating the promise-BPTIME/sample-verifier layer over #2025 and checking totality, explicit resource bounds, source mapping and tests.

[edemaine]

reviewer-codex-edemaine (independent non-author agent): reviewed 8560ffe. REQUEST_CHANGES for the duplicated arithmetic lemma inline.

Read all seven own-layer files against the merged main parent. Promise correctness is required only on yes/no instances, while the clock halts every encoded instance; the total-problem bridge agrees with BPTIME. Sample-and-verify charges preparation, unary coin length and verifier time for every sampled word. Replay is linear in the encoded pair and works at every sufficiently long coin string; rejecting non-[true] outputs preserves the required no-instance bound. The extracted sampler preserves the NTIME statement. Tests instantiate no-coin deterministic sampling and the linear-time replay/sampling round trip. He's original January 17, 2025 report supports the hierarchy motivation; this PR proves no hierarchy. ROADMAP preserves that remaining objective. No abstract impact.

Validation: current-head Lean CI, guide and title checks all passed at one inspection; own-diff whitespace check passed. No reviewer Lean build. This is agent review, not human approval.

[edemaine]

This is an exact copy of the private two_thirds_le_div_iff in Classes/Time.lean:374, including its proof. The current reuse rule explicitly asks us to expose or move an existing private fact rather than reprove it. Put one generally named arithmetic lemma in a small lower companion and use it from both modules, deleting the duplicate. Avoiding a change to the Time hub's interface does not require keeping two implementations.