SAT-specialized guess-and-verify NTM

This file implements the concrete SAT route to NP. It avoids the still-open generic NP.WitnessNTMConstruction by using the proved linear counter subroutine for SAT witnesses, whose length is bounded by |x| + 1. The final theorems prove the composed machine decides language in polynomial time from a polynomial-time verifier.

The machine is parameterized by a verifier DTM M : TM k for pairLang Witness. Its work-tape layout is:

• 0 .. k-1: verifier-internal work tapes,
• k: pair tape, used as the virtual input for M,
• k+1: guessed witness tape,
• k+2: unary counter tape.

The state space is a direct sequence of the existing subroutine phases: counter setup, input rewind, bounded guessing, pair building, and verifier simulation.

def Complexity.SAT.satGuessVerifySetupTime (n : ℕ) : ℕ

Deterministic setup budget for the SAT-specialized machine before pair construction starts: build the |x|+1 counter, rewind the input, and run the bounded guessing subroutine through its phase exit.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.satVerifierWindowTime (f : ℕ → ℕ) (n : ℕ) : ℕ

A uniform verifier-time window for all witnesses of length at most n + 1. We take a finite maximum because the verifier bound f is not assumed monotone.

Equations

• Complexity.SAT.satVerifierWindowTime f n = (Finset.range (n + 2)).sup fun (m : ℕ) => f (2 * n + 2 + m)

def Complexity.SAT.satGuessVerifyTime (f : ℕ → ℕ) (n : ℕ) : ℕ

SAT-specialized witness-independent run budget induced by a verifier bound f.

Equations

• Complexity.SAT.satGuessVerifyTime f n = Complexity.SAT.satGuessVerifySetupTime n + (Complexity.TM.pairBuildTime n (n + 1) + Complexity.SAT.satVerifierWindowTime f n)

theorem Complexity.SAT.satVerifierWindowTime_bounds_pair (f : ℕ → ℕ) (x y : List Bool) (hlen : y.length ≤ x.length + 1) : f (pair x y).length ≤ satVerifierWindowTime f x.length

The verifier window bound dominates f on any pair ⟨x, y⟩ whose witness y has length at most |x| + 1.

theorem Complexity.SAT.polynomial_eval_mono_nat (p : Polynomial ℕ) : Monotone fun (n : ℕ) => Polynomial.eval n p

Evaluation of a natural-coefficient polynomial is monotone in its argument.

def Complexity.SAT.satPairIdx (k : ℕ) : Fin (k + 3)

Work-tape index for the pair/virtual-input tape.

Equations

• Complexity.SAT.satPairIdx k = ⟨k, ⋯⟩

def Complexity.SAT.satWitnessIdx (k : ℕ) : Fin (k + 3)

Work-tape index for the guessed witness tape.

Equations

• Complexity.SAT.satWitnessIdx k = ⟨k + 1, ⋯⟩

def Complexity.SAT.satCounterIdx (k : ℕ) : Fin (k + 3)

Work-tape index for the unary guess-bound counter.

Equations

• Complexity.SAT.satCounterIdx k = ⟨k + 2, ⋯⟩

def Complexity.SAT.satVerifierWorkIdx {k : ℕ} (i : Fin k) : Fin (k + 3)

Embed a verifier-internal work-tape index into the SAT machine layout.

Equations

• Complexity.SAT.satVerifierWorkIdx i = ⟨↑i, ⋯⟩

theorem Complexity.SAT.satWitnessIdx_ne_pairIdx (k : ℕ) : satWitnessIdx k ≠ satPairIdx k

The witness tape and the pair tape are distinct work tapes.

theorem Complexity.SAT.satCounterIdx_ne_pairIdx (k : ℕ) : satCounterIdx k ≠ satPairIdx k

The counter tape and the pair tape are distinct work tapes.

theorem Complexity.SAT.satCounterIdx_ne_witnessIdx (k : ℕ) : satCounterIdx k ≠ satWitnessIdx k

The counter tape and the witness tape are distinct work tapes.

theorem Complexity.SAT.satVerifierWorkIdx_ne_pairIdx {k : ℕ} (i : Fin k) : satVerifierWorkIdx i ≠ satPairIdx k

Embedded verifier work tapes are distinct from the pair tape.

theorem Complexity.SAT.satVerifierWorkIdx_ne_witnessIdx {k : ℕ} (i : Fin k) : satVerifierWorkIdx i ≠ satWitnessIdx k

Embedded verifier work tapes are distinct from the witness tape.

theorem Complexity.SAT.satVerifierWorkIdx_ne_counterIdx {k : ℕ} (i : Fin k) : satVerifierWorkIdx i ≠ satCounterIdx k

Embedded verifier work tapes are distinct from the counter tape.

inductive Complexity.SAT.GuessVerifyPhase (Q : Type) : Type

Control states for the SAT-specialized guess-and-verify machine.

• counter {Q : Type} : TM.LinearCounterPhase → GuessVerifyPhase Q

  Building the |x| + 1 unary counter on the counter tape.

• rewindInput {Q : Type} : TM.RewindPhase → GuessVerifyPhase Q

  Rewinding the input head back to the start marker.

• guess {Q : Type} : NTM.GuessBoundedPhase → GuessVerifyPhase Q

  Nondeterministically guessing a counter-bounded witness.

• pair {Q : Type} : TM.PairBuildPhase → GuessVerifyPhase Q

  Writing pair x y of input and witness onto the pair tape.

• verify {Q : Type} : Q → GuessVerifyPhase Q

  Simulating the verifier M in state Q on the pair tape.

def Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq {Q✝ : Type} [DecidableEq Q✝] (x✝ x✝¹ : GuessVerifyPhase Q✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.counter a) (Complexity.SAT.GuessVerifyPhase.counter b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.counter a) (Complexity.SAT.GuessVerifyPhase.rewindInput a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.counter a) (Complexity.SAT.GuessVerifyPhase.guess a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.counter a) (Complexity.SAT.GuessVerifyPhase.pair a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.counter a) (Complexity.SAT.GuessVerifyPhase.verify a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.rewindInput a) (Complexity.SAT.GuessVerifyPhase.counter a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.rewindInput a) (Complexity.SAT.GuessVerifyPhase.guess a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.rewindInput a) (Complexity.SAT.GuessVerifyPhase.pair a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.rewindInput a) (Complexity.SAT.GuessVerifyPhase.verify a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.guess a) (Complexity.SAT.GuessVerifyPhase.counter a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.guess a) (Complexity.SAT.GuessVerifyPhase.rewindInput a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.guess a) (Complexity.SAT.GuessVerifyPhase.guess b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.guess a) (Complexity.SAT.GuessVerifyPhase.pair a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.guess a) (Complexity.SAT.GuessVerifyPhase.verify a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.pair a) (Complexity.SAT.GuessVerifyPhase.counter a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.pair a) (Complexity.SAT.GuessVerifyPhase.rewindInput a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.pair a) (Complexity.SAT.GuessVerifyPhase.guess a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.pair a) (Complexity.SAT.GuessVerifyPhase.pair b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.pair a) (Complexity.SAT.GuessVerifyPhase.verify a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.verify a) (Complexity.SAT.GuessVerifyPhase.counter a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.verify a) (Complexity.SAT.GuessVerifyPhase.rewindInput a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.verify a) (Complexity.SAT.GuessVerifyPhase.guess a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.verify a) (Complexity.SAT.GuessVerifyPhase.pair a_1) = isFalse ⋯
• Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq (Complexity.SAT.GuessVerifyPhase.verify a) (Complexity.SAT.GuessVerifyPhase.verify b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.SAT.instDecidableEqGuessVerifyPhase {Q✝ : Type} [DecidableEq Q✝] : DecidableEq (GuessVerifyPhase Q✝)

Equations

• Complexity.SAT.instDecidableEqGuessVerifyPhase = Complexity.SAT.instDecidableEqGuessVerifyPhase.decEq

@[implicit_reducible]

instance Complexity.SAT.instFintypeGuessVerifyPhaseOfDecidableEq {Q : Type} [DecidableEq Q] [Fintype Q] : Fintype (GuessVerifyPhase Q)

GuessVerifyPhase Q is finite whenever Q is.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.verifierStartedState {k : ℕ} (M : TM k) : M.Q

State reached when entering the verifier phase from already-started tapes. This is the state component of M's forced first step from its true initial configuration, where every tape reads ▷.

Equations

• Complexity.SAT.verifierStartedState M = (M.δ M.qstart Complexity.Γ.start (fun (x : Fin k) => Complexity.Γ.start) Complexity.Γ.start).1

def Complexity.SAT.satGuessVerifyNTM {k : ℕ} (M : TM k) : NTM (k + 3)

SAT-specialized guess-and-verify NTM parameterized by a verifier M.

It is a concrete composed machine. The proof layer below shows that, when M decides pairLang Witness, this machine decides language in polynomial time.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.satVerifyPhaseTM {k : ℕ} (M : TM k) : TM (k + 3)

The deterministic machine simulated during the verifier phase of satGuessVerifyNTM. It runs M with M's input head retargeted to the SAT pair tape, while the real input tape and the setup-only work tapes are idled.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.satVerifyInnerCfg {k : ℕ} (M : TM k) (c : Cfg (k + 3) M.Q) : Cfg k M.Q

Project a SAT verifier-phase configuration to the corresponding configuration of the underlying verifier M: the SAT pair tape becomes M's input tape, and the first k SAT work tapes become M's work tapes.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.satVerifyInnerCfg_eq_startedCfg {k : ℕ} (M : TM k) (z : List Bool) (hne : M.qstart ≠ M.qhalt) (c : Cfg (k + 3) M.Q) (hstate : c.state = verifierStartedState M) (hpair : c.work (satPairIdx k) = (Tape.init (List.map Γ.ofBool z)).move Dir3.right) (hout : c.output = (Tape.init []).move Dir3.right) (hwork : ∀ (i : Fin k), c.work (satVerifierWorkIdx i) = (Tape.init []).move Dir3.right) : satVerifyInnerCfg M c = M.startedCfg z hne

If the SAT verifier wrapper has just entered the verifier state with the pair tape as virtual input and blank started verifier work/output tapes, its projection is exactly M's post-start configuration on that pair.

theorem Complexity.SAT.verifier_started_trace_halts_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (z : List Bool) : ∃ (V : ℕ), V + 1 ≤ f z.length ∧ ∀ (choices : Fin V → Bool), M.halted (M.toNTM.trace V choices (M.startedCfg z ⋯))

A verifier that decides a language also halts from its post-start configuration. This is the verifier suffix shape used by the composed SAT machine, whose phase boundary has already performed the first move off ▷.

theorem Complexity.SAT.verifier_started_trace_decides_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (z : List Bool) : ∃ (V : ℕ), V + 1 ≤ f z.length ∧ ∀ (choices : Fin V → Bool), have cFinal := M.toNTM.trace V choices (M.startedCfg z ⋯); M.halted cFinal ∧ (z ∈ L → cFinal.output.cells 1 = Γ.one) ∧ (z ∉ L → cFinal.output.cells 1 = Γ.zero)

Output-carrying version of verifier_started_trace_halts_of_decidesInTime.

theorem Complexity.SAT.satVerifyPhaseTM_trace_one_project {k : ℕ} (M : TM k) (choice : Bool) (c : Cfg (k + 3) M.Q) (hstate : c.state ≠ M.qhalt) (hpair : (c.work (satPairIdx k)).head = 0 ∨ (c.work (satPairIdx k)).read ≠ Γ.start) : satVerifyInnerCfg M ((satVerifyPhaseTM M).toNTM.trace 1 (fun (x : Fin 1) => choice) c) = M.toNTM.trace 1 (fun (x : Fin 1) => choice) (satVerifyInnerCfg M c)

One verifier-phase step projects to one ordinary verifier step, provided the virtual-input/pair tape is structurally stable for the no-op readBackWrite.

theorem Complexity.SAT.satVerifyPhaseTM_trace_project_prefix {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) : (∀ (t : ℕ) (ht : t < T), have ct := (satVerifyPhaseTM M).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c; (ct.work (satPairIdx k)).head = 0 ∨ (ct.work (satPairIdx k)).read ≠ Γ.start) → satVerifyInnerCfg M ((satVerifyPhaseTM M).toNTM.trace T choices c) = M.toNTM.trace T choices (satVerifyInnerCfg M c)

Multi-step projection from the SAT verifier phase back to M.toNTM, assuming the virtual-input/pair tape is stable for each proper verifier prefix.

theorem Complexity.SAT.satVerifyPhaseTM_halted_iff {k : ℕ} (M : TM k) (c : Cfg (k + 3) M.Q) : (satVerifyPhaseTM M).halted c ↔ M.halted (satVerifyInnerCfg M c)

The verifier-phase wrapper halts exactly when its projection to M halts.

theorem Complexity.SAT.satVerifyPhaseTM_halts_of_inner_trace_halts {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) (hpair : ∀ (t : ℕ) (ht : t < T), have ct := (satVerifyPhaseTM M).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c; (ct.work (satPairIdx k)).head = 0 ∨ (ct.work (satPairIdx k)).read ≠ Γ.start) (hinner : M.halted (M.toNTM.trace T choices (satVerifyInnerCfg M c))) : (satVerifyPhaseTM M).halted ((satVerifyPhaseTM M).toNTM.trace T choices c)

Halting transfers from the projected verifier trace back to the SAT verifier phase.

theorem Complexity.SAT.satVerifyPhaseTM_pair_cells_ne_start_trace_one {k : ℕ} (M : TM k) (choice : Bool) (c : Cfg (k + 3) M.Q) (hclean : ∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) (j : ℕ) : j ≥ 1 → (((satVerifyPhaseTM M).toNTM.trace 1 (fun (x : Fin 1) => choice) c).work (satPairIdx k)).cells j ≠ Γ.start

One verifier-phase step preserves the invariant that the SAT pair tape has no start markers outside cell zero.

theorem Complexity.SAT.satVerifyPhaseTM_pair_cells_ne_start_trace {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) : (∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) → ∀ j ≥ 1, (((satVerifyPhaseTM M).toNTM.trace T choices c).work (satPairIdx k)).cells j ≠ Γ.start

The SAT pair tape stays free of start markers outside cell zero throughout the verifier phase.

theorem Complexity.SAT.satVerifyPhaseTM_pair_guard_of_clean {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) (hclean : ∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) (t : ℕ) (ht : t < T) : have ct := (satVerifyPhaseTM M).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c; (ct.work (satPairIdx k)).head = 0 ∨ (ct.work (satPairIdx k)).read ≠ Γ.start

A clean SAT pair tape supplies the structural guard needed by the verifier projection: if the pair head is away from cell zero, it cannot be reading a start marker.

def Complexity.SAT.satCounterWrap {k : ℕ} (M : TM k) (c : Cfg (k + 3) TM.LinearCounterPhase) : Cfg (k + 3) (GuessVerifyPhase M.Q)

Wrap a counter-subroutine configuration into the composed machine.

Equations

• Complexity.SAT.satCounterWrap M c = { state := Complexity.SAT.GuessVerifyPhase.counter c.state, input := c.input, work := c.work, output := c.output }

def Complexity.SAT.satRewindInputWrap {k : ℕ} (M : TM k) (c : Cfg (k + 3) TM.RewindPhase) : Cfg (k + 3) (GuessVerifyPhase M.Q)

Wrap an input-rewind configuration into the composed machine.

Equations

• Complexity.SAT.satRewindInputWrap M c = { state := Complexity.SAT.GuessVerifyPhase.rewindInput c.state, input := c.input, work := c.work, output := c.output }

def Complexity.SAT.satGuessWrap {k : ℕ} (M : TM k) (c : Cfg (k + 3) NTM.GuessBoundedPhase) : Cfg (k + 3) (GuessVerifyPhase M.Q)

Wrap a bounded-guess configuration into the composed machine.

Equations

• Complexity.SAT.satGuessWrap M c = { state := Complexity.SAT.GuessVerifyPhase.guess c.state, input := c.input, work := c.work, output := c.output }

def Complexity.SAT.satPairWrap {k : ℕ} (M : TM k) (c : Cfg (k + 3) TM.PairBuildPhase) : Cfg (k + 3) (GuessVerifyPhase M.Q)

Wrap a pair-builder configuration into the composed machine.

Equations

• Complexity.SAT.satPairWrap M c = { state := Complexity.SAT.GuessVerifyPhase.pair c.state, input := c.input, work := c.work, output := c.output }

def Complexity.SAT.satVerifyWrap {k : ℕ} (M : TM k) (c : Cfg (k + 3) M.Q) : Cfg (k + 3) (GuessVerifyPhase M.Q)

Wrap a verifier configuration into the composed machine.

Equations

• Complexity.SAT.satVerifyWrap M c = { state := Complexity.SAT.GuessVerifyPhase.verify c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.SAT.satGuessVerify_verify_halted_iff {k : ℕ} (M : TM k) (c : Cfg (k + 3) M.Q) : (satGuessVerifyNTM M).halted (satVerifyWrap M c) ↔ (satVerifyPhaseTM M).halted c

The composed machine halts on a wrapped verifier configuration exactly when the verifier-phase machine halts on the unwrapped one.

def Complexity.SAT.satBoundaryInput (inp : Tape) : Tape

Tape effect of a SAT phase boundary on the real input tape.

Equations

• Complexity.SAT.satBoundaryInput inp = inp.move (Complexity.TM.idleDir inp.read)

def Complexity.SAT.satBoundaryWork {k : ℕ} (work : Fin (k + 3) → Tape) : Fin (k + 3) → Tape

Tape effect of a SAT phase boundary on the work tapes.

Equations

• Complexity.SAT.satBoundaryWork work i = (work i).writeAndMove (Complexity.TM.readBackWrite (work i).read).toΓ (Complexity.TM.idleDir (work i).read)

def Complexity.SAT.satBoundaryOutput (out : Tape) : Tape

Tape effect of a SAT phase boundary on the output tape.

Equations

• Complexity.SAT.satBoundaryOutput out = out.writeAndMove (Complexity.TM.readBackWrite out.read).toΓ (Complexity.TM.idleDir out.read)

theorem Complexity.SAT.satBoundaryInput_stable (inp : Tape) (hhead : inp.head ≥ 1) (hns : ∀ j ≥ 1, inp.cells j ≠ Γ.start) : satBoundaryInput inp = inp

A phase boundary leaves the input tape unchanged when its head is past cell zero and no start markers occur beyond cell zero.

theorem Complexity.SAT.satBoundaryWork_stable {k : ℕ} (work : Fin (k + 3) → Tape) (i : Fin (k + 3)) (hhead : (work i).head ≥ 1) (hns : ∀ j ≥ 1, (work i).cells j ≠ Γ.start) : satBoundaryWork work i = work i

A phase boundary leaves a work tape unchanged when its head is past cell zero and no start markers occur beyond cell zero.

theorem Complexity.SAT.satBoundaryWork_stable_of_read_ne_start {k : ℕ} (work : Fin (k + 3) → Tape) (i : Fin (k + 3)) (hread : (work i).read ≠ Γ.start) : satBoundaryWork work i = work i

A phase boundary leaves a work tape unchanged when it is not currently reading a start marker.

theorem Complexity.SAT.satPair_cells_ne_start_of_initTape_ofBool_move_right {k : ℕ} (M : TM k) (bits : List Bool) (c : Cfg (k + 3) M.Q) (hpair : c.work (satPairIdx k) = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right) (j : ℕ) : j ≥ 1 → (c.work (satPairIdx k)).cells j ≠ Γ.start

Exact initialized Boolean contents on the SAT pair tape imply the clean-tape invariant required by the verifier phase.

theorem Complexity.SAT.satBoundaryWork_stable_all {k : ℕ} (work : Fin (k + 3) → Tape) (hhead : ∀ (i : Fin (k + 3)), (work i).head ≥ 1) (hns : ∀ (i : Fin (k + 3)), ∀ j ≥ 1, (work i).cells j ≠ Γ.start) : satBoundaryWork work = work

A phase boundary leaves every work tape unchanged when all heads are past cell zero and no start markers occur beyond cell zero.

theorem Complexity.SAT.satBoundaryOutput_stable (out : Tape) (hhead : out.head ≥ 1) (hns : ∀ j ≥ 1, out.cells j ≠ Γ.start) : satBoundaryOutput out = out

A phase boundary leaves the output tape unchanged when its head is past cell zero and no start markers occur beyond cell zero.

theorem Complexity.SAT.satBoundaryOutput_stable_of_read_ne_start (out : Tape) (hread : out.read ≠ Γ.start) : satBoundaryOutput out = out

A phase boundary leaves the output tape unchanged when it is not currently reading a start marker.

theorem Complexity.SAT.satGuessVerify_counter_trace_one {k : ℕ} (M : TM k) (choice : Bool) (c : Cfg (k + 3) TM.LinearCounterPhase) (hstate : c.state ≠ TM.LinearCounterPhase.done) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) (satCounterWrap M c) = satCounterWrap M ((TM.inputLengthPlusOneCounterTM (satCounterIdx k)).toNTM.trace 1 (fun (x : Fin 1) => choice) c)

One composed-machine step on a non-done counter configuration simulates one step of the counter subroutine.

theorem Complexity.SAT.satGuessVerify_counter_trace_prefix {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) TM.LinearCounterPhase) : (∀ (t : ℕ) (ht : t < T), ((TM.inputLengthPlusOneCounterTM (satCounterIdx k)).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ TM.LinearCounterPhase.done) → (satGuessVerifyNTM M).trace T choices (satCounterWrap M c) = satCounterWrap M ((TM.inputLengthPlusOneCounterTM (satCounterIdx k)).toNTM.trace T choices c)

Multi-step counter-phase simulation up to, but not across, the counter subroutine's halt state.

theorem Complexity.SAT.satGuessVerify_counter_trace_exit {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin (T + 1) → Bool) (c : Cfg (k + 3) TM.LinearCounterPhase) (hnot : ∀ (t : ℕ) (ht : t < T), ((TM.inputLengthPlusOneCounterTM (satCounterIdx k)).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ TM.LinearCounterPhase.done) (hdone : ((TM.inputLengthPlusOneCounterTM (satCounterIdx k)).toNTM.trace T (fun (i : Fin T) => choices ⟨↑i, ⋯⟩) c).state = TM.LinearCounterPhase.done) : let counterNTM := (TM.inputLengthPlusOneCounterTM (satCounterIdx k)).toNTM; have counterChoices := fun (i : Fin T) => choices ⟨↑i, ⋯⟩; have cT := counterNTM.trace T counterChoices c; (satGuessVerifyNTM M).trace (T + 1) choices (satCounterWrap M c) = satRewindInputWrap M { state := TM.RewindPhase.moveLeft, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output }

If the counter subroutine first reaches done at time T, then the composed machine exits the counter phase on the next step.

theorem Complexity.SAT.satGuessVerify_counter_init_exits {k : ℕ} (M : TM k) (x : List Bool) (choices : Fin (TM.inputLengthPlusOneCounterTime x.length + 1) → Bool) : ∃ (t : ℕ) (ht : t ≤ TM.inputLengthPlusOneCounterTime x.length), let counterNTM := (TM.inputLengthPlusOneCounterTM (satCounterIdx k)).toNTM; have counterChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := TM.LinearCounterPhase.scan, input := Tape.init (List.map Γ.ofBool x), work := fun (x : Fin (k + 3)) => Tape.init [], output := Tape.init [] }; have cT := counterNTM.trace t counterChoices c0; (satGuessVerifyNTM M).trace (t + 1) (fun (i : Fin (t + 1)) => choices (Fin.castLE ⋯ i)) ((satGuessVerifyNTM M).initCfg x) = satRewindInputWrap M { state := TM.RewindPhase.moveLeft, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ (satBoundaryInput cT.input).cells 0 = Γ.start ∧ (∀ j ≥ 1, (satBoundaryInput cT.input).cells j ≠ Γ.start) ∧ (satBoundaryInput cT.input).cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ (satBoundaryInput cT.input).head ≤ TM.inputLengthPlusOneCounterTime x.length + 1 ∧ (satBoundaryWork cT.work (satCounterIdx k)).HasUnaryCounter (x.length + 1) ∧ (∀ (i : Fin (k + 3)), i ≠ satCounterIdx k → satBoundaryWork cT.work i = (Tape.init []).move Dir3.right) ∧ satBoundaryWork cT.work (satWitnessIdx k) = (Tape.init []).move Dir3.right ∧ satBoundaryWork cT.work (satPairIdx k) = (Tape.init []).move Dir3.right ∧ satBoundaryOutput cT.output = (Tape.init []).move Dir3.right

From the actual composed-machine initial configuration, the counter setup phase reaches the input-rewind phase within the counter bound plus the one boundary step.

theorem Complexity.SAT.satGuessVerify_rewindInput_trace_one {k : ℕ} (M : TM k) (choice : Bool) (c : Cfg (k + 3) TM.RewindPhase) (hstate : c.state ≠ TM.RewindPhase.done) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) (satRewindInputWrap M c) = satRewindInputWrap M (TM.rewindInputTM.toNTM.trace 1 (fun (x : Fin 1) => choice) c)

One composed-machine step on a non-done rewind configuration simulates one step of the input-rewind subroutine.

theorem Complexity.SAT.satGuessVerify_rewindInput_trace_prefix {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) TM.RewindPhase) : (∀ (t : ℕ) (ht : t < T), (TM.rewindInputTM.toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ TM.RewindPhase.done) → (satGuessVerifyNTM M).trace T choices (satRewindInputWrap M c) = satRewindInputWrap M (TM.rewindInputTM.toNTM.trace T choices c)

Multi-step input-rewind simulation up to, but not across, the rewind subroutine's halt state.

theorem Complexity.SAT.satGuessVerify_rewindInput_trace_exit {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin (T + 1) → Bool) (c : Cfg (k + 3) TM.RewindPhase) (hnot : ∀ (t : ℕ) (ht : t < T), (TM.rewindInputTM.toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ TM.RewindPhase.done) (hdone : (TM.rewindInputTM.toNTM.trace T (fun (i : Fin T) => choices ⟨↑i, ⋯⟩) c).state = TM.RewindPhase.done) : let rewindNTM := TM.rewindInputTM.toNTM; have rewindChoices := fun (i : Fin T) => choices ⟨↑i, ⋯⟩; have cT := rewindNTM.trace T rewindChoices c; (satGuessVerifyNTM M).trace (T + 1) choices (satRewindInputWrap M c) = satGuessWrap M { state := NTM.GuessBoundedPhase.choose, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output }

If the input-rewind subroutine first reaches done at time T, then the composed machine exits the rewind phase on the next step.

theorem Complexity.SAT.satGuessVerify_rewindInput_exits {k : ℕ} (M : TM k) (B : ℕ) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : inp.cells 0 = Γ.start ∧ (∀ j ≥ 1, inp.cells j ≠ Γ.start) ∧ inp.head ≤ B) (choices : Fin (B + 2 + 1) → Bool) : ∃ (t : ℕ) (ht : t ≤ B + 2), let rewindNTM := TM.rewindInputTM.toNTM; have rewindChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := TM.RewindPhase.moveLeft, input := inp, work := work, output := out }; have cT := rewindNTM.trace t rewindChoices c0; (satGuessVerifyNTM M).trace (t + 1) (fun (i : Fin (t + 1)) => choices (Fin.castLE ⋯ i)) (satRewindInputWrap M c0) = satGuessWrap M { state := NTM.GuessBoundedPhase.choose, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ (satBoundaryInput cT.input).head = 1

From a standard input-rewind phase start, the composed machine reaches bounded guessing within the input-rewind bound plus the one boundary step.

theorem Complexity.SAT.satGuessVerify_rewindInput_exits_with_frames {k : ℕ} (M : TM k) (B : ℕ) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : inp.cells 0 = Γ.start ∧ (∀ j ≥ 1, inp.cells j ≠ Γ.start) ∧ inp.head ≤ B) (hout : out.read ≠ Γ.start ∧ out.head ≥ 1) (hwork : ∀ (i : Fin (k + 3)), (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) (choices : Fin (B + 2 + 1) → Bool) : ∃ (t : ℕ) (ht : t ≤ B + 2), let rewindNTM := TM.rewindInputTM.toNTM; have rewindChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := TM.RewindPhase.moveLeft, input := inp, work := work, output := out }; have cT := rewindNTM.trace t rewindChoices c0; (satGuessVerifyNTM M).trace (t + 1) (fun (i : Fin (t + 1)) => choices (Fin.castLE ⋯ i)) (satRewindInputWrap M c0) = satGuessWrap M { state := NTM.GuessBoundedPhase.choose, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ (satBoundaryInput cT.input).head = 1 ∧ (satBoundaryInput cT.input).cells = inp.cells ∧ satBoundaryWork cT.work = work ∧ satBoundaryOutput cT.output = out

Rich input-rewind exit theorem: in addition to reaching the guess phase with the input head restored, preserve all work tapes and output through the boundary when their heads are already past ▷.

theorem Complexity.SAT.satGuessVerify_rewindInput_exits_with_frames_exact_input {k : ℕ} (M : TM k) (B : ℕ) (x : List Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : inp.cells 0 = Γ.start ∧ (∀ j ≥ 1, inp.cells j ≠ Γ.start) ∧ inp.head ≤ B) (hinput_cells : inp.cells = (Tape.init (List.map Γ.ofBool x)).cells) (hout : out.read ≠ Γ.start ∧ out.head ≥ 1) (hwork : ∀ (i : Fin (k + 3)), (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) (choices : Fin (B + 2 + 1) → Bool) : ∃ (t : ℕ) (ht : t ≤ B + 2), let rewindNTM := TM.rewindInputTM.toNTM; have rewindChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := TM.RewindPhase.moveLeft, input := inp, work := work, output := out }; have cT := rewindNTM.trace t rewindChoices c0; (satGuessVerifyNTM M).trace (t + 1) (fun (i : Fin (t + 1)) => choices (Fin.castLE ⋯ i)) (satRewindInputWrap M c0) = satGuessWrap M { state := NTM.GuessBoundedPhase.choose, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ satBoundaryInput cT.input = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ satBoundaryWork cT.work = work ∧ satBoundaryOutput cT.output = out

Exact-input corollary of the rich rewind exit, specialized for an input tape whose cells are the initialized encoding of x.

theorem Complexity.SAT.satGuessVerify_guess_trace_one {k : ℕ} (M : TM k) (choice : Bool) (c : Cfg (k + 3) NTM.GuessBoundedPhase) (hstate : c.state ≠ NTM.GuessBoundedPhase.done) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) (satGuessWrap M c) = satGuessWrap M ((NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k)).trace 1 (fun (x : Fin 1) => choice) c)

