Counter-building TM subroutines

Deterministic helper machines for materializing unary counters on work tapes.

The SAT-specific NP construction only needs a linear witness bound: assignment.length ≤ input.length + 1. This file defines a small machine that writes exactly |input| + 1 unary marks to a designated counter tape.

def Complexity.Tape.HasUnaryPrefix (t : Tape) (used : ℕ) : Prop

A counter tape while it is being built: cells 1..used contain unary marks, the head is at cell used + 1, and the tail from that cell onward is blank.

Equations

• t.HasUnaryPrefix used = (t.head = used + 1 ∧ (∀ i < used, t.cells (i + 1) = Complexity.Γ.one) ∧ ∀ (i : ℕ), used ≤ i → t.cells (i + 1) = Complexity.Γ.blank)

theorem Complexity.Tape.init_nil_move_right_hasUnaryPrefix_zero : ((init []).move Dir3.right).HasUnaryPrefix 0

An empty tape moved one cell right has the empty unary prefix: the head is at cell 1 and every cell after ▷ is blank.

theorem Complexity.Tape.hasUnaryPrefix_write_one {t : Tape} {used : ℕ} (h : t.HasUnaryPrefix used) : (t.writeAndMove Γ.one Dir3.right).HasUnaryPrefix (used + 1)

Writing one mark at the current head and moving right extends a unary prefix by one cell.

theorem Complexity.Tape.hasUnaryPrefix_write_one_cell0 {t : Tape} {used : ℕ} (h : t.HasUnaryPrefix used) (h0 : t.cells 0 = Γ.start) : (t.writeAndMove Γ.one Dir3.right).cells 0 = Γ.start

Writing the next unary mark preserves the left-end marker cell.

theorem Complexity.Tape.hasUnaryPrefix_cells_ne_start {t : Tape} {used : ℕ} (h : t.HasUnaryPrefix used) (j : ℕ) : j ≥ 1 → t.cells j ≠ Γ.start

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

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

A unary counter tape positioned at its first data cell.

HasUnaryCounter t B means cells 1..B contain 1, cell B+1 is blank, and the head is at cell 1.

Equations

• t.HasUnaryCounter B = (t.head = 1 ∧ (∀ i < B, t.cells (i + 1) = Complexity.Γ.one) ∧ t.cells (B + 1) = Complexity.Γ.blank)

