Padded fair-coin counts at a linear clock are SharpTIME functions (NTIME/BPTIME/PPTIME from #TIME)

Follow-up to #2050. With this bridge, NTIME[T], BPTIME[T] and PPTIME[T] ⊊ DTIME[2 ^ T] follow from #TIME, as Samuel asked, instead of through the padded-count simulation.

Current state. #2050's PR proves one separation for every class decided by a polynomial-time test of two SharpTIME counts:

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

⊕TIME, Mod_kTIME and C₌TIME are instances of it. NTIME, BPTIME and PPTIME are not yet, because the library reduces them to padded fair-coin counts, not terminal-path counts:

exists_acceptCount_of_mem_NTIME;
exists_acceptCount_of_mem_BPTIME;
MultiTapePTM.decidesByMajorityInTime_iff.

Their separations currently go through ssubset_DTIME_two_pow_of_subset_iUnion and the existing containments.

Missing statement (exact form to be settled):

theorem Turing.MultiTapePTM.acceptCount_mem_SharpTIME {k : ℕ} {State : Type} [Finite State]
    (M : MultiTapePTM k Bool State) (hT : TimeConstructible T) (c₁ c₂ : ℕ) :
    (fun a => M.acceptCount (enc a) (c₁ * T (enc a).length + c₂)) ∈ SharpTIME enc T

With this, together with 2 ^ τ ∈ SharpTIME (the same construction with an always-accepting machine):

NTIME is the instance with rule 0 < f;
PPTIME is the instance with rule g < 2 * f, where g = 2 ^ τ;
BPTIME follows through BPTIME_subset_PPTIME.

Construction. A native counting machine:

computes τ in unary within O(T);
simulates M, taking each coin as a binary choice;
after M halts, keeps making binary choices, with no further effect, until τ coins are used.

This makes the terminal count equal the padded count. main has only polynomial-clock guess-and-verify machines (MultiTape/Counting/Verifier.lean), and CountingChoice.table, which goes the other way: native machine to fair-coin machine.

Not claimed. Proposed by worker-claude-e6cf7b0d-hpv-corollaries.

Claimed by worker-claude-e6cf7b0d-sharp-bridge (Claude Code, Opus), on branch claude/padded-count-sharptime. The branch is stacked on #2054 (claude/hpv-corollaries) by merge.

Bridge statement. The clock is existential rather than exactly c₁ * T n + c₂:

theorem Cslib.Complexity.exists_clock_acceptCount_mem_SharpTIME {α : Type} {enc : α ↪ List Bool}
    {T : ℕ → ℕ} (hT : TimeConstructible T) (c₁ c₂ : ℕ) :
    ∃ τ : ℕ → ℕ, (∀ n, c₁ * T n + c₂ ≤ τ n) ∧ (∃ C, ∀ n, τ n ≤ C * T n + C) ∧
      ∀ {k : ℕ} {State : Type} [Finite State] (M : Turing.MultiTapePTM k Bool State),
        (fun a => M.acceptCount (enc a) (τ (enc a).length)) ∈ SharpTIME enc T

The witness is τ n = (c₁ + c₂) * 2 ^ Nat.size (T n), which lies between c₁ * T n + c₂ and (c₁ + c₂) * (2 * T n + 1).

Why not the exact clock. Preparing exactly c₁ * T n + c₂ in unary would need a binary-to-unary conversion in linear time. The library has only a quadratic one (ComputableInO.natToUnary).

Rounding up to a power of two keeps the whole construction linear. A streaming fold doubles a unary counter once per binary digit of T n. The round costs form a geometric sum, so this takes O(T n).

The rounded clock is enough for every application: each count characterization below holds at every clock of at least c₁ * T n + c₂. Because τ is chosen before M, both counts in a test can share it.

Machine. A deterministic phase prepares τ in unary on a fresh work tape and restores everything else. The counting phase then runs M, taking each coin as a two-occurrence choice and advancing the clock head. After M halts, it keeps making two equal choices per remaining clock cell. It halts when the clock is exhausted. The terminal paths are therefore exactly the coin strings of length τ.

Consequences. These follow from the bridge:

NTIME[T] is the test 0 < f;
PPTIME[T] is the test g < 2 * f, with g = 2 ^ τ from an always-accepting machine;
BPTIME[T] follows through BPTIME_subset_PPTIME.

NTIME/BPTIME/PPTIME_ssubset_DTIME_two_pow keep their statements. Their proofs become instances of ssubset_DTIME_two_pow_of_forall_mem_SharpTIME, so they move beside the other instances in CountingClasses.lean.

worker-claude-e6cf7b0d-sharp-bridge: awaiting review in #2068 (head f6adee005, stacked on #2054 by merge). It proves the bridge as posted above, together with the NTIME/PPTIME/BPTIME count tests. NTIME/BPTIME/PPTIME_ssubset_DTIME_two_pow are now instances of the family separation, with unchanged statements. All six gates pass locally.

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

Navigation Menu

Repository navigation

Padded fair-coin counts at a linear clock are SharpTIME functions (NTIME/BPTIME/PPTIME from #TIME) #2053

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Padded fair-coin counts at a linear clock are SharpTIME functions (NTIME/BPTIME/PPTIME from #TIME) #2053

Description

Activity

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions