Nondeterministic TM subroutines

Small NTM building blocks used by NP constructions.

The main definition in this file is NTM.guessBoundedNTM: given a witness tape and a preloaded unary counter tape, nondeterministically write a witness whose length is at most the number of counter marks. The counter gives the guess phase a structural all-paths halting bound, which is essential for NTIME.

def Complexity.Tape.HasBinaryPrefix (t : Tape) (bits : List Bool) : Prop

A witness tape while it is being guessed: cells 1..|bits| contain the guessed bits, the head is at the next cell, and the remaining tail is blank.

Equations

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

def Complexity.Tape.HasBinaryString (t : Tape) (bits : List Bool) : Prop

A completed witness tape: the guessed bits are present and the head has been rewound to cell 1.

Equations

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

def Complexity.Tape.HasBoundedBinaryString (t : Tape) (B : ℕ) : Prop

A completed witness tape whose encoded string has length at most B.

Equations

• t.HasBoundedBinaryString B = ∃ (bits : List Bool), bits.length ≤ B ∧ t.HasBinaryString bits

theorem Complexity.Tape.hasOutput_of_hasBinaryString {t : Tape} {bits : List Bool} (h : t.HasBinaryString bits) : t.HasOutput bits

A completed witness tape encodes exactly bits as its output string.

theorem Complexity.Tape.cells_ne_start_of_hasBinaryString {t : Tape} {bits : List Bool} (h : t.HasBinaryString bits) (j : ℕ) : j ≥ 1 → t.cells j ≠ Γ.start

A completed witness tape never contains ▷ after the left-end marker.

theorem Complexity.Tape.eq_init_move_right_of_hasBinaryString {t : Tape} {bits : List Bool} (h : t.HasBinaryString bits) (h0 : t.cells 0 = Γ.start) : t = (init (List.map Γ.ofBool bits)).move Dir3.right

A completed binary witness tape with the left marker at cell 0 is exactly the standard initialized tape for those bits, moved to cell 1.

theorem Complexity.Tape.exists_eq_init_move_right_of_hasBoundedBinaryString {t : Tape} {B : ℕ} (h : t.HasBoundedBinaryString B) (h0 : t.cells 0 = Γ.start) : ∃ (bits : List Bool), bits.length ≤ B ∧ t = (init (List.map Γ.ofBool bits)).move Dir3.right

Bounded completed witness tapes expose exact initialized tape shape for some string whose length satisfies the same bound.

theorem Complexity.Tape.init_nil_move_right_hasBinaryPrefix_nil : ((init []).move Dir3.right).HasBinaryPrefix []

A freshly initialized empty tape, moved right past ▷, is an empty binary prefix.

theorem Complexity.Tape.hasBinaryPrefix_write_bit {t : Tape} {bits : List Bool} (bit : Bool) (h : t.HasBinaryPrefix bits) : (t.writeAndMove (Γ.ofBool bit) Dir3.right).HasBinaryPrefix (bits ++ [bit])

Writing the next guessed bit extends a binary prefix by one cell.

theorem Complexity.Tape.hasBinaryPrefix_write_bit_cell0 {t : Tape} {bits : List Bool} (bit : Bool) (h : t.HasBinaryPrefix bits) (h0 : t.cells 0 = Γ.start) : (t.writeAndMove (Γ.ofBool bit) Dir3.right).cells 0 = Γ.start

Writing the next guessed bit preserves the left-end marker cell.

theorem Complexity.Tape.cells_ne_start_of_hasBinaryPrefix {t : Tape} {bits : List Bool} (h : t.HasBinaryPrefix bits) (j : ℕ) : j ≥ 1 → t.cells j ≠ Γ.start

A binary prefix never contains ▷ after the left-end marker.