One composed-machine step on a non-done guess configuration simulates one step of the bounded-guessing subroutine with the same choice bit.

theorem Complexity.SAT.satGuessVerify_guess_trace_prefix {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) NTM.GuessBoundedPhase) : (∀ (t : ℕ) (ht : t < T), ((NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k)).trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ NTM.GuessBoundedPhase.done) → (satGuessVerifyNTM M).trace T choices (satGuessWrap M c) = satGuessWrap M ((NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k)).trace T choices c)

Multi-step bounded-guess simulation up to, but not across, the guess subroutine's halt state.

theorem Complexity.SAT.satGuessVerify_guess_trace_exit {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin (T + 1) → Bool) (c : Cfg (k + 3) NTM.GuessBoundedPhase) (hnot : ∀ (t : ℕ) (ht : t < T), ((NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k)).trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ NTM.GuessBoundedPhase.done) (hdone : ((NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k)).trace T (fun (i : Fin T) => choices ⟨↑i, ⋯⟩) c).state = NTM.GuessBoundedPhase.done) : let guessNTM := NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k); have guessChoices := fun (i : Fin T) => choices ⟨↑i, ⋯⟩; have cT := guessNTM.trace T guessChoices c; (satGuessVerifyNTM M).trace (T + 1) choices (satGuessWrap M c) = satPairWrap M { state := TM.PairBuildPhase.init, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output }

If the bounded-guess subroutine first reaches done at time T, then the composed machine exits the guess phase on the next step.

theorem Complexity.SAT.satGuessVerify_guess_exits {k : ℕ} (M : TM k) (B : ℕ) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : (work (satWitnessIdx k)).HasBinaryPrefix [] ∧ (work (satWitnessIdx k)).cells 0 = Γ.start ∧ (work (satCounterIdx k)).HasUnaryCounter B) (choices : Fin (NTM.guessBoundedTime B 0 + 1) → Bool) : ∃ (t : ℕ) (_ht : t ≤ NTM.guessBoundedTime B 0), let guessNTM := NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k); have guessChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := NTM.GuessBoundedPhase.choose, input := inp, work := work, output := out }; have cT := guessNTM.trace t guessChoices c0; (satGuessVerifyNTM M).trace (t + 1) (fun (i : Fin (t + 1)) => choices (Fin.castLE ⋯ i)) (satGuessWrap M c0) = satPairWrap M { state := TM.PairBuildPhase.init, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ ∃ (y : List Bool), y.length ≤ B ∧ satBoundaryWork cT.work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right

From a standard bounded-guess phase start, the composed machine reaches pair building within the guess bound plus the one boundary step.

theorem Complexity.SAT.satGuessVerify_guess_exits_with_frames {k : ℕ} (M : TM k) (B : ℕ) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : (work (satWitnessIdx k)).HasBinaryPrefix [] ∧ (work (satWitnessIdx k)).cells 0 = Γ.start ∧ (work (satCounterIdx k)).HasUnaryCounter B ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) (hinp : inp.head ≥ 1 ∧ ∀ j ≥ 1, inp.cells j ≠ Γ.start) (hout : out.read ≠ Γ.start) (hwork : ∀ (i : Fin k), (work (satVerifierWorkIdx i)).read ≠ Γ.start) (choices : Fin (NTM.guessBoundedTime B 0 + 1) → Bool) : ∃ (t : ℕ) (_ht : t ≤ NTM.guessBoundedTime B 0) (y : List Bool), y.length ≤ B ∧ let guessNTM := NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k); have guessChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := NTM.GuessBoundedPhase.choose, input := inp, work := work, output := out }; have cT := guessNTM.trace t guessChoices c0; (satGuessVerifyNTM M).trace (t + 1) (fun (i : Fin (t + 1)) => choices (Fin.castLE ⋯ i)) (satGuessWrap M c0) = satPairWrap M { state := TM.PairBuildPhase.init, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ satBoundaryInput cT.input = inp ∧ satBoundaryWork cT.work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ satBoundaryWork cT.work (satPairIdx k) = (Tape.init []).move Dir3.right ∧ satBoundaryOutput cT.output = out ∧ ∀ (i : Fin k), satBoundaryWork cT.work (satVerifierWorkIdx i) = work (satVerifierWorkIdx i)

Arbitrary-choice guess exit with the frame facts needed by pair building: the produced witness is bounded by the counter, while the real input, pair tape, output, and verifier work tapes are preserved through the boundary.

theorem Complexity.SAT.satGuessVerify_guess_generates_with_pair_frame {k : ℕ} (M : TM k) (B : ℕ) (y : List Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) (hlen : y.length ≤ B) (hpre : (work (satWitnessIdx k)).HasBinaryPrefix [] ∧ (work (satWitnessIdx k)).cells 0 = Γ.start ∧ (work (satCounterIdx k)).HasUnaryCounter B ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) : ∃ (t : ℕ) (_ : t ≤ NTM.guessBoundedTime B 0) (choices : Fin (t + 1) → Bool), let guessNTM := NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k); have guessChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := NTM.GuessBoundedPhase.choose, input := inp, work := work, output := out }; have cT := guessNTM.trace t guessChoices c0; (satGuessVerifyNTM M).trace (t + 1) choices (satGuessWrap M c0) = satPairWrap M { state := TM.PairBuildPhase.init, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ satBoundaryWork cT.work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ satBoundaryWork cT.work (satPairIdx k) = (Tape.init []).move Dir3.right

Completeness-oriented guess exit: for any requested witness within the unary counter bound, there is a nondeterministic choice sequence that exits the guess phase with exactly that witness and leaves the pair tape blank.

theorem Complexity.SAT.satGuessVerify_guess_generates_with_input_pair_frame {k : ℕ} (M : TM k) (B : ℕ) (x y : List Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) (hlen : y.length ≤ B) (hinput : inp = (Tape.init (List.map Γ.ofBool x)).move Dir3.right) (hpre : (work (satWitnessIdx k)).HasBinaryPrefix [] ∧ (work (satWitnessIdx k)).cells 0 = Γ.start ∧ (work (satCounterIdx k)).HasUnaryCounter B ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) : ∃ (t : ℕ) (_ : t ≤ NTM.guessBoundedTime B 0) (choices : Fin (t + 1) → Bool), let guessNTM := NTM.guessBoundedNTM (satWitnessIdx k) (satCounterIdx k); have guessChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := NTM.GuessBoundedPhase.choose, input := inp, work := work, output := out }; have cT := guessNTM.trace t guessChoices c0; (satGuessVerifyNTM M).trace (t + 1) choices (satGuessWrap M c0) = satPairWrap M { state := TM.PairBuildPhase.init, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ satBoundaryInput cT.input = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ satBoundaryWork cT.work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ satBoundaryWork cT.work (satPairIdx k) = (Tape.init []).move Dir3.right

Started-input strengthening of satGuessVerify_guess_generates_with_pair_frame. Besides producing the requested witness and preserving the blank pair tape, the phase exit keeps the exact started input tape needed by pair building.

theorem Complexity.SAT.satGuessVerify_rewind_then_guess_generates_pair {k : ℕ} (M : TM k) (B : ℕ) (x y : List Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) (hrewindPre : inp.cells 0 = Γ.start ∧ (∀ j ≥ 1, inp.cells j ≠ Γ.start) ∧ inp.head ≤ B) (hinput_cells : inp.cells = (Tape.init (List.map Γ.ofBool x)).cells) (hout : out.read ≠ Γ.start ∧ out.head ≥ 1) (hwork : ∀ (i : Fin (k + 3)), (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) (hlen : y.length ≤ x.length + 1) (hguessPre : (work (satWitnessIdx k)).HasBinaryPrefix [] ∧ (work (satWitnessIdx k)).cells 0 = Γ.start ∧ (work (satCounterIdx k)).HasUnaryCounter (x.length + 1) ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) : ∃ (T : ℕ) (choices : Fin T → Bool) (cPair : Cfg (k + 3) TM.PairBuildPhase), T ≤ B + 2 + 1 + (NTM.guessBoundedTime (x.length + 1) 0 + 1) ∧ (satGuessVerifyNTM M).trace T choices (satRewindInputWrap M { state := TM.RewindPhase.moveLeft, input := inp, work := work, output := out }) = satPairWrap M cPair ∧ cPair.state = TM.PairBuildPhase.init ∧ cPair.input = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ cPair.work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ cPair.work (satPairIdx k) = (Tape.init []).move Dir3.right ∧ cPair.output = out ∧ ∀ (i : Fin k), cPair.work (satVerifierWorkIdx i) = work (satVerifierWorkIdx i)

Compose input rewind with the completeness-oriented guess phase. Starting from a rewind configuration whose work/output frames already satisfy the guess preconditions, there is a choice sequence reaching pair-building with exact input, witness, and blank pair tapes.

theorem Complexity.SAT.satGuessVerify_setup_generates_pair {k : ℕ} (M : TM k) (x y : List Bool) (hlen : y.length ≤ x.length + 1) : ∃ (T : ℕ) (choices : Fin T → Bool) (cPair : Cfg (k + 3) TM.PairBuildPhase), T ≤ TM.inputLengthPlusOneCounterTime x.length + 1 + (TM.inputLengthPlusOneCounterTime x.length + 1 + 2 + 1 + (NTM.guessBoundedTime (x.length + 1) 0 + 1)) ∧ (satGuessVerifyNTM M).trace T choices ((satGuessVerifyNTM M).initCfg x) = satPairWrap M cPair ∧ cPair.state = TM.PairBuildPhase.init ∧ cPair.input = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ cPair.work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ cPair.work (satPairIdx k) = (Tape.init []).move Dir3.right ∧ cPair.output = (Tape.init []).move Dir3.right ∧ ∀ (i : Fin k), cPair.work (satVerifierWorkIdx i) = (Tape.init []).move Dir3.right

Compose counter setup, input rewind, and the completeness-oriented guess phase from the actual composed-machine initial configuration. The result is a pair-phase configuration with exact input, requested witness, and a blank pair tape.

theorem Complexity.SAT.satGuessVerify_setup_exits_with_pair_frames {k : ℕ} (M : TM k) (x : List Bool) (choices : Fin (satGuessVerifySetupTime x.length) → Bool) : ∃ (T : ℕ) (hT : T ≤ satGuessVerifySetupTime x.length) (y : List Bool), y.length ≤ x.length + 1 ∧ ∃ (cPair : Cfg (k + 3) TM.PairBuildPhase), have setupChoices := fun (i : Fin T) => choices (Fin.castLE hT i); (satGuessVerifyNTM M).trace T setupChoices ((satGuessVerifyNTM M).initCfg x) = satPairWrap M cPair ∧ cPair.state = TM.PairBuildPhase.init ∧ cPair.input = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ cPair.work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ cPair.work (satPairIdx k) = (Tape.init []).move Dir3.right ∧ cPair.output = (Tape.init []).move Dir3.right ∧ ∀ (i : Fin k), cPair.work (satVerifierWorkIdx i) = (Tape.init []).move Dir3.right

Arbitrary-choice setup composition from the real initial configuration. Within the setup budget, every setup choice prefix reaches pair building with some bounded witness, exact started input, blank pair/output tapes, and blank verifier work tapes.

theorem Complexity.SAT.satGuessVerify_pair_trace_one {k : ℕ} (M : TM k) (choice : Bool) (c : Cfg (k + 3) TM.PairBuildPhase) (hstate : c.state ≠ TM.PairBuildPhase.done) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) (satPairWrap M c) = satPairWrap M ((TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM.trace 1 (fun (x : Fin 1) => choice) c)

One composed-machine step on a non-done pair configuration simulates one step of the pair-builder subroutine.

theorem Complexity.SAT.satGuessVerify_pair_trace_prefix {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) TM.PairBuildPhase) : (∀ (t : ℕ) (ht : t < T), ((TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ TM.PairBuildPhase.done) → (satGuessVerifyNTM M).trace T choices (satPairWrap M c) = satPairWrap M ((TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM.trace T choices c)

Multi-step pair-builder simulation up to, but not across, the pair subroutine's halt state.

theorem Complexity.SAT.satGuessVerify_pair_trace_exit {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin (T + 1) → Bool) (c : Cfg (k + 3) TM.PairBuildPhase) (hnot : ∀ (t : ℕ) (ht : t < T), ((TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ TM.PairBuildPhase.done) (hdone : ((TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM.trace T (fun (i : Fin T) => choices ⟨↑i, ⋯⟩) c).state = TM.PairBuildPhase.done) : let pairNTM := (TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM; have pairChoices := fun (i : Fin T) => choices ⟨↑i, ⋯⟩; have cT := pairNTM.trace T pairChoices c; (satGuessVerifyNTM M).trace (T + 1) choices (satPairWrap M c) = satVerifyWrap M { state := verifierStartedState M, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output }

If the pair-builder subroutine first reaches done at time T, then the composed machine exits the pair phase on the next step.

theorem Complexity.SAT.satGuessVerify_pair_exits {k : ℕ} (M : TM k) (x y : List Bool) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) (choices : Fin (TM.pairBuildTime x.length y.length + 1) → Bool) : ∃ (t : ℕ) (ht : t ≤ TM.pairBuildTime x.length y.length), let pairNTM := (TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM; have pairChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; have cT := pairNTM.trace t pairChoices c0; (satGuessVerifyNTM M).trace (t + 1) (fun (i : Fin (t + 1)) => choices (Fin.castLE ⋯ i)) (satPairWrap M c0) = satVerifyWrap M { state := verifierStartedState M, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output } ∧ satBoundaryWork cT.work (satPairIdx k) = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right

From a standard pair-builder phase start, the composed machine reaches verifier simulation within the pair-builder bound plus the one boundary step.

theorem Complexity.SAT.satGuessVerify_pair_exits_with_verifier_frames {k : ℕ} (M : TM k) (x y : List Bool) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) (hout : out.read ≠ Γ.start) (hwork : ∀ (i : Fin k), (work (satVerifierWorkIdx i)).read ≠ Γ.start) (choices : Fin (TM.pairBuildTime x.length y.length + 1) → Bool) : ∃ (t : ℕ) (ht : t ≤ TM.pairBuildTime x.length y.length), let pairNTM := (TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM; have pairChoices := fun (i : Fin t) => choices ⟨↑i, ⋯⟩; have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; have cT := pairNTM.trace t pairChoices c0; have cVerify := { state := verifierStartedState M, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output }; (satGuessVerifyNTM M).trace (t + 1) (fun (i : Fin (t + 1)) => choices (Fin.castLE ⋯ i)) (satPairWrap M c0) = satVerifyWrap M cVerify ∧ cVerify.work (satPairIdx k) = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right ∧ cVerify.output = out ∧ ∀ (i : Fin k), cVerify.work (satVerifierWorkIdx i) = work (satVerifierWorkIdx i)

Pair-builder exit with the verifier frame exposed. Besides the exact pair tape, this packages preservation of the output tape and every internal verifier work tape through pair construction and the boundary step.

theorem Complexity.SAT.satGuessVerify_verify_trace_one {k : ℕ} (M : TM k) (choice : Bool) (c : Cfg (k + 3) M.Q) (hstate : c.state ≠ M.qhalt) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) (satVerifyWrap M c) = satVerifyWrap M ((satVerifyPhaseTM M).toNTM.trace 1 (fun (x : Fin 1) => choice) c)

One composed-machine step on a non-halted verifier configuration simulates one step of the verifier-phase machine.

theorem Complexity.SAT.satGuessVerify_verify_trace_prefix {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) : (∀ (t : ℕ) (ht : t < T), ((satVerifyPhaseTM M).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ M.qhalt) → (satGuessVerifyNTM M).trace T choices (satVerifyWrap M c) = satVerifyWrap M ((satVerifyPhaseTM M).toNTM.trace T choices c)

Multi-step verifier-phase simulation up to, but not across, M's halt state.

theorem Complexity.SAT.satGuessVerify_verify_halts_of_phase_halts {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) (hhalt : (satVerifyPhaseTM M).halted ((satVerifyPhaseTM M).toNTM.trace T choices c)) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace T choices (satVerifyWrap M c))

If the verifier phase has halted by time T, then the composed SAT machine, started in verifier phase, is halted by time T as well.

theorem Complexity.SAT.satGuessVerify_verify_halts_of_inner_trace_halts {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) (hpair : ∀ (t : ℕ) (ht : t < T), have ct := (satVerifyPhaseTM M).toNTM.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c; (ct.work (satPairIdx k)).head = 0 ∨ (ct.work (satPairIdx k)).read ≠ Γ.start) (hinner : M.halted (M.toNTM.trace T choices (satVerifyInnerCfg M c))) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace T choices (satVerifyWrap M c))

If the projected verifier computation halts, then the full SAT machine started in verifier phase halts under the same time bound.

theorem Complexity.SAT.satGuessVerify_verify_halts_of_inner_trace_halts_clean {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) (hclean : ∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) (hinner : M.halted (M.toNTM.trace T choices (satVerifyInnerCfg M c))) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace T choices (satVerifyWrap M c))

If the projected verifier computation halts and the SAT pair tape is clean, then the full SAT machine started in verifier phase halts under the same time bound.

theorem Complexity.SAT.satGuessVerify_verify_outputs_of_inner_trace_output_clean {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) (hclean : ∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) (g : Γ) (hinnerHalt : M.halted (M.toNTM.trace T choices (satVerifyInnerCfg M c))) (hinnerOut : (M.toNTM.trace T choices (satVerifyInnerCfg M c)).output.cells 1 = g) : have cFinal := (satGuessVerifyNTM M).trace T choices (satVerifyWrap M c); (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = g

If the projected verifier computation halts with accepting output and the SAT pair tape is clean, then the full SAT machine started in verifier phase also halts with accepting output.

theorem Complexity.SAT.satGuessVerify_verify_accepts_of_inner_trace_accepts_clean {k : ℕ} (M : TM k) (T : ℕ) (choices : Fin T → Bool) (c : Cfg (k + 3) M.Q) (hclean : ∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) (hinnerHalt : M.halted (M.toNTM.trace T choices (satVerifyInnerCfg M c))) (hinnerOut : (M.toNTM.trace T choices (satVerifyInnerCfg M c)).output.cells 1 = Γ.one) : have cFinal := (satGuessVerifyNTM M).trace T choices (satVerifyWrap M c); (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = Γ.one

If the projected verifier computation halts with accepting output and the SAT pair tape is clean, then the full SAT machine started in verifier phase also halts with accepting output.

theorem Complexity.SAT.satGuessVerify_halts_after_verify_prefix {k : ℕ} (M : TM k) (T V : ℕ) (choices : Fin (T + V) → Bool) (c0 : Cfg (k + 3) (GuessVerifyPhase M.Q)) (c : Cfg (k + 3) M.Q) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) c0 = satVerifyWrap M c) (hclean : ∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) (hinner : M.halted (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c))) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (T + V) choices c0)

If a composed SAT trace prefix has reached the verifier phase, then any halting projected verifier suffix gives a halting full composed trace.

theorem Complexity.SAT.satGuessVerify_accepts_after_verify_prefix {k : ℕ} (M : TM k) (T V : ℕ) (choices : Fin (T + V) → Bool) (c0 : Cfg (k + 3) (GuessVerifyPhase M.Q)) (c : Cfg (k + 3) M.Q) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) c0 = satVerifyWrap M c) (hclean : ∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) (hinnerHalt : M.halted (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c))) (hinnerOut : (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c)).output.cells 1 = Γ.one) : have cFinal := (satGuessVerifyNTM M).trace (T + V) choices c0; (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = Γ.one

If a composed SAT trace prefix has reached the verifier phase, then any accepting projected verifier suffix gives an accepting full composed trace.

theorem Complexity.SAT.satGuessVerify_outputs_after_verify_prefix {k : ℕ} (M : TM k) (T V : ℕ) (choices : Fin (T + V) → Bool) (c0 : Cfg (k + 3) (GuessVerifyPhase M.Q)) (c : Cfg (k + 3) M.Q) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) c0 = satVerifyWrap M c) (hclean : ∀ j ≥ 1, (c.work (satPairIdx k)).cells j ≠ Γ.start) (g : Γ) (hinnerHalt : M.halted (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c))) (hinnerOut : (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c)).output.cells 1 = g) : have cFinal := (satGuessVerifyNTM M).trace (T + V) choices c0; (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = g

If a composed SAT trace prefix has reached the verifier phase, then any projected verifier suffix preserves its final output cell through the composed machine.

theorem Complexity.SAT.satGuessVerify_halts_after_prefix {k : ℕ} (M : TM k) (T U : ℕ) (choices : Fin (T + U) → Bool) (c0 c1 : Cfg (k + 3) (GuessVerifyPhase M.Q)) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) c0 = c1) (hsuffix : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace U (fun (i : Fin U) => choices (Fin.natAdd T i)) c1)) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (T + U) choices c0)

