Assembling a machine that guesses

Complexitylib.Models.TuringMachine.GuessStream reduces building a nondeterministic machine to building a deterministic one that satisfies TM.GuessProtocol on its last work tape. This file supplies the parts.

TM.liftLast puts an ordinary machine to work on the first tapes and leaves the guess tape untouched, so every existing subroutine can be used verbatim. TM.GuessProtocol is then closed under TM.seqTM and TM.loopTM, which is what lets the guessing and the not-guessing be assembled into one machine: all three of its conditions are pointwise properties of the transition function, and the combinators' own steps preserve every tape they are not driving.

Main definitions

• TM.liftLast — run a machine on the first work tapes, holding the last one still
• TM.guessReadTM — copy the guess cell onto a work tape and advance the guess head
• TM.guessWriteTM — the same, advancing the target head too, so a block of guesses can be written
• TM.guessBlockTM — a fixed number of those in sequence
• TM.guessBlocksTM — and a block written into each of several registers
• TM.guessThenTM — guess some blocks, then run a guess-free machine on them
• TM.guessStageTM — and the stage every construction is built from: guess, then rewind the guessed registers so a scan can read them
• TM.guessWriteTapes, TM.guessBlockTapes — the tapes one guess-write, and a block of them, leave behind

Main results

• TM.guessProtocol_liftLast — a lifted machine never consults the guess tape
• TM.liftLast_reachesIn — and its runs are the original's
• TM.lift4, TM.lift4_hoareTime — the same, four tapes at a time
• TM.guessProtocol_seqTM, TM.guessProtocol_loopTM — the protocol survives composition
• TM.guessProtocol_guessReadTM, TM.guessReadTM_stepCfg, TM.guessProtocol_guessWriteTM, TM.guessWriteTM_stepCfg — what the primitives do
• TM.guessProtocol_guessBlockTM, TM.guessProtocol_guessBlocksTM, TM.guessProtocol_guessThenTM — and these respect the protocol
• TM.skipTM_hoareTime', TM.guessBlocksTM_hoareTime, TM.guessThenTM_hoareTime — and their contracts
• TM.guessWriteTM_hoareTime, TM.guessBlockTM_hoareTime — their contracts
• TM.guessWriteTapes_last, TM.guessWriteTapes_target, TM.guessWriteTapes_other — what one guess-write does to each tape, off the left marker
• TM.guessWriteTapes_target_head, TM.guessWriteTapes_target_cells, TM.guessWriteTapes_target_cells_ne — where the guessed bit lands
• TM.guessWriteTapes_startInvariant, TM.guessWriteTapes_head_pos — and that the invariants survive it
• TM.GuessFrom, TM.guessFrom_after — what the guess tape still holds, and that a stage consumes a prefix and leaves the rest
• TM.guessBlocksTapes_spec — what several blocks leave behind, when the registers are distinct
• TM.guessList, TM.guessList_getElem — the guess stream that realizes a family of blocks
• TM.StageBlocks, TM.exists_stageBlocks, TM.blocks_of_stageBlocks — and one that feeds every stage of a loop, with each stage reading its own blocks off it
• TM.guessBlockTapes_spec — what a whole block leaves behind: both heads advanced by the number of bits, those bits on the target, nothing else touched

Lifting a machine past the guess tape

def Complexity.TM.liftLast {m : ℕ} (D : TM m) : TM (m + 1)

Run D on the first m work tapes, writing the last one back unchanged and holding its head still.

Equations

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

@[simp]

theorem Complexity.TM.liftLast_qhalt {m : ℕ} (D : TM m) : D.liftLast.qhalt = D.qhalt

@[simp]

theorem Complexity.TM.liftLast_qstart {m : ℕ} (D : TM m) : D.liftLast.qstart = D.qstart

theorem Complexity.TM.guessProtocol_liftLast {m : ℕ} (D : TM m) : D.liftLast.GuessProtocol fun (x : D.liftLast.Q) => false

A lifted machine never consults the guess tape, so it advances nowhere.

theorem Complexity.TM.liftLast_stepCfg {m : ℕ} (D : TM m) (c : Cfg m D.Q) (τ : Tape) (hτ : τ.read ≠ Γ.start) : D.liftLast.stepCfg (NTM.attach c τ) = NTM.attach (D.stepCfg c) τ

One step of a lifted machine is one step of the original, with the guess tape untouched.

