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

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.

Any machine that fully reads every input of length n needs at least linear time

Statement

Let $M$ be a $k$ -tape machine that halts on every input of length $n$ . If, on every such input, the accepting or rejecting branch of $M$ scans each of the first $n$ input cells before halting, then ${Time}_{M} (n) \geq n .$

Facts & Assumptions

Given: A halting machine $M$ with the input-reading property stated above.

[L1]

Worst-case running time ${Time}_{M} (n)$ is the maximum number of steps over inputs of length $n$ , by Worst-case time and space complexity of a machine.

Proof

technique · direct

1.1

In one machine step, the input head can move across at most one tape edge, so a single step can expose at most one previously unseen input cell. Starting at the leftmost input cell, reaching all first $n$ input cells therefore requires at least $n - 1$ moves and hence at least $n$ time steps under the usual start-and-halt conventions.

given

2.1

The hypothesis says this lower bound applies on every input of length $n$ . By [L1], the worst-case value ${Time}_{M} (n)$ is at least that common lower bound, so ${Time}_{M} (n) \geq n$ .

L1step 1.1∎

Depends on

Worst-case time and space complexity of a machine

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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)