Generic trace composition for the composed SAT machine: if a prefix reaches a configuration whose suffix trace halts, then the combined trace halts.

theorem Complexity.SAT.satGuessVerify_accepts_after_prefix {k : ℕ} (M : TM k) (T U : ℕ) (choices : Fin (T + U) → Bool) (c0 c1 : Cfg (k + 3) (GuessVerifyPhase M.Q)) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) c0 = c1) (hsuffix : have cFinal := (satGuessVerifyNTM M).trace U (fun (i : Fin U) => choices (Fin.natAdd T i)) c1; (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = Γ.one) : have cFinal := (satGuessVerifyNTM M).trace (T + U) choices c0; (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = Γ.one

Generic trace composition for the composed SAT machine: if a prefix reaches a configuration whose suffix trace accepts, then the combined trace accepts.

theorem Complexity.SAT.satGuessVerify_guess_exit_then_suffix_halts {k : ℕ} (M : TM k) (T U : ℕ) (choices : Fin (T + U) → Bool) (c0 : Cfg (k + 3) NTM.GuessBoundedPhase) (cPair : Cfg (k + 3) TM.PairBuildPhase) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) (satGuessWrap M c0) = satPairWrap M cPair) (hsuffix : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace U (fun (i : Fin U) => choices (Fin.natAdd T i)) (satPairWrap M cPair))) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (T + U) choices (satGuessWrap M c0))