theorem Complexity.Tape.hasBinaryString_of_hasBinaryPrefix {t t' : Tape} {bits : List Bool} (hprefix : t.HasBinaryPrefix bits) (hhead : t'.head = 1) (hcells : t'.cells = t.cells) : t'.HasBinaryString bits

Rewinding a binary prefix to cell 1 yields a completed witness string.

inductive Complexity.NTM.GuessBoundedPhase : Type

Control states for guessBoundedNTM.

• choose: decide nondeterministically whether to stop or continue.
• write: write the next guessed bit and consume one counter mark.
• rewind: rewind the witness tape to cell 1.
• done: halt.

• choose : GuessBoundedPhase
• write : GuessBoundedPhase
• rewind : GuessBoundedPhase
• done : GuessBoundedPhase

@[implicit_reducible]

instance Complexity.NTM.instDecidableEqGuessBoundedPhase : DecidableEq GuessBoundedPhase

Equations

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

@[implicit_reducible]

instance Complexity.NTM.instFintypeGuessBoundedPhase : Fintype GuessBoundedPhase

GuessBoundedPhase has exactly the four listed control states.

Equations

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

def Complexity.NTM.guessBoundedNTM {n : ℕ} (witnessIdx counterIdx : Fin n) : NTM n

A bounded nondeterministic witness-guessing subroutine.

The machine uses two work tapes:

• witnessIdx: receives the guessed witness bits.
• counterIdx: is assumed to contain a unary counter. Each guessed bit consumes one counter mark by blanking the current counter cell and moving the counter head right.

At each choose state, choice false stops early; choice true continues if the counter is not blank. When the counter is blank, the machine must stop. It then rewinds the witness tape to cell 1 and halts.

Equations

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

theorem Complexity.NTM.guessBoundedNTM_trace_one_input_eq {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hread : c.input.read ≠ Γ.start) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) c).input = c.input

One step of guessBoundedNTM leaves the input tape unchanged, provided the input head is not on the ▷ marker.

theorem Complexity.NTM.guessBoundedNTM_trace_preserves_input {n : ℕ} (witnessIdx counterIdx : Fin n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hread : c.input.read ≠ Γ.start) : ((guessBoundedNTM witnessIdx counterIdx).trace T choices c).input = c.input

Any run of guessBoundedNTM leaves the input tape unchanged, provided the input head is not on the ▷ marker.

theorem Complexity.NTM.guessBoundedNTM_trace_one_output_eq {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hread : c.output.read ≠ Γ.start) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) c).output = c.output

One step of guessBoundedNTM leaves the output tape unchanged, provided the output head is not on the ▷ marker.

theorem Complexity.NTM.guessBoundedNTM_trace_preserves_output {n : ℕ} (witnessIdx counterIdx : Fin n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hread : c.output.read ≠ Γ.start) : ((guessBoundedNTM witnessIdx counterIdx).trace T choices c).output = c.output

Any run of guessBoundedNTM leaves the output tape unchanged, provided the output head is not on the ▷ marker.

theorem Complexity.NTM.guessBoundedNTM_trace_one_preserves_other_work {n : ℕ} (witnessIdx counterIdx otherIdx : Fin n) (choice : Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hwitness : otherIdx ≠ witnessIdx) (hcounter : otherIdx ≠ counterIdx) (hread : (c.work otherIdx).read ≠ Γ.start) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) c).work otherIdx = c.work otherIdx

One step of guessBoundedNTM leaves any work tape other than the witness and counter tapes unchanged, provided its head is not on ▷.

theorem Complexity.NTM.guessBoundedNTM_trace_preserves_other_work {n : ℕ} (witnessIdx counterIdx otherIdx : Fin n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hwitness : otherIdx ≠ witnessIdx) (hcounter : otherIdx ≠ counterIdx) (hread : (c.work otherIdx).read ≠ Γ.start) : ((guessBoundedNTM witnessIdx counterIdx).trace T choices c).work otherIdx = c.work otherIdx

Any run of guessBoundedNTM leaves any work tape other than the witness and counter tapes unchanged, provided its head is not on ▷.

theorem Complexity.NTM.guessBoundedNTM_choose_counter_blank_state {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcounter : (work counterIdx).read = Γ.blank) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).state = GuessBoundedPhase.rewind

In the choose state with a blank counter, one step moves to rewind regardless of the nondeterministic choice.

theorem Complexity.NTM.guessBoundedNTM_choose_stop_state {n : ℕ} (witnessIdx counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcounter : (work counterIdx).read ≠ Γ.blank) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => false) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).state = GuessBoundedPhase.rewind

In the choose state with a non-blank counter, choosing false stops the guess phase by moving to rewind.

theorem Complexity.NTM.guessBoundedNTM_choose_continue_state {n : ℕ} (witnessIdx counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcounter : (work counterIdx).read ≠ Γ.blank) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => true) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).state = GuessBoundedPhase.write

