Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Nondeterministic acceptance time and exact clocks

Definition

For a fixed finitely branching nondeterministic multitape machine N, let τN(x) be the minimum length of an accepting branch, or if there is none. The minimum of a nonempty set of natural lengths exists by searching lengths in increasing order. This extends the existential acceptance convention in Accepting computations of a nondeterministic machine to the finite-valued multitape transition map in The classes DTIME, NTIME, DSPACE, and NSPACE. Nonaccepting branches may diverge. For a finite integer t, acceptance within t means τN(x)t. For b:NN, put Lb(N)={x:τN(x)b(x)}. The acceptance-time class for b consists of languages L(N) with τN(x)=O(b(x)) on their accepted inputs, uniformly in the input and with fixed machine-dependent constants.

This differs at the machine level from the maximum-branch convention in Worst-case time and space complexity of a machine. The library class NTIME uses all-branch halting as in The classes DTIME, NTIME, DSPACE, and NSPACE. Big-O and little-o have the zero-safe and finite-exception meanings in Uniform asymptotic time space comparison.

An exact clock for T here is a deterministic fixed multitape machine that halts after exactly T(n) transitions on every binary input of length n. Its initial state is nonhalting, so T(n)1. We do not require monotonicity. The exact-clock clause of Machine time and space constructibility motivates the terminology but its separate nondecreasing guard is not imported into this local definition; a unary-only clock can be run after copying a binary input to unary, paying O(n+1) preprocessing time. No equivalence with an output constructor is asserted.

For an acceptor N and such a clock, copy the input for N to one tape set and simultaneously write one binary 0 per input symbol to the clock's input tape, producing 0x even when N has a nonbinary input alphabet. Then perform one simulated transition of each machine per round. Check acceptance at the initial instant and after each N-transition, including the last allowed one; after the clock's T(n)th transition reject if no acceptance has occurred. Missing transition options count as rejecting branches. This recognizes exactly LT(N): an accepting branch of length at most T survives, and every surviving acceptance came from such a branch. Every branch terminates in ON(n+T(n)+1) real transitions. Temporary stay-put bookkeeping is implementable in the L/R-only model by a two-move excursion right and left, returning to the same cell even at zero, with intermediate states not halting.

To retain a bound CT(n) rather than just T(n), run C clock copies sequentially while continuing N for one step per simulated clock transition; for a fixed integer C this is still ON(n+T(n)+1). Resets or prebuilt copies cost the same order. If an acceptor recognizes a language within O(T) and Tn, choose C covering the tail bound and the finitely many accepting exceptions (T is positive there). This yields an all-branch machine for the same language in NTIME(T). There is no such conversion asserted for arbitrary unclocked recursive b.

Depends on

Used by

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources