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.

The Cook-Levin formula is satisfiable if and only if an accepting bounded tableau exists

Statement

Fix a nondeterministic one-tape machine $N$ , an input $w$ , and a bound $T \geq ∣ w ∣$ such that every branch of $N$ on $w$ halts within $T$ steps and never visits a tape cell beyond position $T$ . Let $ψ_{N, w} : = ψ_{c e l l} \land ψ_{s t a r t} \land ψ_{m o v e} \land ψ_{a c c e p t}$ be the standard Cook-Levin formula built from the tableau variables. Then $ψ_{N, w}$ is satisfiable if and only if there exists an accepting bounded computation tableau for $N$ on $w$ of height and width $T + 1$ .

Facts & Assumptions

Given: A nondeterministic one-tape machine $N$ , an input $w$ , a bound $T$ satisfying the hypotheses in the statement, and the Cook-Levin formula $ψ_{N, w}$ .

[L1]

The cell constraints force each tableau position to carry exactly one symbol, by The exactly-one-symbol constraints have polynomial size.

[L2]

The start, accept, and transition constraints enforce the initial row, an accepting position, and local transition legality, by The start, accept, and transition constraints have polynomial size.

[L3]

A tableau is a valid branch computation history exactly when its first row is correct and every local window is legal, by A tableau is legal exactly when the start row is correct and every local window is legal.

Proof

technique · direct

1.1L2L3givenconstruct

If an accepting bounded tableau exists, assign each variable $X_{r, c, a}$ the value $1$ exactly when the tableau places symbol $a$ in cell $(r, c)$ . The tableau then satisfies $ψ_{c e l l}$ by construction, while [L2] and [L3] show that it also satisfies $ψ_{s t a r t}$ , $ψ_{m o v e}$ , and $ψ_{a c c e p t}$ . Hence $ψ_{N, w}$ is satisfiable.

1.2L1given

Conversely, suppose $ψ_{N, w}$ is satisfiable. By [L1], the satisfying assignment determines one symbol in every tableau cell.

2.1L2L3step 1.2

The tableau extracted in step 1.2 satisfies the required start, accept, and local transition conditions by [L2]. Therefore [L3] turns it into a genuine branch computation history for $N$ on $w$ , with later rows allowed to repeat once a halting configuration has appeared, and the accept part of [L2] makes that history accepting.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 prove both implication directions, so $ψ_{N, w}$ is satisfiable exactly when an accepting bounded tableau exists.

Depends on

Used by

FALSE: the Cook-Levin reduction enumerates all nondeterministic branches False statement
The Cook--Levin construction can be made parsimonious Lemma
SAT is NP-complete Theorem

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

MIT 18.404J / 6.840J, Lecture 16: Cook-Levin Theorem (standard reference, not scraped)
Stephen A. Cook, The Complexity of Theorem-Proving Procedures (standard reference, not scraped)