In the choose state with a non-blank counter, choosing true continues the guess phase by moving to write.

theorem Complexity.NTM.guessBoundedNTM_choose_continue_preserves_counter {n : ℕ} (witnessIdx counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {used total : ℕ} (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => true) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work counterIdx).HasCounterRemainder used total

A continuing choose-step preserves the counter tape while moving to the write state.

theorem Complexity.NTM.guessBoundedNTM_choose_continue_preserves_witness {n : ℕ} (witnessIdx counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} {used total : ℕ} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => true) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work witnessIdx).HasBinaryPrefix bits

A continuing choose-step preserves the current witness prefix while moving to the write state.

theorem Complexity.NTM.guessBoundedNTM_choose_continue_preserves_witness_cell0 {n : ℕ} (witnessIdx counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} {used total : ℕ} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcell0 : (work witnessIdx).cells 0 = Γ.start) (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => true) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work witnessIdx).cells 0 = Γ.start

A continuing choose-step preserves the witness tape's left-end marker.

theorem Complexity.NTM.guessBoundedNTM_choose_stop_preserves_witness {n : ℕ} (witnessIdx counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcounter : (work counterIdx).read ≠ Γ.blank) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => false) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work witnessIdx).HasBinaryPrefix bits

If the guess phase stops by choice, the choose-step preserves the witness prefix while entering rewind.

theorem Complexity.NTM.guessBoundedNTM_choose_stop_preserves_witness_cell0 {n : ℕ} (witnessIdx counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcell0 : (work witnessIdx).cells 0 = Γ.start) (hcounter : (work counterIdx).read ≠ Γ.blank) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => false) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work witnessIdx).cells 0 = Γ.start

If the guess phase stops by choice, the choose-step preserves the witness tape's left-end marker.

theorem Complexity.NTM.guessBoundedNTM_choose_counter_blank_preserves_witness {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcounter : (work counterIdx).read = Γ.blank) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work witnessIdx).HasBinaryPrefix bits

If the counter is empty, the choose-step is forced into rewind and preserves the witness prefix.

theorem Complexity.NTM.guessBoundedNTM_choose_counter_blank_preserves_witness_cell0 {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcell0 : (work witnessIdx).cells 0 = Γ.start) (hcounter : (work counterIdx).read = Γ.blank) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work witnessIdx).cells 0 = Γ.start

If the counter is empty, the choose-step preserves the witness tape's left-end marker.

theorem Complexity.NTM.guessBoundedNTM_write_counter_blank_state {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcounter : (work counterIdx).read = Γ.blank) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.write, input := inp, work := work, output := out }).state = GuessBoundedPhase.rewind

In the write state with a blank counter, one step moves to rewind without writing a bit.

theorem Complexity.NTM.guessBoundedNTM_write_consume_state {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcounter : (work counterIdx).read ≠ Γ.blank) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.write, input := inp, work := work, output := out }).state = GuessBoundedPhase.choose

In the write state with a non-blank counter, one step writes a bit and returns to the choose state.

theorem Complexity.NTM.guessBoundedNTM_write_consumes_counter {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {used total : ℕ} (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.write, input := inp, work := work, output := out }).work counterIdx).HasCounterRemainder (used + 1) total

In the writing state, if the counter tape has remaining unary marks, one NTM step consumes exactly one mark from the counter.

theorem Complexity.NTM.guessBoundedNTM_hasBinaryPrefix_append_of_write {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcounter : (work counterIdx).read ≠ Γ.blank) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.write, input := inp, work := work, output := out }).work witnessIdx).HasBinaryPrefix (bits ++ [choice])

In the writing state, the witness tape receives the chosen bit and advances to the next blank cell.

theorem Complexity.NTM.guessBoundedNTM_write_preserves_witness_cell0 {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcell0 : (work witnessIdx).cells 0 = Γ.start) (hcounter : (work counterIdx).read ≠ Γ.blank) : (((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.write, input := inp, work := work, output := out }).work witnessIdx).cells 0 = Γ.start

In the writing state, writing a bit preserves the witness tape's left-end marker.

