Sharper counting separations: NTIME/BPTIME/PPTIME[T·h] ⊊ DTIME[2^T] for h = o(√log T) #2093

Samuel asked for this follow-up to #2054: strengthen its separations from NTIME[T] ⊊ DTIME[2 ^ T] to NTIME[T · h] ⊊ DTIME[2 ^ T] for every factor h = o(√log T), and likewise for BPTIME, PPTIME, ⊕TIME, Mod_kTIME and C₌TIME.

Claimed by worker-claude-e6cf7b0d-sharpsep (Claude Code, Opus), on branch claude/sharper-counting-separations.

Statements

Separation.lean is generalized in place. The union now runs over the scale of a second bound t, under the hypothesis t / √⌊log₂ t⌋ = o(T). The #2054 statements are the case t = T.

theorem ssubset_DTIME_two_pow_of_subset_iUnion {𝒞 : Set (Set (List Bool))}
    (hT : TimeConstructible T) (hTn : ∀ n, n ≤ T n)
    (hTt : ∀ C, ∀ᶠ n in atTop, C * t n ≤ T n * Nat.sqrt (Nat.log 2 (t n)))
    (h : 𝒞 ⊆ ⋃ C, DTIME encBits fun n => 2 ^ (C * t n / Nat.sqrt (Nat.log 2 (t n)))) :
    𝒞 ⊂ DTIME encBits fun n => 2 ^ T n

The new class statements take a factor h ≥ 1 with h = o(√⌊log₂ T⌋):

theorem NTIME_mul_ssubset_DTIME_two_pow {h : ℕ → ℕ} (hT : TimeConstructible T)
    (hTn : ∀ n, max n 2 ≤ T n) (hTh : TimeConstructible fun n => T n * h n)
    (hh₁ : ∀ n, 1 ≤ h n) (hh : ∀ C, ∀ᶠ n in atTop, C * h n ≤ Nat.sqrt (Nat.log 2 (T n))) :
    NTIME encBits (fun n => T n * h n) ⊂ DTIME encBits fun n => 2 ^ T n

BPTIME, PPTIME, ParityTIME, ModTIME k and CeqTIME get the same statement. A factor g (T n) with g = o(√log) on ℕ is a special case.

The concrete corollary uses h = ⌊⌊log₂ T⌋^{1/4}⌋. Its time-constructibility is proved, so the only hypotheses are those of #2054:

theorem NTIME_mul_sqrt_sqrt_log_two_ssubset_DTIME_two_pow (hT : TimeConstructible T)
    (hTn : ∀ n, max n 2 ≤ T n) :
    NTIME encBits (fun n => T n * Nat.sqrt (Nat.sqrt (Nat.log 2 (T n)))) ⊂
      DTIME encBits fun n => 2 ^ T n

BPTIME and PPTIME get the same corollary.

Proof sketch, and why o(√log T)

The counting simulation (#1995, #2041) at t = T · h gives NTIME[t] ⊆ ⋃ C, DTIME[2 ^ (C t / √⌊log₂ t⌋)]. The constant C depends on the machine: its tapes, its states and the constant c₁ in NTIME's O(t) bound (Classes/Time.lean). Because h ≥ 1, we have √⌊log₂ t⌋ ≥ √⌊log₂ T⌋. So 8 C t ≤ T √⌊log₂ t⌋ holds eventually, for every C, as soon as 8 C h ≤ √⌊log₂ T⌋ eventually. That is the hypothesis h = o(√log T).

Then each exponent C t / √log t is eventually at most T / 8. The clocked diagonal with clock 2 ^ (T / 4) from #2054 therefore lies in DTIME[2 ^ T] and outside every member of the union. Only Separation.lean's exponent bound changes; the diagonal and the universal-machine overhead are untouched.

o(√log T) is the limit of this argument. For h = ε √log T, the exponents are about C ε T, and C is unbounded over machines. Then no single clock 2 ^ (T / 4) beats every member of the union.

The hypotheses are needed as stated:

• TimeConstructible does not include n ≤ t (Classes/Constructible.lean).
• The simulation needs max n 2 ≤ T h and the diagonal needs n ≤ T. Both follow from max n 2 ≤ T and h ≥ 1, and h ≥ 1 is forced anyway by max n 2 ≤ T h.
• T h must be time-constructible. The general statements assume it. For the fourth root it is proved with TimeConstructible.comp_of_computableInPolyTime and the binary Nat.log 2 and Nat.sqrt certificates.

Novelty check

Verdict: not found.

• Samuel's note sources/hpv_counting_simulation.pdf states only the containments, as its Theorem 3.1 and the closing PPTIME remark. It states no separation, not even DTIME[2 ^ T] ⊄ NTIME[T].
• O'Donnell's Some exposition of "The Exponential Time Hypothesis Is False" (PDF dated October 30, 2026), p. 13, states NTIME(T) ⊆ DTIME(2^{O(T (log log T)^3 / √log T)}) and attributes its encoding to Subercaseaux. It states no separation corollary.
• Before 2026 the simulation side was open. Doty, An Oracle Strongly Separating Deterministic Time from Nondeterministic Time, via Kolmogorov Complexity, Conjecture 2.4, records Lipton's conjecture that NTIME(t) ⊆ DTIME(2^{εt}) for every ε > 0.
• Searches turned up no statement of DTIME(2^n) ⊄ NTIME(n · g(n)) for any g → ∞.

The result is a direct combination of the containment with the deterministic time hierarchy. The PR will label it as original in this library, without claiming it is a new theorem.

Completion

Done when one PR (under about 1.5k lines) lands with the statements above and test instances at T n = (n + 1) ^ 2 + 1. The new and generalized declarations are not headline candidates. The counting simulation has no abstract, so there is no abstract impact.