theorem Complexity.Tape.hasUnaryCounter_of_hasUnaryPrefix {t t' : Tape} {B : ℕ} (hprefix : t.HasUnaryPrefix B) (hhead : t'.head = 1) (hcells : t'.cells = t.cells) : t'.HasUnaryCounter B

Rewinding a built unary prefix to cell 1 yields the public counter shape.

theorem Complexity.Tape.hasUnaryCounter_read_zero {t : Tape} (h : t.HasUnaryCounter 0) : t.read = Γ.blank

A tape holding a zero-length unary counter reads blank at its head.

theorem Complexity.Tape.hasUnaryCounter_read_pos {t : Tape} {B : ℕ} (h : t.HasUnaryCounter B) (hB : 0 < B) : t.read = Γ.one

A tape holding a positive-length unary counter reads 1 at its head.

def Complexity.Tape.HasCounterRemainder (t : Tape) (used total : ℕ) : Prop

Counter shape after used marks have already been consumed. The head is at the next unconsumed counter cell, previous cells are blanked, remaining marks are 1, and the first cell after the total bound is blank.

Equations

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

theorem Complexity.Tape.hasUnaryCounter_iff_remainder_zero {t : Tape} {B : ℕ} : t.HasUnaryCounter B ↔ t.HasCounterRemainder 0 B

A fresh unary counter is exactly a counter remainder with zero marks consumed.

theorem Complexity.Tape.hasCounterRemainder_read_blank_of_done {t : Tape} {B : ℕ} (h : t.HasCounterRemainder B B) : t.read = Γ.blank

Once all counter marks are consumed, the head reads blank.

theorem Complexity.Tape.hasCounterRemainder_read_one_of_remaining {t : Tape} {used total : ℕ} (h : t.HasCounterRemainder used total) (hlt : used < total) : t.read = Γ.one

While counter marks remain unconsumed, the head reads 1.

theorem Complexity.Tape.hasCounterRemainder_consume {t : Tape} {used total : ℕ} (h : t.HasCounterRemainder used total) (hlt : used < total) : (t.writeAndMove Γ.blank Dir3.right).HasCounterRemainder (used + 1) total

Blanking the current counter mark and moving right advances the unary counter remainder by one.

theorem Complexity.Tape.writeAndMove_readBack_idle_of_ne_start (t : Tape) (hread : t.read ≠ Γ.start) : t.writeAndMove (TM.readBackWrite t.read).toΓ (TM.idleDir t.read) = t

Writing back the currently read non-start symbol and idling preserves a tape. This is the basic preservation fact for non-active tapes in the counter and guessing machines.

inductive Complexity.TM.LinearCounterPhase : Type

Control states for inputLengthPlusOneCounterTM.

• scan : LinearCounterPhase
• rewind : LinearCounterPhase
• done : LinearCounterPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqLinearCounterPhase : DecidableEq LinearCounterPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeLinearCounterPhase : Fintype LinearCounterPhase

LinearCounterPhase has exactly the three states scan, rewind, done.

Equations

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

def Complexity.TM.inputLengthPlusOneCounterTM {n : ℕ} (counterIdx : Fin n) : TM n

Write a unary counter of length |input| + 1 to counterIdx.

Starting with the input head on ▷ and an empty counter tape, the scan phase skips the input start cell, writes one counter mark per input bit, then writes one extra mark when the input head reaches blank. The rewind phase rewinds the counter tape to cell 1 and halts.

The machine does not try to restore the input head; later composition layers can rewind or retarget input as needed.

Equations

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

theorem Complexity.TM.inputLengthPlusOneCounterTM_scan_start_state {n : ℕ} (counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hinp : inp.read = Γ.start) : (((inputLengthPlusOneCounterTM counterIdx).step { state := LinearCounterPhase.scan, input := inp, work := work, output := out }).get ⋯).state = LinearCounterPhase.scan

In the scan phase, reading ▷ on the input keeps the machine in scan.

theorem Complexity.TM.inputLengthPlusOneCounterTM_scan_start_initializes_counter {n : ℕ} (counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hinp : inp.read = Γ.start) (hcounter : work counterIdx = Tape.init []) : ((((inputLengthPlusOneCounterTM counterIdx).step { state := LinearCounterPhase.scan, input := inp, work := work, output := out }).get ⋯).work counterIdx).HasUnaryPrefix 0

The start-skip step positions an initially empty counter tape at cell 1, giving the zero-length unary-prefix invariant.

theorem Complexity.TM.inputLengthPlusOneCounterTM_scan_blank_state {n : ℕ} (counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hinp : inp.read = Γ.blank) : (((inputLengthPlusOneCounterTM counterIdx).step { state := LinearCounterPhase.scan, input := inp, work := work, output := out }).get ⋯).state = LinearCounterPhase.rewind

In the scan phase, reading blank on the input moves the machine to the rewind phase.

theorem Complexity.TM.inputLengthPlusOneCounterTM_scan_bit_state {n : ℕ} (counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hstart : inp.read ≠ Γ.start) (hblank : inp.read ≠ Γ.blank) : (((inputLengthPlusOneCounterTM counterIdx).step { state := LinearCounterPhase.scan, input := inp, work := work, output := out }).get ⋯).state = LinearCounterPhase.scan

In the scan phase, reading an input bit (neither ▷ nor blank) keeps the machine in scan.

theorem Complexity.TM.inputLengthPlusOneCounterTM_scan_bit_extends_counter {n : ℕ} (counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {used : ℕ} (hprefix : (work counterIdx).HasUnaryPrefix used) (hstart : inp.read ≠ Γ.start) (hblank : inp.read ≠ Γ.blank) : ((((inputLengthPlusOneCounterTM counterIdx).step { state := LinearCounterPhase.scan, input := inp, work := work, output := out }).get ⋯).work counterIdx).HasUnaryPrefix (used + 1)

Scanning an input bit writes one unary mark and advances the counter prefix by one.

theorem Complexity.TM.inputLengthPlusOneCounterTM_scan_blank_extends_counter {n : ℕ} (counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {used : ℕ} (hprefix : (work counterIdx).HasUnaryPrefix used) (hinp : inp.read = Γ.blank) : ((((inputLengthPlusOneCounterTM counterIdx).step { state := LinearCounterPhase.scan, input := inp, work := work, output := out }).get ⋯).work counterIdx).HasUnaryPrefix (used + 1)

Scanning the input blank writes the final extra unary mark and enters the rewind phase.

theorem Complexity.TM.inputLengthPlusOneCounterTM_rewind_start_state {n : ℕ} (counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcounter : (work counterIdx).read = Γ.start) : (((inputLengthPlusOneCounterTM counterIdx).step { state := LinearCounterPhase.rewind, input := inp, work := work, output := out }).get ⋯).state = LinearCounterPhase.done

In the rewind phase, reading ▷ on the counter tape moves the machine to done.

theorem Complexity.TM.inputLengthPlusOneCounterTM_rewind_left_state {n : ℕ} (counterIdx : Fin n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcounter : (work counterIdx).read ≠ Γ.start) : (((inputLengthPlusOneCounterTM counterIdx).step { state := LinearCounterPhase.rewind, input := inp, work := work, output := out }).get ⋯).state = LinearCounterPhase.rewind

In the rewind phase, a counter-tape read other than ▷ keeps the machine in rewind.

theorem Complexity.TM.inputLengthPlusOneCounterTM_toNTM_trace_one_preserves_started_blank_other_work {n : ℕ} (counterIdx : Fin n) (choice : Bool) (c : Cfg n (inputLengthPlusOneCounterTM counterIdx).Q) (i : Fin n) (hi : i ≠ counterIdx) (hwork : c.work i = (Tape.init []).move Dir3.right) : ((inputLengthPlusOneCounterTM counterIdx).toNTM.trace 1 (fun (x : Fin 1) => choice) c).work i = (Tape.init []).move Dir3.right

One NTM trace step of the lifted counter machine leaves a non-counter work tape unchanged when that tape is the started blank tape.

theorem Complexity.TM.inputLengthPlusOneCounterTM_toNTM_trace_one_initializes_blank_other_work {n : ℕ} (counterIdx : Fin n) (choice : Bool) (c : Cfg n (inputLengthPlusOneCounterTM counterIdx).Q) (i : Fin n) (hi : i ≠ counterIdx) (hstate : c.state ≠ LinearCounterPhase.done) (hwork : c.work i = Tape.init []) : ((inputLengthPlusOneCounterTM counterIdx).toNTM.trace 1 (fun (x : Fin 1) => choice) c).work i = (Tape.init []).move Dir3.right

One NTM trace step of the lifted counter machine (in a non-halted state) moves a fresh blank non-counter work tape past its ▷ marker, turning it into the started blank tape.

theorem Complexity.TM.inputLengthPlusOneCounterTM_toNTM_trace_one_preserves_started_blank_output {n : ℕ} (counterIdx : Fin n) (choice : Bool) (c : Cfg n (inputLengthPlusOneCounterTM counterIdx).Q) (houtput : c.output = (Tape.init []).move Dir3.right) : ((inputLengthPlusOneCounterTM counterIdx).toNTM.trace 1 (fun (x : Fin 1) => choice) c).output = (Tape.init []).move Dir3.right

One NTM trace step of the lifted counter machine leaves a started blank output tape unchanged.

theorem Complexity.TM.inputLengthPlusOneCounterTM_toNTM_trace_one_initializes_blank_output {n : ℕ} (counterIdx : Fin n) (choice : Bool) (c : Cfg n (inputLengthPlusOneCounterTM counterIdx).Q) (hstate : c.state ≠ LinearCounterPhase.done) (houtput : c.output = Tape.init []) : ((inputLengthPlusOneCounterTM counterIdx).toNTM.trace 1 (fun (x : Fin 1) => choice) c).output = (Tape.init []).move Dir3.right

One NTM trace step of the lifted counter machine (in a non-halted state) moves a fresh blank output tape past its ▷ marker, turning it into the started blank tape.

def Complexity.TM.inputLengthPlusOneCounterTime (xLen : ℕ) : ℕ

A convenient linear upper bound for inputLengthPlusOneCounterTM.

Equations

• Complexity.TM.inputLengthPlusOneCounterTime xLen = 3 * xLen + 10

theorem Complexity.TM.inputLengthPlusOneCounterTM_hoareTime {n : ℕ} (counterIdx : Fin n) (x : List Bool) : (inputLengthPlusOneCounterTM counterIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (x_1 : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ work counterIdx = Tape.init []) (fun (x_1 : Tape) (work : Fin n → Tape) (x_2 : Tape) => (work counterIdx).HasUnaryCounter (x.length + 1)) (inputLengthPlusOneCounterTime x.length)

inputLengthPlusOneCounterTM materializes a unary counter of length |x| + 1 on the designated work tape and rewinds it to cell 1.

theorem Complexity.TM.inputLengthPlusOneCounterTM_started_hoareTime {n : ℕ} (counterIdx : Fin n) (x : List Bool) : (inputLengthPlusOneCounterTM counterIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (x_1 : Tape) => inp = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work counterIdx = (Tape.init []).move Dir3.right) (fun (x_1 : Tape) (work : Fin n → Tape) (x_2 : Tape) => (work counterIdx).HasUnaryCounter (x.length + 1) ∧ (work counterIdx).cells 0 = Γ.start ∧ ∀ j ≥ 1, (work counterIdx).cells j ≠ Γ.start) (inputLengthPlusOneCounterTime x.length)

Started-tape variant of inputLengthPlusOneCounterTM_hoareTime: if the input is already positioned at cell 1 and the counter tape is the started blank tape, the machine still builds a unary counter of length |x| + 1. The postcondition also exposes the structural fact that the resulting counter tape has no ▷ markers beyond cell 0.

theorem Complexity.TM.inputLengthPlusOneCounterTM_started_tracksInput_hoareTime {n : ℕ} (counterIdx : Fin n) (x : List Bool) : (inputLengthPlusOneCounterTM counterIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (x_1 : Tape) => inp = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work counterIdx = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin n → Tape) (x_1 : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ inp.head = x.length + 1 ∧ (work counterIdx).HasUnaryCounter (x.length + 1) ∧ (work counterIdx).cells 0 = Γ.start ∧ ∀ j ≥ 1, (work counterIdx).cells j ≠ Γ.start) (inputLengthPlusOneCounterTime x.length)

Started-tape variant of the unary counter builder that also records the final input position. The input cells are unchanged, and the input head ends at the first blank after the scanned Boolean string.

theorem Complexity.TM.inputLengthPlusOneCounterTM_started_tracksInput_preserves_work_hoareTime {n : ℕ} (counterIdx passiveIdx : Fin n) (hne : passiveIdx ≠ counterIdx) (x y : List Bool) : (inputLengthPlusOneCounterTM counterIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work counterIdx = (Tape.init []).move Dir3.right ∧ work passiveIdx = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ inp.head = x.length + 1 ∧ work passiveIdx = (Tape.init (List.map Γ.ofBool y)).move Dir3.right ∧ (work counterIdx).HasUnaryCounter (x.length + 1) ∧ (work counterIdx).cells 0 = Γ.start ∧ (∀ j ≥ 1, (work counterIdx).cells j ≠ Γ.start) ∧ out = (Tape.init []).move Dir3.right) (inputLengthPlusOneCounterTime x.length)

Started-tape variant of the unary counter builder that also records the final input position and preserves one passive started Boolean work tape exactly.

theorem Complexity.TM.inputLengthPlusOneCounterTM_toNTM_hoareTime {n : ℕ} (counterIdx : Fin n) (x : List Bool) : (inputLengthPlusOneCounterTM counterIdx).toNTM.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (x_1 : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ work counterIdx = Tape.init []) (fun (x_1 : Tape) (work : Fin n → Tape) (x_2 : Tape) => (work counterIdx).HasUnaryCounter (x.length + 1)) (inputLengthPlusOneCounterTime x.length)

Nondeterministic form of inputLengthPlusOneCounterTM_hoareTime, for use inside NTM constructions after lifting the deterministic setup machine.