Guess-phase exit followed by any halting pair/verifier suffix gives a halting combined run.

theorem Complexity.SAT.satGuessVerify_rewindInput_exit_then_suffix_halts {k : ℕ} (M : TM k) (T U : ℕ) (choices : Fin (T + U) → Bool) (c0 : Cfg (k + 3) TM.RewindPhase) (cGuess : Cfg (k + 3) NTM.GuessBoundedPhase) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) (satRewindInputWrap M c0) = satGuessWrap M cGuess) (hsuffix : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace U (fun (i : Fin U) => choices (Fin.natAdd T i)) (satGuessWrap M cGuess))) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (T + U) choices (satRewindInputWrap M c0))

Input-rewind exit followed by any halting guess/pair/verifier suffix gives a halting combined run.

theorem Complexity.SAT.satGuessVerify_counter_exit_then_suffix_halts {k : ℕ} (M : TM k) (T U : ℕ) (choices : Fin (T + U) → Bool) (c0 : Cfg (k + 3) TM.LinearCounterPhase) (cRewind : Cfg (k + 3) TM.RewindPhase) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) (satCounterWrap M c0) = satRewindInputWrap M cRewind) (hsuffix : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace U (fun (i : Fin U) => choices (Fin.natAdd T i)) (satRewindInputWrap M cRewind))) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (T + U) choices (satCounterWrap M c0))

Counter-setup exit followed by any halting rewind/guess/pair/verifier suffix gives a halting combined run.

theorem Complexity.SAT.satGuessVerify_pair_exit_then_verify_halts {k : ℕ} (M : TM k) (x y : List Bool) (T V : ℕ) (choices : Fin (T + V) → Bool) (c0 : Cfg (k + 3) TM.PairBuildPhase) (c : Cfg (k + 3) M.Q) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) (satPairWrap M c0) = satVerifyWrap M c) (hpair : c.work (satPairIdx k) = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right) (hinner : M.halted (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c))) : (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (T + V) choices (satPairWrap M c0))

Pair-builder-to-verifier composition: once a SAT trace prefix has exited the pair phase with the exact encoded (x, y) pair tape, a halting projected verifier suffix makes the full composed machine halt.

