Cell constraints encode exactly one symbol

Proved

PvsNP.cellsCNF_correct

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

complexity-theoryformalizationp-vs-np

The cell formula is satisfied exactly when the assignment encodes a bounded symbol value at each tableau cell.

Status: Known mathematics / implementation obligation awaiting formal proof.

Formal statement

import Definitions.Def_PvsNPFrontier

namespace PvsNP
theorem cellsCNF_correct (S : TableauSpec) (τ : ℕ → Bool) :
    evalCNF τ (cellsCNF S) = true ↔ ∃ T, TableauEncoding S τ T := 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$ and every assignment $\tau:\mathbb N\to B$ , all clauses of the cell formula are true under $\tau$ if and only if there exists a total function $T:\mathbb N\times\mathbb N\to\mathbb N$ satisfying the encoding condition described here. No initial, boundary, accepting, or transition constraint is included in that encoding condition. 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 cell formula consists, in increasing $t=0,\ldots,s$ and then increasing $c=0,\ldots,W-1$ , of the clause of all positive literals $(\mathrm{true},v(t,c,a))$ for $a=0,\ldots,Q-1$ , followed by every two-literal clause $[(\mathrm{false},v(t,c,a)),(\mathrm{false},v(t,c,b))]$ with $0\le a<b<Q$ , ordered first by $a$ and then by $b$ . 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. 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