LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

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.

A constructible time bound yields a uniformly clocked simulator

Statement

Let $t : N \to N$ be time-constructible, and assume $n \leq t (n)$ for all sufficiently large $n$ . Then for every coded deterministic machine $e = ⌜ M ⌝$ there exists a deterministic machine ${Clock}_{e, t}$ such that, on each input $x$ :

if $M$ halts within at most $t (∣ x ∣)$ steps, then ${Clock}_{e, t}$ halts with the same output;
if $M$ has not halted by time $t (∣ x ∣)$ , then ${Clock}_{e, t}$ halts and rejects.

Facts & Assumptions

Given: A time-constructible function $t$ and a coded deterministic machine $e = ⌜ M ⌝$ .

[L1]

Time-constructibility means that a machine can compute the binary numeral of $t (n)$ within $O (t (n))$ time on input $1^{n}$ , by Time-constructible and space-constructible functions.

[L2]

A universal simulator reproduces the halting outputs and divergence of the coded machine on the coded input, by A universal Turing machine relative to a fixed machine encoding.

[L3]

The machine code $e$ is an effective binary description of $M$ , by A fixed effective binary encoding of deterministic one-tape Turing machines.

[L4]

Any machine that must fully read an input of length $n$ needs at least linear time, by Any machine that fully reads every input of length n needs at least linear time.

Proof

technique · direct

1.1

On input $x$ , the machine ${Clock}_{e, t}$ first scans the whole input once to learn $∣ x ∣$ . The lower bound hypothesis $n \leq t (n)$ together with [L4] ensures that this preliminary scan fits inside the intended asymptotic budget. It then runs the constructor from [L1] on unary input $1^{∣ x ∣}$ to obtain the binary numeral of $t (∣ x ∣)$ and writes a counter of that size on a work tape.

L1L4givenconstruct

2.1

Next, using the fixed code $e$ from [L3], the machine simulates $M$ on $x$ while decrementing the counter once per simulated step. If the simulation halts before the counter reaches $0$ , the simulator outputs exactly what $M$ outputs; if the counter reaches $0$ first, the machine enters a rejecting state and stops. This is the standard clocked simulation built from the universal behavior in [L2].

L2L3step 1.1construct

3.1

Step 2.1 proves the two clauses of the statement: successful runs of $M$ before the deadline are preserved, and overlong runs are cut off by a halting reject state.

step 2.1∎

Depends on

Used by

FALSE: clocked-simulation and time-hierarchy arguments never need constructibility hypotheses False statement

Dependency tree · two levels

10 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

John Watrous, Introduction to the Theory of Computing, Lecture 19: Time-bounded computations (standard reference, not scraped)
Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach (standard reference, not scraped)