theorem Complexity.SAT.satGuessVerify_pair_exit_then_verify_accepts {k : ℕ} (M : TM k) (x y : List Bool) (T V : ℕ) (choices : Fin (T + V) → Bool) (c0 : Cfg (k + 3) TM.PairBuildPhase) (c : Cfg (k + 3) M.Q) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) (satPairWrap M c0) = satVerifyWrap M c) (hpair : c.work (satPairIdx k) = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right) (hinnerHalt : M.halted (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c))) (hinnerOut : (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c)).output.cells 1 = Γ.one) : have cFinal := (satGuessVerifyNTM M).trace (T + V) choices (satPairWrap M c0); (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = Γ.one

Pair-builder-to-verifier composition with accepting output.

theorem Complexity.SAT.satGuessVerify_pair_exit_then_verify_outputs {k : ℕ} (M : TM k) (x y : List Bool) (T V : ℕ) (choices : Fin (T + V) → Bool) (c0 : Cfg (k + 3) TM.PairBuildPhase) (c : Cfg (k + 3) M.Q) (hprefix : (satGuessVerifyNTM M).trace T (fun (i : Fin T) => choices (Fin.castLE ⋯ i)) (satPairWrap M c0) = satVerifyWrap M c) (hpair : c.work (satPairIdx k) = (Tape.init (List.map Γ.ofBool (pair x y))).move Dir3.right) (g : Γ) (hinnerHalt : M.halted (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c))) (hinnerOut : (M.toNTM.trace V (fun (i : Fin V) => choices (Fin.natAdd T i)) (satVerifyInnerCfg M c)).output.cells 1 = g) : have cFinal := (satGuessVerifyNTM M).trace (T + V) choices (satPairWrap M c0); (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = g

Pair-builder-to-verifier composition preserving the projected verifier's final output cell.

theorem Complexity.SAT.satGuessVerify_pair_exits_then_verify_halts {k : ℕ} (M : TM k) (x y : List Bool) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) (V : ℕ) (choices : Fin (TM.pairBuildTime x.length y.length + 1 + V) → Bool) (hinner : ∀ (t : ℕ) (ht : t ≤ TM.pairBuildTime x.length y.length), let pairNTM := (TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM; have runChoices := fun (i : Fin (t + 1 + V)) => choices (Fin.castLE ⋯ i); have pairChoices := fun (i : Fin t) => runChoices ⟨↑i, ⋯⟩; have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; have cT := pairNTM.trace t pairChoices c0; have cVerify := { state := verifierStartedState M, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output }; M.halted (M.toNTM.trace V (fun (i : Fin V) => runChoices (Fin.natAdd (t + 1) i)) (satVerifyInnerCfg M cVerify))) : ∃ (t : ℕ) (ht : t ≤ TM.pairBuildTime x.length y.length), have runChoices := fun (i : Fin (t + 1 + V)) => choices (Fin.castLE ⋯ i); have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (t + 1 + V) runChoices (satPairWrap M c0))

Bounded pair-building followed by a halting verifier suffix gives a bounded halting run of the composed machine. The existential t is the first pair-builder halt time supplied by satGuessVerify_pair_exits.

theorem Complexity.SAT.satGuessVerify_pair_start_halts_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x y : List Bool) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) (hout : out = (Tape.init []).move Dir3.right) (hwork : ∀ (i : Fin k), work (satVerifierWorkIdx i) = (Tape.init []).move Dir3.right) : ∃ (V : ℕ), V + 1 ≤ f (pair x y).length ∧ ∃ (t : ℕ) (_ : t ≤ TM.pairBuildTime x.length y.length) (choices : Fin (t + 1 + V) → Bool), have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (t + 1 + V) choices (satPairWrap M c0))

Pair-start completeness with a real deciding verifier. If the pair phase starts from exact input/witness/pair tapes and blank verifier frame tapes, then pair construction followed by verifier simulation halts.

theorem Complexity.SAT.satGuessVerify_pair_start_halts_within_bound_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x y : List Bool) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) (hout : out = (Tape.init []).move Dir3.right) (hwork : ∀ (i : Fin k), work (satVerifierWorkIdx i) = (Tape.init []).move Dir3.right) (hlen : y.length ≤ x.length + 1) (choices : Fin (TM.pairBuildTime x.length (x.length + 1) + satVerifierWindowTime f x.length) → Bool) : have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace (TM.pairBuildTime x.length (x.length + 1) + satVerifierWindowTime f x.length) choices (satPairWrap M c0))

Pair-start all-path halting under the uniform SAT witness bound. Once the witness tape contains any y with |y| ≤ |x|+1, every remaining choice sequence reaches a halt within the pair-builder worst-case plus verifier window budget.

theorem Complexity.SAT.satGuessVerify_pair_start_decides_within_bound_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x y : List Bool) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) (hout : out = (Tape.init []).move Dir3.right) (hwork : ∀ (i : Fin k), work (satVerifierWorkIdx i) = (Tape.init []).move Dir3.right) (hlen : y.length ≤ x.length + 1) (choices : Fin (TM.pairBuildTime x.length (x.length + 1) + satVerifierWindowTime f x.length) → Bool) : have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; have cFinal := (satGuessVerifyNTM M).trace (TM.pairBuildTime x.length (x.length + 1) + satVerifierWindowTime f x.length) choices (satPairWrap M c0); (satGuessVerifyNTM M).halted cFinal ∧ (pair x y ∈ L → cFinal.output.cells 1 = Γ.one) ∧ (pair x y ∉ L → cFinal.output.cells 1 = Γ.zero)

Pair-start bounded deciding suffix under the uniform SAT witness bound. Once setup has produced a bounded witness y, every remaining choice sequence halts within the pair/verifier window and outputs the correct verifier bit for pair x y.

theorem Complexity.SAT.satGuessVerify_pair_start_accepts_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x y : List Bool) (work : Fin (k + 3) → Tape) (out : Tape) (hpre : work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ work (satPairIdx k) = (Tape.init []).move Dir3.right) (hout : out = (Tape.init []).move Dir3.right) (hwork : ∀ (i : Fin k), work (satVerifierWorkIdx i) = (Tape.init []).move Dir3.right) (hmem : pair x y ∈ L) : ∃ (V : ℕ), V + 1 ≤ f (pair x y).length ∧ ∃ (t : ℕ) (_ : t ≤ TM.pairBuildTime x.length y.length) (choices : Fin (t + 1 + V) → Bool), have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; have cFinal := (satGuessVerifyNTM M).trace (t + 1 + V) choices (satPairWrap M c0); (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = Γ.one

Pair-start completeness with accepting output from a real deciding verifier.

theorem Complexity.SAT.satGuessVerify_init_generates_witness_then_verify_halts {k : ℕ} (M : TM k) (x y : List Bool) (V : ℕ) (hlen : y.length ≤ x.length + 1) (hinner : ∀ (work : Fin (k + 3) → Tape) (out : Tape), work (satWitnessIdx k) = (Tape.init (List.map Γ.ofBool y)).move Dir3.right → work (satPairIdx k) = (Tape.init []).move Dir3.right → ∀ t ≤ TM.pairBuildTime x.length y.length, let pairNTM := (TM.pairBuildTM (satWitnessIdx k) (satPairIdx k)).toNTM; have c0 := { state := TM.PairBuildPhase.init, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := work, output := out }; have cT := pairNTM.trace t (fun (x : Fin t) => false) c0; have cVerify := { state := verifierStartedState M, input := satBoundaryInput cT.input, work := satBoundaryWork cT.work, output := satBoundaryOutput cT.output }; M.halted (M.toNTM.trace V (fun (x : Fin V) => false) (satVerifyInnerCfg M cVerify))) : ∃ (T : ℕ) (choices : Fin T → Bool), T ≤ TM.inputLengthPlusOneCounterTime x.length + 1 + (TM.inputLengthPlusOneCounterTime x.length + 1 + 2 + 1 + (NTM.guessBoundedTime (x.length + 1) 0 + 1)) + (TM.pairBuildTime x.length y.length + 1 + V) ∧ (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace T choices ((satGuessVerifyNTM M).initCfg x))

End-to-end SAT-specialized completeness spine. If a target witness y fits the SAT linear witness bound and the projected verifier suffix halts from every possible pair-builder first halt for the exact (x, y) pair setup, then there is a full nondeterministic run of satGuessVerifyNTM M from the real initial configuration that halts.

theorem Complexity.SAT.satGuessVerify_init_generates_witness_halts_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x y : List Bool) (hlen : y.length ≤ x.length + 1) : ∃ (T : ℕ) (choices : Fin T → Bool), T ≤ TM.inputLengthPlusOneCounterTime x.length + 1 + (TM.inputLengthPlusOneCounterTime x.length + 1 + 2 + 1 + (NTM.guessBoundedTime (x.length + 1) 0 + 1)) + (TM.pairBuildTime x.length y.length + f (pair x y).length) ∧ (satGuessVerifyNTM M).halted ((satGuessVerifyNTM M).trace T choices ((satGuessVerifyNTM M).initCfg x))

End-to-end completeness halting from a real deciding verifier. For any SAT witness candidate y within the linear bound, the SAT-specialized guess-and-verify machine has a nondeterministic run from its real initial configuration that reaches a halted state.

theorem Complexity.SAT.satGuessVerify_init_generates_witness_accepts_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x y : List Bool) (hlen : y.length ≤ x.length + 1) (hmem : pair x y ∈ L) : ∃ (T : ℕ) (choices : Fin T → Bool), T ≤ TM.inputLengthPlusOneCounterTime x.length + 1 + (TM.inputLengthPlusOneCounterTime x.length + 1 + 2 + 1 + (NTM.guessBoundedTime (x.length + 1) 0 + 1)) + (TM.pairBuildTime x.length y.length + f (pair x y).length) ∧ have cFinal := (satGuessVerifyNTM M).trace T choices ((satGuessVerifyNTM M).initCfg x); (satGuessVerifyNTM M).halted cFinal ∧ cFinal.output.cells 1 = Γ.one

End-to-end accepting completeness from a real deciding verifier. For any SAT witness candidate y within the linear bound whose encoded pair is in the verifier language, the SAT-specialized guess-and-verify machine has a nondeterministic accepting run from its real initial configuration.

theorem Complexity.SAT.satGuessVerify_acceptsInTime_of_witness_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x y : List Bool) (hlen : y.length ≤ x.length + 1) (hmem : pair x y ∈ L) : (satGuessVerifyNTM M).AcceptsInTime x (TM.inputLengthPlusOneCounterTime x.length + 1 + (TM.inputLengthPlusOneCounterTime x.length + 1 + 2 + 1 + (NTM.guessBoundedTime (x.length + 1) 0 + 1)) + (TM.pairBuildTime x.length y.length + f (pair x y).length))

The end-to-end accepting completeness theorem packaged in the standard NTM.AcceptsInTime interface, using the concrete witness-dependent run budget from the phase construction.