theorem Complexity.TM.liftLast_reachesIn {m : ℕ} (D : TM m) (τ : Tape) (hτ : τ.read ≠ Γ.start) (t : ℕ) {c c' : Cfg m D.Q} : D.reachesIn t c c' → D.liftLast.reachesIn t (NTM.attach c τ) (NTM.attach c' τ)

A run of a lifted machine is a run of the original.

theorem Complexity.TM.liftLast_initCfg {m : ℕ} (D : TM m) (inp out : Tape) (work : Fin (m + 1) → Tape) : { state := D.liftLast.qstart, input := inp, work := work, output := out } = NTM.attach { state := D.qstart, input := inp, work := fun (i : Fin m) => work i.castSucc, output := out } (work (Fin.last m))

The starting configuration of a lifted machine is the original's with the guess tape attached.

theorem Complexity.TM.liftLast_hoareTime {m : ℕ} (D : TM m) {pre post : TapePred m} {bound : ℕ} (h : D.HoareTime pre post bound) (τ : Tape) (hτ : τ.read ≠ Γ.start) : D.liftLast.HoareTime (fun (inp : Tape) (work : Fin (m + 1) → Tape) (out : Tape) => work (Fin.last m) = τ ∧ pre inp (fun (i : Fin m) => work i.castSucc) out) (fun (inp : Tape) (work : Fin (m + 1) → Tape) (out : Tape) => work (Fin.last m) = τ ∧ post inp (fun (i : Fin m) => work i.castSucc) out) bound

A Hoare triple for a lifted machine. Everything the original guarantees still holds, and the guess tape comes out exactly as it went in.

def Complexity.TM.lift4 {m : ℕ} (D : TM m) : TM (m + 4)

Lift a machine past four fresh tapes, holding them still. Four at a time because a check's block is four tapes wide.

Equations

• D.lift4 = D.liftLast.liftLast.liftLast.liftLast

theorem Complexity.TM.guessProtocol_lift4 {m : ℕ} (D : TM m) : D.lift4.GuessProtocol fun (x : D.lift4.Q) => false

A lifted-by-four machine never consults the last tape.

theorem Complexity.TM.lift4_hoareTime {m : ℕ} (D : TM m) {pre post : TapePred m} {b : ℕ} (h : D.HoareTime pre post b) (τ₁ τ₂ τ₃ τ₄ : Tape) (h₁ : τ₁.read ≠ Γ.start) (h₂ : τ₂.read ≠ Γ.start) (h₃ : τ₃.read ≠ Γ.start) (h₄ : τ₄.read ≠ Γ.start) : D.lift4.HoareTime (fun (inp : Tape) (work : Fin (m + 4) → Tape) (out : Tape) => work (Fin.last (m + 3)) = τ₄ ∧ (fun (i : Fin (m + 2 + 1)) => work i.castSucc) (Fin.last (m + 2)) = τ₃ ∧ (fun (i : Fin (m + 1 + 1)) => work i.castSucc.castSucc) (Fin.last (m + 1)) = τ₂ ∧ (fun (i : Fin (m + 1)) => work i.castSucc.castSucc.castSucc) (Fin.last m) = τ₁ ∧ pre inp (fun (i : Fin m) => work i.castSucc.castSucc.castSucc.castSucc) out) (fun (inp : Tape) (work : Fin (m + 4) → Tape) (out : Tape) => work (Fin.last (m + 3)) = τ₄ ∧ (fun (i : Fin (m + 2 + 1)) => work i.castSucc) (Fin.last (m + 2)) = τ₃ ∧ (fun (i : Fin (m + 1 + 1)) => work i.castSucc.castSucc) (Fin.last (m + 1)) = τ₂ ∧ (fun (i : Fin (m + 1)) => work i.castSucc.castSucc.castSucc) (Fin.last m) = τ₁ ∧ post inp (fun (i : Fin m) => work i.castSucc.castSucc.castSucc.castSucc) out) b

A lifted-by-four machine's contract. Four fresh tapes come through untouched.

def Complexity.TM.liftMany {m : ℕ} (D : TM m) (r : ℕ) : TM (m + r)

Lift a machine past r fresh tapes, holding them still. The original tapes keep their indices — Fin.castAdd r — and the fresh ones are appended.

TM.liftTM in Models/TuringMachine/Lift.lean widens a machine the same way, but its interface carries blank extra tapes, for lifting whole decision procedures. This one is the iterated liftLast, so its Hoare rule below carries arbitrary extra tapes through untouched — what an assembled subroutine needs.

Equations

• D.liftMany 0 = D
• D.liftMany r.succ = (D.liftMany r).liftLast

theorem Complexity.TM.liftMany_hoareTime {m : ℕ} (D : TM m) {pre post : TapePred m} {b : ℕ} (h : D.HoareTime pre post b) (r : ℕ) (τ : Fin r → Tape) : (∀ (i : Fin r), (τ i).read ≠ Γ.start) → (D.liftMany r).HoareTime (fun (inp : Tape) (work : Fin (m + r) → Tape) (out : Tape) => (∀ (i : Fin r), work (Fin.natAdd m i) = τ i) ∧ pre inp (fun (i : Fin m) => work (Fin.castAdd r i)) out) (fun (inp : Tape) (work : Fin (m + r) → Tape) (out : Tape) => (∀ (i : Fin r), work (Fin.natAdd m i) = τ i) ∧ post inp (fun (i : Fin m) => work (Fin.castAdd r i)) out) b

A padded machine's contract. The r fresh tapes come through untouched, and the original tapes keep their meaning under Fin.castAdd.

theorem Complexity.TM.IsTransducer.liftLast {m : ℕ} {D : TM m} (h : D.IsTransducer) : D.liftLast.IsTransducer

A lifted machine keeps the one-way-output discipline.

theorem Complexity.TM.IsTransducer.liftMany {m : ℕ} {D : TM m} (h : D.IsTransducer) (r : ℕ) : (D.liftMany r).IsTransducer

A padded machine keeps the one-way-output discipline.

The protocol survives composition

def Complexity.TM.seqAdv {k : ℕ} {A B : TM (k + 1)} (AdvA : A.Q → Bool) (AdvB : B.Q → Bool) : SeqQ A.Q B.Q → Bool

The advancing states of a sequential composition: each part's own, with the handoff step — which the combinator takes in A's halt state — excluded.

Equations

• Complexity.TM.seqAdv AdvA AdvB = Sum.elim (fun (q : A.Q) => AdvA q && !decide (q = A.qhalt)) AdvB

theorem Complexity.TM.guessProtocol_seqTM {k : ℕ} {A B : TM (k + 1)} {AdvA : A.Q → Bool} {AdvB : B.Q → Bool} (hA : A.GuessProtocol AdvA) (hB : B.GuessProtocol AdvB) : (A.seqTM B).GuessProtocol (seqAdv AdvA AdvB)

The guess protocol survives sequential composition.

def Complexity.TM.loopAdv {k : ℕ} {Body Test : TM (k + 1)} (AdvB : Body.Q → Bool) (AdvT : Test.Q → Bool) : LoopQ Body.Q Test.Q → Bool

The advancing states of a loop: each part's own, with the combinator's own control phases and handoff steps excluded.

Equations

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

theorem Complexity.TM.guessProtocol_loopTM {k : ℕ} {Body Test : TM (k + 1)} {AdvB : Body.Q → Bool} {AdvT : Test.Q → Bool} (hB : Body.GuessProtocol AdvB) (hT : Test.GuessProtocol AdvT) : (Body.loopTM Test).GuessProtocol (loopAdv AdvB AdvT)

The guess protocol survives looping.

Reading a guess

inductive Complexity.TM.GuessPhase : Type

Control states of TM.guessReadTM.

• read : GuessPhase

  Copy the guess cell onto the target tape.

• done : GuessPhase

  Halt.

@[instance_reducible]

instance Complexity.TM.instDecidableEqGuessPhase : DecidableEq GuessPhase

Equations

• Complexity.TM.instDecidableEqGuessPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complexity.TM.instFintypeGuessPhase : Fintype GuessPhase

Equations

• Complexity.TM.instFintypeGuessPhase = { elems := {Complexity.TM.GuessPhase.read, Complexity.TM.GuessPhase.done}, complete := ⋯ }

def Complexity.TM.guessPhaseAdv (q : GuessPhase) : Bool

The advancing state of the guess primitives: only read consumes a guess bit. Stated on GuessPhase itself so instance search never has to see through a machine's Q projection.

Equations

• Complexity.TM.guessPhaseAdv q = decide (q = Complexity.TM.GuessPhase.read)

def Complexity.TM.guessReadTM {k : ℕ} (j : Fin (k + 1)) : TM (k + 1)

The guess-reading primitive. In one step it copies the symbol under the guess head onto work tape j, advances the guess head, and halts. This is the only place a machine assembled with TM.liftLast ever consults the guess tape.

Equations

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

@[simp]

theorem Complexity.TM.guessReadTM_qhalt {k : ℕ} (j : Fin (k + 1)) : (guessReadTM j).qhalt = GuessPhase.done

@[simp]

theorem Complexity.TM.guessReadTM_qstart {k : ℕ} (j : Fin (k + 1)) : (guessReadTM j).qstart = GuessPhase.read

theorem Complexity.TM.guessProtocol_guessReadTM {k : ℕ} (j : Fin (k + 1)) : (guessReadTM j).GuessProtocol guessPhaseAdv

The guess-reading primitive advances exactly in its one working state.

theorem Complexity.TM.guessReadTM_stepCfg {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (c : Cfg (k + 1) (guessReadTM j).Q) (hstate : c.state = GuessPhase.read) : ((guessReadTM j).stepCfg c).state = GuessPhase.done ∧ ((guessReadTM j).stepCfg c).work j = (c.work j).writeAndMove (readBackWrite (c.work (Fin.last k)).read).toΓ (idleDir (c.work j).read) ∧ ((guessReadTM j).stepCfg c).work (Fin.last k) = (c.work (Fin.last k)).writeAndMove (readBackWrite (c.work (Fin.last k)).read).toΓ Dir3.right ∧ ∀ (i : Fin (k + 1)), i ≠ j → i ≠ Fin.last k → ((guessReadTM j).stepCfg c).work i = (c.work i).writeAndMove (readBackWrite (c.work i).read).toΓ (idleDir (c.work i).read)

One step of the guess-reading primitive: the guess symbol lands on tape j, the guess head advances, and every other tape is left where it was.

def Complexity.TM.guessWriteTM {k : ℕ} (j : Fin (k + 1)) : TM (k + 1)

The guess-writing primitive. Like TM.guessReadTM, but it also advances the target head, so that repeating it writes a block of guessed bits.

Equations

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

@[simp]

theorem Complexity.TM.guessWriteTM_qhalt {k : ℕ} (j : Fin (k + 1)) : (guessWriteTM j).qhalt = GuessPhase.done

@[simp]

theorem Complexity.TM.guessWriteTM_qstart {k : ℕ} (j : Fin (k + 1)) : (guessWriteTM j).qstart = GuessPhase.read

theorem Complexity.TM.guessProtocol_guessWriteTM {k : ℕ} (j : Fin (k + 1)) : (guessWriteTM j).GuessProtocol guessPhaseAdv

The guess-writing primitive advances exactly in its one working state.

theorem Complexity.TM.guessWriteTM_stepCfg {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (c : Cfg (k + 1) (guessWriteTM j).Q) (hstate : c.state = GuessPhase.read) : ((guessWriteTM j).stepCfg c).state = GuessPhase.done ∧ ((guessWriteTM j).stepCfg c).work j = (c.work j).writeAndMove (readBackWrite (c.work (Fin.last k)).read).toΓ Dir3.right ∧ ((guessWriteTM j).stepCfg c).work (Fin.last k) = (c.work (Fin.last k)).writeAndMove (readBackWrite (c.work (Fin.last k)).read).toΓ Dir3.right ∧ ∀ (i : Fin (k + 1)), i ≠ j → i ≠ Fin.last k → ((guessWriteTM j).stepCfg c).work i = (c.work i).writeAndMove (readBackWrite (c.work i).read).toΓ (idleDir (c.work i).read)

One step of the guess-writing primitive: the guess symbol lands on tape j, which then advances, the guess head advances, and every other tape is left where it was.

def Complexity.TM.guessWriteTapes {k : ℕ} (j : Fin (k + 1)) (W : Fin (k + 1) → Tape) : Fin (k + 1) → Tape

The tapes after one guess-write: the target takes the guessed symbol and advances, the guess tape advances, and every other tape passes through the phase transition unchanged.

Equations

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

theorem Complexity.TM.guessWriteTM_hoareTime {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (inp₀ out₀ : Tape) (W₀ : Fin (k + 1) → Tape) : (guessWriteTM j).HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = W₀) (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = transitionInput inp₀ ∧ out = transitionTape out₀ ∧ work = guessWriteTapes j W₀) 1

The contract of one guess-write.

Writing a block of guesses

A parameter block is a fixed number of bits — fixed because it holds a state, a choice bit and one symbol per head, none of which grows with the input — so the machine that writes it can be built by recursion on that number rather than by a counted loop.

def Complexity.TM.guessBlockTM {k : ℕ} (j : Fin (k + 1)) : ℕ → TM (k + 1)

Write n + 1 guessed bits onto work tape j, advancing it.

Equations

• Complexity.TM.guessBlockTM j 0 = Complexity.TM.guessWriteTM j
• Complexity.TM.guessBlockTM j r.succ = (Complexity.TM.guessWriteTM j).seqTM (Complexity.TM.guessBlockTM j r)

def Complexity.TM.guessBlockAdv {k : ℕ} (j : Fin (k + 1)) (n : ℕ) : (guessBlockTM j n).Q → Bool

Its advancing states: every state of every stage.

Equations

• Complexity.TM.guessBlockAdv j 0 = Complexity.TM.guessPhaseAdv
• Complexity.TM.guessBlockAdv j r.succ = Complexity.TM.seqAdv Complexity.TM.guessPhaseAdv (Complexity.TM.guessBlockAdv j r)

def Complexity.TM.guessBlockTapes {k : ℕ} (j : Fin (k + 1)) : ℕ → (Fin (k + 1) → Tape) → Fin (k + 1) → Tape

The tapes a block of guess-writes leaves behind. Each stage writes, then the composition's own handoff step passes every tape through TM.transitionTape.

Equations

• Complexity.TM.guessBlockTapes j 0 x✝ = Complexity.TM.guessWriteTapes j x✝
• Complexity.TM.guessBlockTapes j n.succ x✝ = Complexity.TM.guessBlockTapes j n fun (i : Fin (k + 1)) => Complexity.TM.transitionTape (Complexity.TM.guessWriteTapes j x✝ i)

def Complexity.TM.guessBlockInput : ℕ → Tape → Tape

The input tape a block of guess-writes leaves behind.

Equations

• Complexity.TM.guessBlockInput 0 x✝ = Complexity.TM.transitionInput x✝
• Complexity.TM.guessBlockInput n.succ x✝ = Complexity.TM.guessBlockInput n (Complexity.TM.transitionInput (Complexity.TM.transitionInput x✝))

def Complexity.TM.guessBlockOutput : ℕ → Tape → Tape

The output tape a block of guess-writes leaves behind.

Equations

• Complexity.TM.guessBlockOutput 0 x✝ = Complexity.TM.transitionTape x✝
• Complexity.TM.guessBlockOutput n.succ x✝ = Complexity.TM.guessBlockOutput n (Complexity.TM.transitionTape (Complexity.TM.transitionTape x✝))

theorem Complexity.TM.guessBlockTM_hoareTime {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (n : ℕ) (inp₀ out₀ : Tape) (W₀ : Fin (k + 1) → Tape) : (guessBlockTM j n).HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = W₀) (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = guessBlockInput n inp₀ ∧ out = guessBlockOutput n out₀ ∧ work = guessBlockTapes j n W₀) (2 * n + 1)

The contract of a block of guess-writes.

What a block of guesses actually leaves behind

On tapes whose heads are off the left marker — which is how every stage of an assembled machine runs — the phase transitions are the identity, and the description collapses.

theorem Complexity.TM.guessBlockInput_eq_self {t : Tape} (h : t.read ≠ Γ.start) (n : ℕ) : guessBlockInput n t = t

theorem Complexity.TM.guessBlockOutput_eq_self {t : Tape} (h : t.read ≠ Γ.start) (n : ℕ) : guessBlockOutput n t = t

theorem Complexity.TM.guessWriteTapes_last {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (W : Fin (k + 1) → Tape) (hg : (W (Fin.last k)).read ≠ Γ.start) : guessWriteTapes j W (Fin.last k) = (W (Fin.last k)).move Dir3.right

theorem Complexity.TM.guessWriteTapes_target {k : ℕ} (j : Fin (k + 1)) (W : Fin (k + 1) → Tape) (hg : (W (Fin.last k)).read ≠ Γ.start) : guessWriteTapes j W j = ((W j).write (W (Fin.last k)).read).move Dir3.right

theorem Complexity.TM.guessWriteTapes_other {k : ℕ} (j : Fin (k + 1)) (W : Fin (k + 1) → Tape) (i : Fin (k + 1)) (hij : i ≠ j) (hil : i ≠ Fin.last k) (h : (W i).read ≠ Γ.start) : guessWriteTapes j W i = W i

theorem Complexity.TM.guessWriteTapes_target_head {k : ℕ} (j : Fin (k + 1)) (W : Fin (k + 1) → Tape) (hg : (W (Fin.last k)).read ≠ Γ.start) : (guessWriteTapes j W j).head = (W j).head + 1

theorem Complexity.TM.guessWriteTapes_target_cells {k : ℕ} (j : Fin (k + 1)) (W : Fin (k + 1) → Tape) (hg : (W (Fin.last k)).read ≠ Γ.start) (hh : 1 ≤ (W j).head) : (guessWriteTapes j W j).cells (W j).head = (W (Fin.last k)).read

theorem Complexity.TM.guessWriteTapes_target_cells_ne {k : ℕ} (j : Fin (k + 1)) (W : Fin (k + 1) → Tape) (hg : (W (Fin.last k)).read ≠ Γ.start) {q : ℕ} (hq : q ≠ (W j).head) : (guessWriteTapes j W j).cells q = (W j).cells q

theorem Complexity.TM.guessWriteTapes_startInvariant {k : ℕ} (j : Fin (k + 1)) (W : Fin (k + 1) → Tape) (hinv : ∀ (i : Fin (k + 1)), (W i).StartInvariant) (hh : ∀ (i : Fin (k + 1)), 1 ≤ (W i).head) (i : Fin (k + 1)) : (guessWriteTapes j W i).StartInvariant

theorem Complexity.TM.guessWriteTapes_head_pos {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (W : Fin (k + 1) → Tape) (hinv : ∀ (i : Fin (k + 1)), (W i).StartInvariant) (hh : ∀ (i : Fin (k + 1)), 1 ≤ (W i).head) (i : Fin (k + 1)) : 1 ≤ (guessWriteTapes j W i).head

theorem Complexity.TM.guessBlockTapes_startInvariant {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (n : ℕ) (W : Fin (k + 1) → Tape) : (∀ (i : Fin (k + 1)), (W i).StartInvariant) → (∀ (i : Fin (k + 1)), 1 ≤ (W i).head) → ∀ (i : Fin (k + 1)), (guessBlockTapes j n W i).StartInvariant

A block of guess-writes preserves the left-marker invariant.

theorem Complexity.TM.guessBlockTapes_spec {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (n : ℕ) (W : Fin (k + 1) → Tape) : (∀ (i : Fin (k + 1)), (W i).StartInvariant) → (∀ (i : Fin (k + 1)), 1 ≤ (W i).head) → guessBlockTapes j n W (Fin.last k) = { head := (W (Fin.last k)).head + (n + 1), cells := (W (Fin.last k)).cells } ∧ (guessBlockTapes j n W j).head = (W j).head + (n + 1) ∧ (∀ (i : Fin (k + 1)), i ≠ j → i ≠ Fin.last k → guessBlockTapes j n W i = W i) ∧ (∀ q < (W j).head, (guessBlockTapes j n W j).cells q = (W j).cells q) ∧ ∀ p ≤ n, (guessBlockTapes j n W j).cells ((W j).head + p) = (W (Fin.last k)).cells ((W (Fin.last k)).head + p)

What a block of guess-writes leaves behind. The guess tape and the target have both advanced by the number of bits written, the target's cells hold those bits, its earlier cells and every other tape are untouched.

theorem Complexity.TM.guessProtocol_guessBlockTM {k : ℕ} (j : Fin (k + 1)) (n : ℕ) : (guessBlockTM j n).GuessProtocol (guessBlockAdv j n)

A block of guesses respects the protocol.

Several blocks of guesses

A configuration is spread over several registers, so guessing one means writing a block into each. The registers are addressed by index, so no placement is involved.

theorem Complexity.TM.guessProtocol_skipTM {k : ℕ} : skipTM.GuessProtocol fun (x : skipTM.Q) => false

The do-nothing machine never consults the guess tape.

theorem Complexity.TM.skipTM_hoareTime' {k : ℕ} (inp₀ out₀ : Tape) (W₀ : Fin (k + 1) → Tape) : skipTM.HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = W₀) (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = transitionInput inp₀ ∧ out = transitionTape out₀ ∧ work = fun (i : Fin (k + 1)) => transitionTape (W₀ i)) 1

The do-nothing machine's contract, in the pinned form the guess stages use: one step, and every tape passes through the phase transition.

theorem Complexity.TM.guessBlockTapes_head_pos {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (n : ℕ) (W : Fin (k + 1) → Tape) (hinv : ∀ (i : Fin (k + 1)), (W i).StartInvariant) (hh : ∀ (i : Fin (k + 1)), 1 ≤ (W i).head) (i : Fin (k + 1)) : 1 ≤ (guessBlockTapes j n W i).head

A block of guess-writes leaves every head off the left marker.

def Complexity.TM.guessOffset (w : ℕ → ℕ) : ℕ → ℕ

Where block p's guesses sit on the guess tape: each block consumes one cell per bit plus one for the block's final advance.

Equations

• Complexity.TM.guessOffset w 0 = 0
• Complexity.TM.guessOffset w r.succ = Complexity.TM.guessOffset w r + (w r + 1)

theorem Complexity.TM.guessOffset_le (w : ℕ → ℕ) {p t : ℕ} : p ≤ t → guessOffset w p ≤ guessOffset w t

Offsets grow with the number of blocks.

def Complexity.TM.guessList (w : ℕ → ℕ) (b : ℕ → ℕ → Bool) : ℕ → List Bool

The bits of a family of blocks, laid end to end: this is the guess stream that makes each register of TM.guessBlocksTM hold what the caller wants it to hold.

Equations

• Complexity.TM.guessList w b 0 = []
• Complexity.TM.guessList w b r.succ = Complexity.TM.guessList w b r ++ List.ofFn fun (q : Fin (w r + 1)) => b r ↑q

@[simp]

theorem Complexity.TM.guessList_length (w : ℕ → ℕ) (b : ℕ → ℕ → Bool) (t : ℕ) : (guessList w b t).length = guessOffset w t

theorem Complexity.TM.guessList_getElem (w : ℕ → ℕ) (b : ℕ → ℕ → Bool) (t p q : ℕ) : p < t → q ≤ w p → (guessList w b t)[guessOffset w p + q]? = some (b p q)

Block p's bits sit at offset guessOffset w p.

def Complexity.TM.guessBlocksTM {k : ℕ} (j : ℕ → Fin (k + 1)) (w : ℕ → ℕ) : ℕ → TM (k + 1)

Write a block of guesses into each of t registers in turn.

Equations

• Complexity.TM.guessBlocksTM j w 0 = Complexity.TM.skipTM
• Complexity.TM.guessBlocksTM j w r.succ = (Complexity.TM.guessBlocksTM j w r).seqTM (Complexity.TM.guessBlockTM (j r) (w r))

def Complexity.TM.guessBlocksAdv {k : ℕ} (j : ℕ → Fin (k + 1)) (w : ℕ → ℕ) (t : ℕ) : (guessBlocksTM j w t).Q → Bool

Its advancing states.

Equations

• Complexity.TM.guessBlocksAdv j w 0 = fun (x : (Complexity.TM.guessBlocksTM j w 0).Q) => false
• Complexity.TM.guessBlocksAdv j w r.succ = Complexity.TM.seqAdv (Complexity.TM.guessBlocksAdv j w r) (Complexity.TM.guessBlockAdv (j r) (w r))

def Complexity.TM.guessBlocksTapes {k : ℕ} (j : ℕ → Fin (k + 1)) (w : ℕ → ℕ) : ℕ → (Fin (k + 1) → Tape) → Fin (k + 1) → Tape

The tapes several blocks of guesses leave behind.

Equations

• Complexity.TM.guessBlocksTapes j w 0 x✝ = fun (i : Fin (k + 1)) => Complexity.TM.transitionTape (x✝ i)
• Complexity.TM.guessBlocksTapes j w n.succ x✝ = Complexity.TM.guessBlockTapes (j n) (w n) fun (i : Fin (k + 1)) => Complexity.TM.transitionTape (Complexity.TM.guessBlocksTapes j w n x✝ i)

theorem Complexity.TM.guessBlockTapes_beyond {k : ℕ} (j : Fin (k + 1)) (hj : j ≠ Fin.last k) (n : ℕ) (W : Fin (k + 1) → Tape) : (∀ (i : Fin (k + 1)), (W i).StartInvariant) → (∀ (i : Fin (k + 1)), 1 ≤ (W i).head) → ∀ (q : ℕ), (W j).head + n < q → (guessBlockTapes j n W j).cells q = (W j).cells q

A guessed block leaves the tape beyond it untouched. The blank that stops a scan belongs to the tape, not to the guess, so it has to survive the guess.

theorem Complexity.TM.guessBlocksTapes_spec {k : ℕ} (j : ℕ → Fin (k + 1)) (hj : ∀ (p : ℕ), j p ≠ Fin.last k) (w : ℕ → ℕ) (t : ℕ) (W : Fin (k + 1) → Tape) : (∀ (i : Fin (k + 1)), (W i).StartInvariant) → (∀ (i : Fin (k + 1)), 1 ≤ (W i).head) → (∀ (p q : ℕ), p < t → q < t → j p = j q → p = q) → (∀ (i : Fin (k + 1)), (guessBlocksTapes j w t W i).StartInvariant) ∧ (∀ (i : Fin (k + 1)), 1 ≤ (guessBlocksTapes j w t W i).head) ∧ guessBlocksTapes j w t W (Fin.last k) = { head := (W (Fin.last k)).head + guessOffset w t, cells := (W (Fin.last k)).cells } ∧ (∀ (i : Fin (k + 1)), i ≠ Fin.last k → (∀ p < t, i ≠ j p) → guessBlocksTapes j w t W i = W i) ∧ ∀ p < t, (guessBlocksTapes j w t W (j p)).head = (W (j p)).head + (w p + 1) ∧ ∀ q ≤ w p, (guessBlocksTapes j w t W (j p)).cells ((W (j p)).head + q) = (W (Fin.last k)).cells ((W (Fin.last k)).head + guessOffset w p + q)

What several blocks of guesses leave behind. When the target registers are distinct, each one ends up holding its own block of guessed bits, read off the guess tape at that block's offset — which is what lets a stage guess a whole structured object at once.

theorem Complexity.TM.guessBlocksTapes_beyond {k : ℕ} (j : ℕ → Fin (k + 1)) (hj : ∀ (p : ℕ), j p ≠ Fin.last k) (w : ℕ → ℕ) (t : ℕ) (W : Fin (k + 1) → Tape) : (∀ (i : Fin (k + 1)), (W i).StartInvariant) → (∀ (i : Fin (k + 1)), 1 ≤ (W i).head) → (∀ (p q : ℕ), p < t → q < t → j p = j q → p = q) → ∀ p < t, ∀ (q : ℕ), (W (j p)).head + w p < q → (guessBlocksTapes j w t W (j p)).cells q = (W (j p)).cells q

And so do several blocks. A register is written by at most one block, so beyond that block's own width its cells are the ones it started with.

def Complexity.TM.guessBlocksInput (w : ℕ → ℕ) : ℕ → Tape → Tape

The input tape they leave behind.

Equations

• Complexity.TM.guessBlocksInput w 0 x✝ = Complexity.TM.transitionInput x✝
• Complexity.TM.guessBlocksInput w n.succ x✝ = Complexity.TM.guessBlockInput (w n) (Complexity.TM.transitionInput (Complexity.TM.guessBlocksInput w n x✝))

def Complexity.TM.guessBlocksOutput (w : ℕ → ℕ) : ℕ → Tape → Tape

The output tape they leave behind.

Equations

• Complexity.TM.guessBlocksOutput w 0 x✝ = Complexity.TM.transitionTape x✝
• Complexity.TM.guessBlocksOutput w n.succ x✝ = Complexity.TM.guessBlockOutput (w n) (Complexity.TM.transitionTape (Complexity.TM.guessBlocksOutput w n x✝))

theorem Complexity.TM.guessBlocksInput_eq_self {t : Tape} (h : t.read ≠ Γ.start) (w : ℕ → ℕ) (s : ℕ) : guessBlocksInput w s t = t

Several blocks of guesses leave a parked input tape alone.

theorem Complexity.TM.guessBlocksOutput_eq_self {t : Tape} (h : t.read ≠ Γ.start) (w : ℕ → ℕ) (s : ℕ) : guessBlocksOutput w s t = t

Several blocks of guesses leave a parked output tape alone.

def Complexity.TM.guessBlocksTime (w : ℕ → ℕ) : ℕ → ℕ

How long several blocks of guesses take.

Equations

• Complexity.TM.guessBlocksTime w 0 = 1
• Complexity.TM.guessBlocksTime w r.succ = Complexity.TM.guessBlocksTime w r + 1 + (2 * w r + 1)

theorem Complexity.TM.guessBlocksTM_hoareTime {k : ℕ} (j : ℕ → Fin (k + 1)) (hj : ∀ (t : ℕ), j t ≠ Fin.last k) (w : ℕ → ℕ) (t : ℕ) (inp₀ out₀ : Tape) (W₀ : Fin (k + 1) → Tape) : (guessBlocksTM j w t).HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = W₀) (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = guessBlocksInput w t inp₀ ∧ out = guessBlocksOutput w t out₀ ∧ work = guessBlocksTapes j w t W₀) (guessBlocksTime w t)

The contract of several blocks of guesses.

theorem Complexity.TM.guessProtocol_guessBlocksTM {k : ℕ} (j : ℕ → Fin (k + 1)) (w : ℕ → ℕ) (t : ℕ) : (guessBlocksTM j w t).GuessProtocol (guessBlocksAdv j w t)

Several blocks of guesses respect the protocol.

def Complexity.TM.guessThenTM {k : ℕ} (j : ℕ → Fin (k + 1)) (w : ℕ → ℕ) (t : ℕ) (D : TM k) : TM (k + 1)

Guess, then check. Every stage of a guess-and-verify machine has this shape: write some blocks of guesses onto the registers, then run a guess-free machine on them.

Equations

• Complexity.TM.guessThenTM j w t D = (Complexity.TM.guessBlocksTM j w t).seqTM D.liftLast

theorem Complexity.TM.guessProtocol_guessThenTM {k : ℕ} (j : ℕ → Fin (k + 1)) (w : ℕ → ℕ) (t : ℕ) (D : TM k) : (guessThenTM j w t D).GuessProtocol (seqAdv (guessBlocksAdv j w t) fun (x : D.liftLast.Q) => false)

A guess-and-check stage respects the protocol.

theorem Complexity.TM.guessThenTM_hoareTime {k : ℕ} (j : ℕ → Fin (k + 1)) (hj : ∀ (t : ℕ), j t ≠ Fin.last k) (w : ℕ → ℕ) (t : ℕ) (D : TM k) {mid post : TapePred (k + 1)} {b : ℕ} (inp₀ out₀ : Tape) (W₀ : Fin (k + 1) → Tape) (h_trans : ∀ (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape), inp = guessBlocksInput w t inp₀ ∧ out = guessBlocksOutput w t out₀ ∧ work = guessBlocksTapes j w t W₀ → mid (transitionInput inp) (fun (i : Fin (k + 1)) => transitionTape (work i)) (transitionTape out)) (hD : D.liftLast.HoareTime mid post b) : (guessThenTM j w t D).HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = W₀) post (guessBlocksTime w t + 1 + b)

The contract of a guess-and-check stage. The caller says what the guessed tapes give the checking machine; this composes the two halves.

What the guess tape still holds

A stage consumes a prefix of the guess tape and leaves the rest for the stages after it. Stating that as a predicate on the tape lets a loop carry it as an invariant: each iteration shifts the stream by the bits it used.

def Complexity.TM.GuessFrom (g : ℕ → Bool) (t : Tape) : Prop

The guess tape carries the bits of g from its head onward.

Equations

• Complexity.TM.GuessFrom g t = ∀ (q : ℕ), t.cells (t.head + q) = Complexity.Γ.ofBool (g q)

theorem Complexity.TM.guessFrom_loadTape (g : ℕ → Bool) : GuessFrom g (NTM.loadTape g)

A loaded guess tape carries its stream.

theorem Complexity.TM.guessFrom_blocks {g : ℕ → Bool} {t : Tape} (h : GuessFrom g t) (w : ℕ → ℕ) (p q : ℕ) : t.cells (t.head + guessOffset w p + q) = Γ.ofBool (g (guessOffset w p + q))

A stage's blocks are read off the stream at their offsets.

theorem Complexity.TM.guessFrom_after {k : ℕ} (j : ℕ → Fin (k + 1)) (hj : ∀ (p : ℕ), j p ≠ Fin.last k) (w : ℕ → ℕ) (t : ℕ) (W : Fin (k + 1) → Tape) (hinv : ∀ (i : Fin (k + 1)), (W i).StartInvariant) (hh : ∀ (i : Fin (k + 1)), 1 ≤ (W i).head) (hinj : ∀ (p q : ℕ), p < t → q < t → j p = j q → p = q) (g : ℕ → Bool) (hg : GuessFrom g (W (Fin.last k))) : GuessFrom (fun (q : ℕ) => g (guessOffset w t + q)) (guessBlocksTapes j w t W (Fin.last k))

A stage consumes a prefix and leaves the rest.

A stream that feeds every stage

A machine that guesses in a loop consumes one stage's worth of bits per pass. Saying what the whole guess tape must contain is then a statement about a doubly-indexed family: stage s, block p, bit q. Such a stream always exists — the offsets of distinct stages and blocks never collide.

def Complexity.TM.StageBlocks (w : ℕ → ℕ) (t : ℕ) (b : ℕ → ℕ → ℕ → Bool) (g : ℕ → Bool) : Prop

The stream gives stage s its block p's bit q.

Equations

• Complexity.TM.StageBlocks w t b g = ∀ (s p q : ℕ), p < t → q ≤ w p → g (s * Complexity.TM.guessOffset w t + (Complexity.TM.guessOffset w p + q)) = b s p q

theorem Complexity.TM.guessOffset_pos (w : ℕ → ℕ) {t : ℕ} (ht : 0 < t) : 0 < guessOffset w t

theorem Complexity.TM.guessOffset_lt (w : ℕ → ℕ) {t p q : ℕ} (hp : p < t) (hq : q ≤ w p) : guessOffset w p + q < guessOffset w t

theorem Complexity.TM.exists_stageBlocks (w : ℕ → ℕ) {t : ℕ} (ht : 0 < t) (b : ℕ → ℕ → ℕ → Bool) : ∃ (g : ℕ → Bool), StageBlocks w t b g

Every family of stages is realized by some stream.

theorem Complexity.TM.blocks_of_stageBlocks {w : ℕ → ℕ} {t : ℕ} {b : ℕ → ℕ → ℕ → Bool} {g : ℕ → Bool} (hs : StageBlocks w t b g) (s : ℕ) {τ : Tape} (hgf : GuessFrom (fun (q : ℕ) => g (s * guessOffset w t + q)) τ) (p : ℕ) : p < t → ∀ q ≤ w p, τ.cells (τ.head + guessOffset w p + q) = Γ.ofBool (b s p q)

A stage reads its own blocks off the stream. This is the hypothesis a guess stage's contract asks for, supplied by the loop invariant's guess-tape clause.

A whole guess-and-rewind stage

def Complexity.TM.guessStageTM {k : ℕ} (j : ℕ → Fin (k + 1)) (w : ℕ → ℕ) (t : ℕ) (targets : List (Fin k)) : TM (k + 1)

A guess stage. Write a block of guesses onto each of t registers, then bring the named registers' heads back to cell one — the form every scan expects to read. The input head is left alone: a machine simulating another one keeps its input head where the simulation put it.

Equations

• Complexity.TM.guessStageTM j w t targets = Complexity.TM.guessThenTM j w t (Complexity.TM.parkRewindWorkTM targets)

theorem Complexity.TM.guessProtocol_guessStageTM {k : ℕ} (j : ℕ → Fin (k + 1)) (w : ℕ → ℕ) (t : ℕ) (targets : List (Fin k)) : (guessStageTM j w t targets).GuessProtocol (seqAdv (guessBlocksAdv j w t) fun (x : (parkRewindWorkTM targets).liftLast.Q) => false)

A guess stage respects the protocol.

theorem Complexity.TM.guessStageTM_hoareTime {k : ℕ} (j : ℕ → Fin (k + 1)) (hj : ∀ (p : ℕ), j p ≠ Fin.last k) (w : ℕ → ℕ) (t : ℕ) (targets : List (Fin k)) (hnodup : targets.Nodup) (B : ℕ) (hB : 1 ≤ B) (inp₀ out₀ : Tape) (W₀ : Fin (k + 1) → Tape) (hinpSI : inp₀.StartInvariant) (houtSI : out₀.StartInvariant) (hinp : inp₀.read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) (hinvW : ∀ (i : Fin (k + 1)), (W₀ i).StartInvariant) (hhW : ∀ (i : Fin (k + 1)), 1 ≤ (W₀ i).head) (hinj : ∀ (p q : ℕ), p < t → q < t → j p = j q → p = q) (hbound : ∀ i ∈ targets, (guessBlocksTapes j w t W₀ i.castSucc).head ≤ B) : (guessStageTM j w t targets).HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = W₀) (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => work (Fin.last k) = guessBlocksTapes j w t W₀ (Fin.last k) ∧ inp = parkTape inp₀ ∧ ((fun (i : Fin k) => work i.castSucc) = fun (i : Fin k) => if i ∈ targets then { head := 1, cells := (guessBlocksTapes j w t W₀ i.castSucc).cells } else parkTape (guessBlocksTapes j w t W₀ i.castSucc)) ∧ out = parkTape out₀) (guessBlocksTime w t + 1 + (1 + 1 + (targets.length * (B + 3) + 1)))

The contract of a guess stage.