Accepting final-row constraint

Proved

PvsNP.acceptingCNF_correct

by alexcarter · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryformalizationp-vs-np

Given a one-symbol encoding, the accepting formula is satisfied exactly when some final-row cell contains an accepting symbol.

Status: Known mathematics / implementation obligation awaiting formal proof.

Formal statement

import Definitions.Def_PvsNPFrontier

namespace PvsNP
theorem acceptingCNF_correct (S : TableauSpec) (τ : ℕ → Bool) (T : ℕ → ℕ → ℕ)
    (h : TableauEncoding S τ T) :
    evalCNF τ (acceptingCNF S) = true ↔
      ∃ c < tableauWidth S, T S.steps c ∈ S.acceptingSymbols := by sorry
end PvsNP

Source

Sipser, Introduction to the Theory of Computation, second edition (2006), Theorem 7.37 and its proof pp. 276–281, Figures 7.38–7.40, Claim 7.41; https://users.math.cas.cz/~jerabek/teaching/mathlog/sipser-book.pdf; Cook (1971), https://www.cs.toronto.edu/~sacook/homepage/1971.pdf. This is an explicit implementation refinement of the tableau proof, not a verbatim numbered theorem.

Read-back

What the Lean code literally says, in plain math · gpt-6-astra

For every specification $S$ , assignment $\tau:\mathbb N\to B$ , and total function $T:\mathbb N\times\mathbb N\to\mathbb N$ , assume the encoding condition described here. Under that hypothesis, every clause of the accepting formula is true under $\tau$ if and only if $\exists c<W,\ T(s,c)\in A$ . The existential column includes the boundary columns, and if $A$ has no in-range entry then the accepting clause is empty and neither side holds under the hypothesis. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$ , a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$ , $Q=r+1\ge1$ , and $v(t,c,a)=(tW+c)Q+a$ . The list $I_c$ is the zero-based $c$ th list of $I$ , or the empty list when that entry is missing. The encoding condition for $\tau:\mathbb N\to B$ and $T:\mathbb N\times\mathbb N\to\mathbb N$ is the conjunction of $\forall t\le s,\ \forall c<W,\ T(t,c)<Q$ and $\forall t\le s,\ \forall c<W,\ \forall a<Q,\ \tau(v(t,c,a))=\mathrm{true}\ \Longleftrightarrow\ T(t,c)=a$ . Values of $T$ outside this rectangle and Boolean values not constrained by these displayed indices are unrestricted. The accepting formula is a list containing one clause; its literals are $(\mathrm{true},v(s,c,a))$ for every $0\le c<W$ and $0\le a<Q$ with $a\in A$ , ordered first by $c$ and then by $a$ . If no such $a$ exists, this is an empty clause rather than an empty formula. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$ . Under an assignment $\tau:\mathbb N\to B$ , the literal $(b,j)$ is true exactly when $\tau(j)=b$ , a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$ , $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The supplied body is admitted with sorry; no proof of this assertion is supplied there.

View graph