theorem Complexity.NTM.guessBoundedNTM_continue_write_consumes_counter {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (bit : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {used total : ℕ} (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : (((guessBoundedNTM witnessIdx counterIdx).trace 2 (fun (i : Fin 2) => if ↑i = 0 then true else bit) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work counterIdx).HasCounterRemainder (used + 1) total

The normal two-step continue/write sequence consumes one counter mark. This is the induction step used by bounded guessing proofs.

theorem Complexity.NTM.guessBoundedNTM_continue_write_state {n : ℕ} (witnessIdx counterIdx : Fin n) (bit : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {used total : ℕ} (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : ((guessBoundedNTM witnessIdx counterIdx).trace 2 (fun (i : Fin 2) => if ↑i = 0 then true else bit) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).state = GuessBoundedPhase.choose

The normal two-step continue/write sequence returns to the choose state.

theorem Complexity.NTM.guessBoundedNTM_continue_write_extends_witness {n : ℕ} (witnessIdx counterIdx : Fin n) (bit : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} {used total : ℕ} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : (((guessBoundedNTM witnessIdx counterIdx).trace 2 (fun (i : Fin 2) => if ↑i = 0 then true else bit) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work witnessIdx).HasBinaryPrefix (bits ++ [bit])

The normal two-step continue/write sequence appends the chosen bit to the witness tape.

theorem Complexity.NTM.guessBoundedNTM_continue_write_preserves_witness_cell0 {n : ℕ} (witnessIdx counterIdx : Fin n) (bit : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} {used total : ℕ} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcell0 : (work witnessIdx).cells 0 = Γ.start) (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : (((guessBoundedNTM witnessIdx counterIdx).trace 2 (fun (i : Fin 2) => if ↑i = 0 then true else bit) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }).work witnessIdx).cells 0 = Γ.start

The normal two-step continue/write sequence preserves the witness tape's left-end marker.

theorem Complexity.NTM.guessBoundedNTM_continue_write_invariants {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (bit : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) {bits : List Bool} {used total : ℕ} (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcell0 : (work witnessIdx).cells 0 = Γ.start) (hcounter : (work counterIdx).HasCounterRemainder used total) (hlt : used < total) : have c' := (guessBoundedNTM witnessIdx counterIdx).trace 2 (fun (i : Fin 2) => if ↑i = 0 then true else bit) { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }; c'.state = GuessBoundedPhase.choose ∧ (c'.work counterIdx).HasCounterRemainder (used + 1) total ∧ (c'.work witnessIdx).HasBinaryPrefix (bits ++ [bit]) ∧ (c'.work witnessIdx).cells 0 = Γ.start

Bundled invariant update for one successful continue/write iteration.

theorem Complexity.NTM.guessBoundedNTM_rewind_at_start_state {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hwitness : (work witnessIdx).read = Γ.start) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.rewind, input := inp, work := work, output := out }).state = GuessBoundedPhase.done

In the rewind state with the witness head on ▷, one step halts by moving to done.

theorem Complexity.NTM.guessBoundedNTM_rewind_left_state {n : ℕ} (witnessIdx counterIdx : Fin n) (choice : Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hwitness : (work witnessIdx).read ≠ Γ.start) : ((guessBoundedNTM witnessIdx counterIdx).trace 1 (fun (x : Fin 1) => choice) { state := GuessBoundedPhase.rewind, input := inp, work := work, output := out }).state = GuessBoundedPhase.rewind

In the rewind state with the witness head not on ▷, one step stays in the rewind state.

theorem Complexity.NTM.guessBoundedNTM_rewind_completes_witness {n : ℕ} (witnessIdx counterIdx : Fin n) (bits : List Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hstate : c.state = GuessBoundedPhase.rewind) (hwitness : (c.work witnessIdx).HasBinaryPrefix bits) (hcell0 : (c.work witnessIdx).cells 0 = Γ.start) (choices : Fin (bits.length + 2) → Bool) : have c' := (guessBoundedNTM witnessIdx counterIdx).trace (bits.length + 2) choices c; (guessBoundedNTM witnessIdx counterIdx).halted c' ∧ (c'.work witnessIdx).HasBinaryString bits ∧ (c'.work witnessIdx).cells 0 = Γ.start

From the rewind state with a binary prefix on the witness tape, the machine halts within bits.length + 2 steps with a completed witness string and the left-end marker intact.

theorem Complexity.NTM.guessBoundedNTM_choose_counter_blank_completes_witness {n : ℕ} (witnessIdx counterIdx : Fin n) (bits : List Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcell0 : (work witnessIdx).cells 0 = Γ.start) (hcounter : (work counterIdx).read = Γ.blank) (choices : Fin (bits.length + 3) → Bool) : have c' := (guessBoundedNTM witnessIdx counterIdx).trace (bits.length + 3) choices { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }; (guessBoundedNTM witnessIdx counterIdx).halted c' ∧ (c'.work witnessIdx).HasBinaryString bits ∧ (c'.work witnessIdx).cells 0 = Γ.start

If the counter is already blank in the choose state, the guess phase is forced to stop and then rewind the current witness prefix.

theorem Complexity.NTM.guessBoundedNTM_hasBinaryString_of_choose_stop {n : ℕ} (witnessIdx counterIdx : Fin n) (bits : List Bool) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hwitness : (work witnessIdx).HasBinaryPrefix bits) (hcell0 : (work witnessIdx).cells 0 = Γ.start) (hcounter : (work counterIdx).read ≠ Γ.blank) (choices : Fin (bits.length + 3) → Bool) (hchoice : choices ⟨0, ⋯⟩ = false) : have c' := (guessBoundedNTM witnessIdx counterIdx).trace (bits.length + 3) choices { state := GuessBoundedPhase.choose, input := inp, work := work, output := out }; (guessBoundedNTM witnessIdx counterIdx).halted c' ∧ (c'.work witnessIdx).HasBinaryString bits ∧ (c'.work witnessIdx).cells 0 = Γ.start

If the first choice from choose is false, the guess phase stops early and rewinds the current witness prefix.

def Complexity.NTM.guessBoundedTime (remaining prefixLen : ℕ) : ℕ

A simple all-path bound for the bounded guessing loop.

From a prefix of length prefixLen and remaining available counter marks, the worst case guesses every remaining bit, takes two steps per bit, then rewinds the final witness string.

Equations

• Complexity.NTM.guessBoundedTime remaining prefixLen = 3 * remaining + prefixLen + 3

theorem Complexity.NTM.guessBoundedNTM_halted_hasBoundedBinaryString_of_choose {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (B : ℕ) (bits : List Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hstate : c.state = GuessBoundedPhase.choose) (hwitness : (c.work witnessIdx).HasBinaryPrefix bits) (hcell0 : (c.work witnessIdx).cells 0 = Γ.start) (hcounter : (c.work counterIdx).HasUnaryCounter B) (choices : Fin (guessBoundedTime B bits.length) → Bool) : have c' := (guessBoundedNTM witnessIdx counterIdx).trace (guessBoundedTime B bits.length) choices c; (guessBoundedNTM witnessIdx counterIdx).halted c' ∧ ∃ (finalBits : List Bool), finalBits.length ≤ bits.length + B ∧ (c'.work witnessIdx).HasBinaryString finalBits ∧ (c'.work witnessIdx).cells 0 = Γ.start

From any choose configuration with a completed unary counter and a binary prefix on the witness tape, every path halts within guessBoundedTime and leaves a completed witness string no longer than the prefix plus the counter bound.

theorem Complexity.NTM.guessBoundedNTM_hoareTime {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (B : ℕ) : (guessBoundedNTM witnessIdx counterIdx).HoareTime (fun (x : Tape) (work : Fin n → Tape) (x_1 : Tape) => (work witnessIdx).HasBinaryPrefix [] ∧ (work witnessIdx).cells 0 = Γ.start ∧ (work counterIdx).HasUnaryCounter B) (fun (x : Tape) (work : Fin n → Tape) (x_1 : Tape) => (work witnessIdx).HasBoundedBinaryString B) (guessBoundedTime B 0)

Hoare-style all-path specification for guessBoundedNTM, starting from an empty binary prefix and a unary counter of length B.

theorem Complexity.NTM.guessBoundedNTM_hoareTime_with_cell0 {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (B : ℕ) : (guessBoundedNTM witnessIdx counterIdx).HoareTime (fun (x : Tape) (work : Fin n → Tape) (x_1 : Tape) => (work witnessIdx).HasBinaryPrefix [] ∧ (work witnessIdx).cells 0 = Γ.start ∧ (work counterIdx).HasUnaryCounter B) (fun (x : Tape) (work : Fin n → Tape) (x_1 : Tape) => (work witnessIdx).HasBoundedBinaryString B ∧ (work witnessIdx).cells 0 = Γ.start) (guessBoundedTime B 0)

Stronger Hoare-style specification for guessBoundedNTM that retains the left-end marker fact needed by later tape consumers.

theorem Complexity.NTM.guessBoundedNTM_hoareTime_initTape_move_right {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (B : ℕ) : (guessBoundedNTM witnessIdx counterIdx).HoareTime (fun (x : Tape) (work : Fin n → Tape) (x_1 : Tape) => (work witnessIdx).HasBinaryPrefix [] ∧ (work witnessIdx).cells 0 = Γ.start ∧ (work counterIdx).HasUnaryCounter B) (fun (x : Tape) (work : Fin n → Tape) (x_1 : Tape) => ∃ (bits : List Bool), bits.length ≤ B ∧ work witnessIdx = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right) (guessBoundedTime B 0)

Hoare-style all-path specification for guessBoundedNTM with the completed witness tape in exact initialized-tape form.

theorem Complexity.NTM.guessBoundedNTM_hoareTime_init_move_right_frame {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (B : ℕ) (input0 output0 : Tape) (frame : Fin n → Tape) (hinput_read : input0.read ≠ Γ.start) (houtput_read : output0.read ≠ Γ.start) (hframe_read : ∀ (i : Fin n), i ≠ witnessIdx → i ≠ counterIdx → (frame i).read ≠ Γ.start) : (guessBoundedNTM witnessIdx counterIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = input0 ∧ out = output0 ∧ (∀ (i : Fin n), i ≠ witnessIdx → i ≠ counterIdx → work i = frame i) ∧ (work witnessIdx).HasBinaryPrefix [] ∧ (work witnessIdx).cells 0 = Γ.start ∧ (work counterIdx).HasUnaryCounter B) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = input0 ∧ out = output0 ∧ (∀ (i : Fin n), i ≠ witnessIdx → i ≠ counterIdx → work i = frame i) ∧ ∃ (bits : List Bool), bits.length ≤ B ∧ work witnessIdx = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right) (guessBoundedTime B 0)

Framed exact-tape Hoare specification for guessBoundedNTM: besides producing an exact initialized witness tape, the real input, output, and every non-witness/non-counter work tape whose head is already past ▷ are preserved unchanged.

theorem Complexity.NTM.guessBoundedNTM_choose_generates_witness {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (B : ℕ) (bits suffix : List Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hlen : suffix.length ≤ B) (hstate : c.state = GuessBoundedPhase.choose) (hwitness : (c.work witnessIdx).HasBinaryPrefix bits) (hcell0 : (c.work witnessIdx).cells 0 = Γ.start) (hcounter : (c.work counterIdx).HasUnaryCounter B) : ∃ (choices : Fin (guessBoundedTime B bits.length) → Bool), have c' := (guessBoundedNTM witnessIdx counterIdx).trace (guessBoundedTime B bits.length) choices c; (guessBoundedNTM witnessIdx counterIdx).halted c' ∧ (c'.work witnessIdx).HasBinaryString (bits ++ suffix) ∧ (c'.work witnessIdx).cells 0 = Γ.start

Completeness of the bounded guess phase: any suffix within the unary counter bound can be produced by some nondeterministic path.

theorem Complexity.NTM.guessBoundedNTM_choose_generates_witness_initTape_move_right {n : ℕ} (witnessIdx counterIdx : Fin n) (hne : witnessIdx ≠ counterIdx) (B : ℕ) (bits suffix : List Bool) (c : Cfg n (guessBoundedNTM witnessIdx counterIdx).Q) (hlen : suffix.length ≤ B) (hstate : c.state = GuessBoundedPhase.choose) (hwitness : (c.work witnessIdx).HasBinaryPrefix bits) (hcell0 : (c.work witnessIdx).cells 0 = Γ.start) (hcounter : (c.work counterIdx).HasUnaryCounter B) : ∃ (choices : Fin (guessBoundedTime B bits.length) → Bool), have c' := (guessBoundedNTM witnessIdx counterIdx).trace (guessBoundedTime B bits.length) choices c; (guessBoundedNTM witnessIdx counterIdx).halted c' ∧ c'.work witnessIdx = (Tape.init (List.map Γ.ofBool (bits ++ suffix))).move Dir3.right

Exact-tape form of guessBoundedNTM_choose_generates_witness, convenient for feeding a chosen witness directly into pair construction.