HPV corollaries: ⊕TIME, Mod_kTIME, C₌TIME in 2^O(T/√log T), and NTIME[T] ⊊ DTIME[2^T]

Two follow-ups to the unconditional HPV containments of #1833 (CountingSimulation/FastSimulation.lean). coordinator-claude-e6cf7b0d proposed them and Samuel selected them.

Claimed by worker-claude-e6cf7b0d-hpv-corollaries (Claude Code, Opus), on branch claude/hpv-corollaries.

Throughout, T is time-constructible with max n 2 ≤ T n, as in the HPV theorems.

1. ⊕TIME, Mod_kTIME and C₌TIME

main has ParityP, ModP k and CeqP only at polynomial time; there is no time-parameterized version. I propose minimal definitions as predicates on SharpTIME, the native terminal-path counts from #2003. Unlike padded coin-string counts, a terminal count does not change when the clock grows, so residues are well defined.

def ParityTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
  {A | ∃ f ∈ SharpTIME enc t, ∀ a, a ∈ A ↔ Odd (f a)}
def ModTIME (k : ℕ) (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
  {A | ∃ f ∈ SharpTIME enc t, ∀ a, a ∈ A ↔ f a % k ≠ 0}
def CeqTIME (enc : α ↪ List Bool) (t : ℕ → ℕ) : Set (Set α) :=
  {A | ∃ f ∈ SharpTIME enc t, ∃ g ∈ SharpTIME enc t, ∀ a, a ∈ A ↔ f a = g a}

These follow the conventions of ModP (a nonzero residue) and mem_CeqP_iff_exists_SharpP (equality of two counts). Each comes with a polynomial-time bridge, for example A ∈ ModP k enc ↔ ∃ d, A ∈ ModTIME k enc (· ^ d); the other two are the same for ParityP and CeqP.

The containments:

theorem ModTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two (k : ℕ)
    (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
    ModTIME k enc T ⊆ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)))

ParityTIME and CeqTIME get the same statement. The proof computes the exact counts with the HPV counting simulation, then applies a polynomial-time test: the residue, or equality of the two counts. The statement holds for every fixed k, not only k ≥ 2. A joint polynomial-space form will be added where it is cheap.

2. Strict containments

theorem DTIME_two_pow_not_subset_iUnion_DTIME_two_pow_div_sqrt_log_two
    (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
    ¬DTIME encBits (fun n => 2 ^ T n) ⊆
      ⋃ C, DTIME encBits fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)))

theorem NTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
    NTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n

BPTIME, PPTIME, ParityTIME, ModTIME k and CeqTIME get the same statement as NTIME.

The separating language is the clocked diagonal of Hierarchy/Time.lean with clock J n = 2 ^ (T n / 4). That one language lies in DTIME[2 ^ T] and outside DTIME[2 ^ (C T / √⌊log₂ T⌋)] for every C. It is in DTIME[2 ^ T] because (n + 1) ^ 5 * (J n + 1) ^ 3 = O(2 ^ T), and outside each class because J eventually beats every c * 2 ^ (C T / √log T) + c. Beyond the HPV hypotheses, the proof needs only a new lemma that n ↦ 2 ^ (T n / k) is time-constructible; no extra growth hypothesis is required.

Tests will instantiate these at the clock (n + 1) ^ 2 + 1.

worker-claude-e6cf7b0d-hpv-corollaries: revised plan, following Samuel's direction that the counting classes and the separations come from #TIME. The branch now stacks on #2041 by merge.

1. A postprocessing lemma for FTIME. A polynomial-time test of two FTIME[t] outputs is decidable in time polynomial in t. The output length is at most c * t n + c, so the test costs O((t n + 1) ^ e).

theorem setOf_mem_DTIME_of_mem_FTIME {f : α → β₁} {g : α → β₂} {t : ℕ → ℕ}
    (hf : f ∈ FTIME enc enc₁ t) (hg : g ∈ FTIME enc enc₂ t) {rule : β₁ × β₂ → Bool}
    (hrule : ComputableInPolyTime rule (encPair enc₁ enc₂) encBool) :
    ∃ e, {a | rule (f a, g a) = true} ∈ DTIME enc fun n => (t n + 1) ^ e

2. The generic containment for count predicates, from #2041's SharpTIME_subset_iUnion_FTIME_two_pow_div_sqrt_log_two and lemma 1. Since (2 ^ x + 1) ^ e ≤ 2 ^ e * 2 ^ (e * x), the result stays at scale 2 ^ O(T / √log T).

theorem setOf_mem_iUnion_DTIME_of_mem_SharpTIME (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n)
    {f g : α → ℕ} (hf : f ∈ SharpTIME enc T) (hg : g ∈ SharpTIME enc T) {rule : ℕ × ℕ → Bool}
    (hrule : ComputableInPolyTime rule (encPair encNat encNat) encBool) :
    {a | rule (f a, g a) = true} ∈ ⋃ C, DTIME enc fun n => 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n)))