theorem Complexity.SAT.satGuessVerify_acceptsInTime_of_witness_bound_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x y : List Bool) (hlen : y.length ≤ x.length + 1) (hmem : pair x y ∈ L) : (satGuessVerifyNTM M).AcceptsInTime x (satGuessVerifyTime f x.length)

The accepting witness run under the uniform SAT-specialized bound depending only on |x| and the verifier time window.

theorem Complexity.SAT.satGuessVerify_acceptsInTime_of_RSAT_of_decidesInTime {k : ℕ} (M : TM k) {f : ℕ → ℕ} (hM : M.DecidesInTime (pairLang Witness) f) (x y : List Bool) (hR : Witness x y) : (satGuessVerifyNTM M).AcceptsInTime x (TM.inputLengthPlusOneCounterTime x.length + 1 + (TM.inputLengthPlusOneCounterTime x.length + 1 + 2 + 1 + (NTM.guessBoundedTime (x.length + 1) 0 + 1)) + (TM.pairBuildTime x.length y.length + f (pair x y).length))

SAT-specific accepting run from any concrete satisfying assignment, assuming M decides the SAT verifier pair language.

theorem Complexity.SAT.satGuessVerify_acceptsInTime_of_RSAT_bound_of_decidesInTime {k : ℕ} (M : TM k) {f : ℕ → ℕ} (hM : M.DecidesInTime (pairLang Witness) f) (x y : List Bool) (hR : Witness x y) : (satGuessVerifyNTM M).AcceptsInTime x (satGuessVerifyTime f x.length)

SAT-specific accepting run from any concrete satisfying assignment under the uniform SAT-specialized bound.

theorem Complexity.SAT.satGuessVerify_acceptsInTime_of_mem_LSAT_of_decidesInTime {k : ℕ} (M : TM k) {f : ℕ → ℕ} (hM : M.DecidesInTime (pairLang Witness) f) (x : List Bool) (hx : x ∈ language) : (satGuessVerifyNTM M).AcceptsInTime x (satGuessVerifyTime f x.length)

Timed yes-instance half for language under the uniform SAT-specialized bound, assuming M decides the SAT verifier pair language.

theorem Complexity.SAT.satGuessVerify_accepts_of_mem_LSAT_of_decidesInTime {k : ℕ} (M : TM k) {f : ℕ → ℕ} (hM : M.DecidesInTime (pairLang Witness) f) (x : List Bool) (hx : x ∈ language) : (satGuessVerifyNTM M).Accepts x

Yes-instances of language are accepted by the SAT-specialized guess-and-verify machine, assuming M decides the SAT verifier pair language. This is the unbounded acceptance half of the final NP decision theorem.

theorem Complexity.SAT.satGuessVerify_allPathsHaltIn_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) : (satGuessVerifyNTM M).AllPathsHaltIn (satGuessVerifyTime f)

All computation paths of the SAT-specialized machine halt within the uniform bound induced by the setup budget and the verifier time window.

theorem Complexity.SAT.satGuessVerify_trace_decides_for_some_setup_witness_of_decidesInTime {k : ℕ} (M : TM k) {L : Language} {f : ℕ → ℕ} (hM : M.DecidesInTime L f) (x : List Bool) (choices : Fin (satGuessVerifyTime f x.length) → Bool) : ∃ (y : List Bool), y.length ≤ x.length + 1 ∧ have cFinal := (satGuessVerifyNTM M).trace (satGuessVerifyTime f x.length) choices ((satGuessVerifyNTM M).initCfg x); (satGuessVerifyNTM M).halted cFinal ∧ (pair x y ∈ L → cFinal.output.cells 1 = Γ.one) ∧ (pair x y ∉ L → cFinal.output.cells 1 = Γ.zero)

Every full SAT-specialized run within the uniform bound factors through some bounded guessed witness y, and the final output bit matches the verifier's decision on pair x y.

theorem Complexity.SAT.satGuessVerify_not_acceptsInTime_of_not_mem_LSAT_of_decidesInTime {k : ℕ} (M : TM k) {f : ℕ → ℕ} (hM : M.DecidesInTime (pairLang Witness) f) (x : List Bool) (hx : x ∉ language) : ¬(satGuessVerifyNTM M).AcceptsInTime x (satGuessVerifyTime f x.length)

No SAT instance outside language has an accepting run within the uniform SAT-specialized bound, assuming the verifier decides pairLang Witness.

theorem Complexity.SAT.satGuessVerify_decidesInTime_of_decidesInTime {k : ℕ} (M : TM k) {f : ℕ → ℕ} (hM : M.DecidesInTime (pairLang Witness) f) : (satGuessVerifyNTM M).DecidesInTime language (satGuessVerifyTime f)

The SAT-specialized machine decides language within the uniform bound satGuessVerifyTime, assuming M decides the SAT verifier pair language.

theorem Complexity.SAT.satGuessVerifyTime_polynomial_bound {f : ℕ → ℕ} {c : ℕ} (hfO : BigO f fun (x : ℕ) => x ^ c) : ∃ (q : Polynomial ℕ), ∀ (n : ℕ), satGuessVerifyTime f n ≤ Polynomial.eval n q

If the verifier time bound is polynomial, then the SAT-specialized witness-independent runtime satGuessVerifyTime is pointwise bounded by an explicit polynomial.

theorem Complexity.SAT.satGuessVerifyTime_bigO_of_bigO {f : ℕ → ℕ} {c : ℕ} (hfO : BigO f fun (x : ℕ) => x ^ c) : ∃ (d : ℕ), BigO (satGuessVerifyTime f) fun (x : ℕ) => x ^ d

If the verifier time bound is polynomial, then the SAT-specialized runtime satGuessVerifyTime is polynomial too.

theorem Complexity.SAT.language_mem_NP_of_verifierP_direct (h : pairLang Witness ∈ P) : language ∈ NP

Direct SAT route: if the deterministic verifier for Witness is in P, then the completed SAT-specialized guess-and-verify machine puts language in NP. This bypasses the still-open generic witness-language interface and packages the concrete construction proved in this file.

theorem Complexity.SAT.satGuessVerify_counter_done_trace_one {k : ℕ} (M : TM k) (choice : Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) { state := GuessVerifyPhase.counter TM.LinearCounterPhase.done, input := inp, work := work, output := out } = satRewindInputWrap M { state := TM.RewindPhase.moveLeft, input := satBoundaryInput inp, work := satBoundaryWork work, output := satBoundaryOutput out }

The full boundary step from counter setup into input rewind.

theorem Complexity.SAT.satGuessVerify_rewind_done_trace_one {k : ℕ} (M : TM k) (choice : Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) { state := GuessVerifyPhase.rewindInput TM.RewindPhase.done, input := inp, work := work, output := out } = satGuessWrap M { state := NTM.GuessBoundedPhase.choose, input := satBoundaryInput inp, work := satBoundaryWork work, output := satBoundaryOutput out }

The full boundary step from input rewind into bounded guessing.

theorem Complexity.SAT.satGuessVerify_guess_done_trace_one {k : ℕ} (M : TM k) (choice : Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) { state := GuessVerifyPhase.guess NTM.GuessBoundedPhase.done, input := inp, work := work, output := out } = satPairWrap M { state := TM.PairBuildPhase.init, input := satBoundaryInput inp, work := satBoundaryWork work, output := satBoundaryOutput out }

The full boundary step from bounded guessing into pair building.

theorem Complexity.SAT.satGuessVerify_pair_done_trace_one {k : ℕ} (M : TM k) (choice : Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) : (satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) { state := GuessVerifyPhase.pair TM.PairBuildPhase.done, input := inp, work := work, output := out } = satVerifyWrap M { state := verifierStartedState M, input := satBoundaryInput inp, work := satBoundaryWork work, output := satBoundaryOutput out }

The full boundary step from pair building into verifier simulation.

theorem Complexity.SAT.satGuessVerify_counter_done_trace_one_state {k : ℕ} (M : TM k) (choice : Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) : ((satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) { state := GuessVerifyPhase.counter TM.LinearCounterPhase.done, input := inp, work := work, output := out }).state = GuessVerifyPhase.rewindInput TM.RewindPhase.moveLeft

State-only form of the boundary step from a finished counter phase into input rewinding.

theorem Complexity.SAT.satGuessVerify_rewind_done_trace_one_state {k : ℕ} (M : TM k) (choice : Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) : ((satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) { state := GuessVerifyPhase.rewindInput TM.RewindPhase.done, input := inp, work := work, output := out }).state = GuessVerifyPhase.guess NTM.GuessBoundedPhase.choose

State-only form of the boundary step from a finished rewind phase into bounded guessing.

theorem Complexity.SAT.satGuessVerify_guess_done_trace_one_state {k : ℕ} (M : TM k) (choice : Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) : ((satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) { state := GuessVerifyPhase.guess NTM.GuessBoundedPhase.done, input := inp, work := work, output := out }).state = GuessVerifyPhase.pair TM.PairBuildPhase.init

State-only form of the boundary step from a finished guess phase into pair building.

theorem Complexity.SAT.satGuessVerify_pair_done_trace_one_state {k : ℕ} (M : TM k) (choice : Bool) (inp : Tape) (work : Fin (k + 3) → Tape) (out : Tape) : ((satGuessVerifyNTM M).trace 1 (fun (x : Fin 1) => choice) { state := GuessVerifyPhase.pair TM.PairBuildPhase.done, input := inp, work := work, output := out }).state = GuessVerifyPhase.verify (verifierStartedState M)