Local transition constraints

Proved

PvsNP.transitionCNF_correct

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

complexity-theoryformalizationp-vs-np

Given a one-symbol encoding, all transition clauses hold exactly when every adjacent 2-by-3 window is in the allowed-window list.

Status: Known mathematics / implementation obligation awaiting formal proof.

Formal statement

import Definitions.Def_PvsNPFrontier

namespace PvsNP
theorem transitionCNF_correct (S : TableauSpec) (τ : ℕ → Bool) (T : ℕ → ℕ → ℕ)
    (h : TableauEncoding S τ T) :
    evalCNF τ (transitionCNF S) = true ↔
      ∀ t < S.steps, ∀ c < S.interior, windowValues T t c ∈ S.allowedWindows := 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 transition formula is true under $\tau$ if and only if $\forall t<s,\ \forall c<i,\ [T(t,c),T(t,c+1),T(t,c+2),T(t+1,c),T(t+1,c+1),T(t+1,c+2)]\in H$ . When $s=0$ or $i=0$ , the formula is empty and the right-hand universal condition is vacuous. 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 transition formula ranges in increasing order over $0\le t<s$ , $0\le c<i$ , and lexicographically over all six-tuples $u\in\{0,\ldots,Q-1\}^6$ absent from the list $H$ . For each such tuple it has the clause of the six negative literals at positions $(t,c),(t,c+1),(t,c+2),(t+1,c),(t+1,c+1),(t+1,c+2)$ with symbol indices given by the corresponding entries of $u$ , in that order. If $s=0$ or $i=0$ , the transition formula is empty. 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