3. One separation for the whole family, using the time hierarchy on main with clock 2 ^ (T n / 4). One language serves every C.

theorem ssubset_DTIME_two_pow_of_forall_mem_SharpTIME {𝒞 : Set (Set (List Bool))}
    (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n)
    (h : ∀ A ∈ 𝒞, ∃ f ∈ SharpTIME encBits T, ∃ g ∈ SharpTIME encBits T, ∃ rule : ℕ × ℕ → Bool,
      ComputableInPolyTime rule (encPair encNat encNat) encBool ∧ ∀ x, x ∈ A ↔ rule (f x, g x) = true) :
    𝒞 ⊂ DTIME encBits fun n => 2 ^ T n

This is assembled from DTIME_two_pow_not_subset_iUnion_DTIME_two_pow_div_sqrt_log_two and iUnion_DTIME_two_pow_div_sqrt_log_two_subset, both already compiled locally.

4. Instances that follow directly. ParityTIME (rule p.1 % 2 = 1), ModTIME k (rule p.1 % k ≠ 0, any fixed k) and CeqTIME (rule p.1 = p.2) each get the containment and ⊊ DTIME[2 ^ T]. The definitions are those in the issue body.

5. NTIME, BPTIME and PPTIME as instances: needs one bridge first. Their library definitions reduce to padded fair-coin counts, not terminal-path counts. See exists_acceptCount_of_mem_NTIME, exists_acceptCount_of_mem_BPTIME and decidesByMajorityInTime_iff: in each, the count of a halted run doubles with every extra coin. The existing bridge runs the other way. CountingChoice.table turns a SharpTIME machine into a fair-coin machine whose padded count equals the terminal count, so Count.lean derives #TIME from padded counts.

To make N/BP/PP instances of statement 3, the library needs the converse at a linear clock: the padded count of a fair-coin machine at τ = c₁ T + c₂ is in SharpTIME[T]. That takes a native counting machine that computes the clock, simulates the coin machine with each coin as a binary choice, and keeps branching after a halt until the clock runs out. main has only the polynomial-clock guess-and-verify machines (MultiTape/Counting/Verifier.lean), not an O(T) one.

That bridge is a substantial machine construction, beyond this PR's time budget. My proposal:

this PR proves statements 1–4;
it keeps NTIME/BPTIME/PPTIME_ssubset_DTIME_two_pow as instances of the class-level separation ssubset_DTIME_two_pow_of_subset_iUnion, through their existing containments;
I open a follow-up issue for the padded-count → SharpTIME bridge, after which N/BP/PP become instances of statement 3 directly.

If you'd rather block on the bridge, say so.

Joint polynomial-space forms for the new classes are not planned. The postprocessing runs in time polynomial in the count's digit length, which is bounded only by the time scale.

worker-claude-e6cf7b0d-hpv-corollaries: awaiting review in #2054 (head f6d28d6b6, stacked on #2041 by merge). It covers statements 1–4 of the revised plan:

the FTIME postprocessing lemma;
the #TIME count-predicate containment, from feat(CountingSimulation): unconditional SharpTIME ⊆ FTIME in time 2^O(T/√log T) (#1833) #2041;
one ⊊ DTIME[2 ^ T] separation for the whole family;
the ⊕/Mod_k/C₌ instances.

NTIME/BPTIME/PPTIME ⊊ DTIME[2 ^ T] are proved through their existing containments, not yet as instances of the #TIME family statement. The bridge for that is in #2053. Keep this issue open until #2053 is decided.

worker-claude-e6cf7b0d-sharp-bridge: #2053's bridge is in #2068, stacked on #2054. With it, NTIME/BPTIME/PPTIME ⊊ DTIME[2 ^ T] are direct instances of ssubset_DTIME_two_pow_of_forall_mem_SharpTIME.

feat(CountingSimulation): counting classes from #TIME and NTIME/BPTIM…

feat(SharpP): padded coin counts at a linear clock are SharpTIME func…

Navigation Menu

Repository navigation

HPV corollaries: ⊕TIME, Mod_kTIME, C₌TIME in 2^O(T/√log T), and NTIME[T] ⊊ DTIME[2^T] #2050

1. ⊕TIME, Mod_kTIME and C₌TIME

2. Strict containments

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

HPV corollaries: ⊕TIME, Mod_kTIME, C₌TIME in 2^O(T/√log T), and NTIME[T] ⊊ DTIME[2^T] #2050

Description

1. ⊕TIME, Mod_kTIME and C₌TIME

2. Strict containments

Activity

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions