Checking one tape window against its successor

⚠️ Unreviewed by Bolton

A configuration of the simulated machine is held in registers, one per field, and the machine checks a guessed successor rather than computing one — on a nondeterministic machine that is free, and checking is a scan.

This file is the part of that check concerning one tape window. The window is a marked block: one chunk per cell, each chunk three bits, the head marker first so that a rightward scan knows whether the head is on a cell before it reads that cell's symbol. The checks are

• the marker is on exactly one chunk,
• the symbols agree everywhere except under the marker, where the new window carries the written symbol — except at cell zero, where a write is a no-op,
• the new marker sits where the direction says.

Each is a fold over chunks, and Complexity.Scanner.cellFold_chunk turns it into the cell-level fold a Complexity.Scanner runs.

Main definitions

• Complexity.markOf, Complexity.symOf — the marker and symbol of a chunk
• Complexity.markCount — how many chunks carry the marker
• Complexity.markStep, Complexity.agreeStep — the marker-count and symbol folds
• Complexity.stayStep, Complexity.rightStep, Complexity.leftStep — one fold per direction
• Complexity.dirStep, Complexity.movedMark — the three folded into one, and where the marker must land
• Complexity.HoldsWindow, Complexity.HoldsBits — a register whose cells spell out an encoded window, or any bitstring
• Complexity.inHeadStep, Complexity.inHeadEmit — the input-head check, all three directions
• Complexity.blockStep, Complexity.blockEmit — the four checks run together
• Complexity.SuccParams, Complexity.succParamsCodec — what the check is handed, and its layout

Main results

• Complexity.markStep_run — the count fold reports whether there are none, one, or more
• Complexity.agreeStep_run, Complexity.agreeOk_iff — what the symbol check reports
• Complexity.stayStep_run, Complexity.rightStep_run, Complexity.leftStep_state — what each displacement check reports
• Complexity.dirEmit_run — and what the combined displacement check reports, whichever way the head moves
• Complexity.blockEmit_run — and what all four together report on one block
• Complexity.markOf_of_holds, Complexity.symOf_of_holds — what a scan reads off an encoded window
• Complexity.markCount_eq — an encoded window carries exactly one marker
• Complexity.eq_run_of_holds, Complexity.eq_run_state — the comparison scan decides equality of what two registers hold, and so decides the state field
• Complexity.valUpTo_of_holds — what a scan reads a register as, as a number
• Complexity.tableSlice_eq, Complexity.ofTable_of_holdsBits, Complexity.ofTable_of_holds — and through a codec, as a value: whatever bits a register holds, and when they are an encoding
• Complexity.plusOne_of_holds, Complexity.plusOne_of_holds_fin — the increment scan decides the input-head field
• Complexity.inHeadEmit_of_holds — and the input-head check, whichever way the head moves
• Complexity.moved_of_holds, Complexity.sym_of_holds — the displacement and symbol conditions, read as statements about the decoded windows
• Complexity.blockEmit_holds — and the whole check: the scan accepts exactly when the new window is the old one stepped
• Complexity.mem_codeSucc_iff — a successor code is the code of one step
• Complexity.succCode_state, Complexity.succCode_inputHead, Complexity.succCode_work_head, Complexity.succCode_work_cells, Complexity.succCode_output_head, Complexity.succCode_output_cells — a successor's fields, one by one
• Complexity.eq_succCode_iff — and all of them at once: under the space bound a code is a successor exactly when every field is what the transition makes it
• Complexity.params_eq — the guessed parameters are pinned by the checks themselves
• Complexity.eq_succCode_of_checks — so the conditions the checks establish say exactly that one code is the successor of another
• Complexity.mem_codeSucc_of_checks — and hence that it is a successor at all

def Complexity.markOf {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (r : Fin (j + 1)) (p : ℕ) : Bool

The head marker of chunk p of the block starting after cell off, on register r.

Equations

• Complexity.markOf cols off r p = decide (cols (off + 3 * p + 1) r = Complexity.Γ.one)

def Complexity.symOf {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (r : Fin (j + 1)) (p : ℕ) : Bool × Bool

The two symbol bits of chunk p, on register r.

Equations

• Complexity.symOf cols off r p = (decide (cols (off + 3 * p + 2) r = Complexity.Γ.one), decide (cols (off + 3 * p + 3) r = Complexity.Γ.one))

def Complexity.markCount {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (r : Fin (j + 1)) : ℕ → ℕ

How many of the first m chunks carry the marker.

Equations

• Complexity.markCount cols off r 0 = 0
• Complexity.markCount cols off r p.succ = Complexity.markCount cols off r p + if Complexity.markOf cols off r p = true then 1 else 0

def Complexity.markStep {j : ℕ} (r : Fin (j + 1)) (x : Bool × Bool) (c1 _c2 _c3 : Fin (j + 1) → Γ) : Bool × Bool

Count the markers, saturating at two: the first component says there is at least one, the second that there are at least two.

Equations

• Complexity.markStep r x c1 _c2 _c3 = if c1 r = Complexity.Γ.one then (true, x.1 || x.2) else x

theorem Complexity.markStep_run {j : ℕ} (r : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off m : ℕ) : Scanner.chunkRun (markStep r) cols off (false, false) m = (decide (0 < markCount cols off r m), decide (1 < markCount cols off r m))

What the marker count reports.

The symbols

def Complexity.wantSym {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a : Fin (j + 1)) (wrB : Bool × Bool) (p : ℕ) : Bool × Bool

What the new window should carry at chunk p.

Equations

• Complexity.wantSym cols off a wrB p = if (Complexity.markOf cols off a p && decide (0 < p)) = true then wrB else Complexity.symOf cols off a p

def Complexity.agreeOk {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a b : Fin (j + 1)) (symB wrB : Bool × Bool) : ℕ → Bool

The symbol conditions on the first m chunks.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.agreeOk cols off a b symB wrB 0 = true

def Complexity.agreeStep {j : ℕ} (a b : Fin (j + 1)) (symB wrB x : Bool × Bool) (c1 c2 c3 : Fin (j + 1) → Γ) : Bool × Bool

The symbol-agreement fold. Its second component remembers that chunk zero has gone by, which is what suppresses the write there.

Equations

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

theorem Complexity.agreeStep_run {j : ℕ} (a b : Fin (j + 1)) (symB wrB : Bool × Bool) (cols : ℕ → Fin (j + 1) → Γ) (off m : ℕ) : Scanner.chunkRun (agreeStep a b symB wrB) cols off (true, false) m = (agreeOk cols off a b symB wrB m, decide (0 < m))

What the symbol check reports.

theorem Complexity.agreeOk_iff {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a b : Fin (j + 1)) (symB wrB : Bool × Bool) (m : ℕ) : agreeOk cols off a b symB wrB m = true ↔ ∀ p < m, symOf cols off b p = wantSym cols off a wrB p ∧ (markOf cols off a p = true → symOf cols off a p = symB)

The fold's verdict spelled out.

Where the marker moves

def Complexity.stayStep {j : ℕ} (a b : Fin (j + 1)) (x : Bool) (c1 _c2 _c3 : Fin (j + 1) → Γ) : Bool

The head stays: the markers must agree.

Equations

• Complexity.stayStep a b x c1 _c2 _c3 = (x && decide (c1 a = Complexity.Γ.one) == decide (c1 b = Complexity.Γ.one))

theorem Complexity.stayStep_run {j : ℕ} (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off m : ℕ) : Scanner.chunkRun (stayStep a b) cols off true m = true ↔ ∀ p < m, markOf cols off a p = markOf cols off b p

def Complexity.prevMark {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a : Fin (j + 1)) (p : ℕ) : Bool

The marker the rightward rule expects at chunk p.

Equations

• Complexity.prevMark cols off a p = if p = 0 then false else Complexity.markOf cols off a (p - 1)

def Complexity.rightStep {j : ℕ} (a b : Fin (j + 1)) (x : Bool × Bool) (c1 _c2 _c3 : Fin (j + 1) → Γ) : Bool × Bool

The head moves right: the new marker is one chunk on.

Equations

• Complexity.rightStep a b x c1 _c2 _c3 = (x.1 && decide (c1 b = Complexity.Γ.one) == x.2, decide (c1 a = Complexity.Γ.one))

theorem Complexity.rightStep_run {j : ℕ} (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off m : ℕ) : ((Scanner.chunkRun (rightStep a b) cols off (true, false) m).2 = if m = 0 then false else markOf cols off a (m - 1)) ∧ ((Scanner.chunkRun (rightStep a b) cols off (true, false) m).1 = true ↔ ∀ p < m, markOf cols off b p = prevMark cols off a p)

def Complexity.leftStep {j : ℕ} (a b : Fin (j + 1)) (x : Bool × Bool × Bool × Bool) (c1 _c2 _c3 : Fin (j + 1) → Γ) : Bool × Bool × Bool × Bool

The head moves left: the new marker is one chunk back, except from chunk zero, where moving left stays put. The fold carries the previous chunk's new marker, whether chunk zero has gone by, and whether the old marker was on chunk zero.

Equations

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

theorem Complexity.leftStep_state {j : ℕ} (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off m : ℕ) : 0 < m → (Scanner.chunkRun (leftStep a b) cols off (true, false, false, false) m).2.2.1 = true ∧ (Scanner.chunkRun (leftStep a b) cols off (true, false, false, false) m).2.2.2 = markOf cols off a 0 ∧ (Scanner.chunkRun (leftStep a b) cols off (true, false, false, false) m).2.1 = markOf cols off b (m - 1) ∧ ((Scanner.chunkRun (leftStep a b) cols off (true, false, false, false) m).1 = true ↔ if markOf cols off a 0 = true then markOf cols off b 0 = true ∧ ∀ (p : ℕ), 1 ≤ p → p < m → markOf cols off b p = false else ∀ (p : ℕ), 1 ≤ p → p < m → markOf cols off b (p - 1) = markOf cols off a p)

The state of the leftward-move check.

One displacement check, whichever way the head moves

def Complexity.dirStep {j : ℕ} (a b : Fin (j + 1)) (d : Dir3) (x : Bool × Bool × Bool × Bool) (c1 c2 c3 : Fin (j + 1) → Γ) : Bool × Bool × Bool × Bool

The displacement check for one block, in the direction the transition dictates. The three directions need different amounts of memory; this gives them all the widest state.

Equations

• Complexity.dirStep a b Complexity.Dir3.stay x c1 c2 c3 = (Complexity.stayStep a b x.1 c1 c2 c3, x.2)
• Complexity.dirStep a b Complexity.Dir3.right x c1 c2 c3 = ((Complexity.rightStep a b (x.1, x.2.1) c1 c2 c3).1, (Complexity.rightStep a b (x.1, x.2.1) c1 c2 c3).2, x.2.2)
• Complexity.dirStep a b Complexity.Dir3.left x c1 c2 c3 = Complexity.leftStep a b x c1 c2 c3

def Complexity.dirEmit (d : Dir3) (x : Bool × Bool × Bool × Bool) : Bool

The verdict of the displacement check.

Equations

• Complexity.dirEmit Complexity.Dir3.stay x = x.1
• Complexity.dirEmit Complexity.Dir3.right x = x.1
• Complexity.dirEmit Complexity.Dir3.left x = if x.2.2.2 = true then x.1 else x.1 && !x.2.1

theorem Complexity.dirStep_stay {j : ℕ} (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (y : Bool × Bool × Bool) (m : ℕ) : (Scanner.chunkRun (dirStep a b Dir3.stay) cols off (true, y) m).1 = Scanner.chunkRun (stayStep a b) cols off true m

theorem Complexity.dirStep_right {j : ℕ} (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (z : Bool × Bool) (m : ℕ) : ((Scanner.chunkRun (dirStep a b Dir3.right) cols off (true, false, z) m).1, (Scanner.chunkRun (dirStep a b Dir3.right) cols off (true, false, z) m).2.1) = Scanner.chunkRun (rightStep a b) cols off (true, false) m

theorem Complexity.dirStep_left {j : ℕ} (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off m : ℕ) : Scanner.chunkRun (dirStep a b Dir3.left) cols off (true, false, false, false) m = Scanner.chunkRun (leftStep a b) cols off (true, false, false, false) m

def Complexity.movedMark {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a : Fin (j + 1)) (d : Dir3) (p : ℕ) : Bool

Where the marker must sit in the new block, given the direction.

Equations

• Complexity.movedMark cols off a Complexity.Dir3.stay p = Complexity.markOf cols off a p
• Complexity.movedMark cols off a Complexity.Dir3.right p = Complexity.prevMark cols off a p
• Complexity.movedMark cols off a Complexity.Dir3.left p = if Complexity.markOf cols off a 0 = true then decide (p = 0) else Complexity.markOf cols off a (p + 1)

theorem Complexity.dirEmit_run {j : ℕ} (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (d : Dir3) (m : ℕ) (hm : 0 < m) (hend : markOf cols off a m = false) : dirEmit d (Scanner.chunkRun (dirStep a b d) cols off (true, false, false, false) m) = true ↔ ∀ p < m, markOf cols off b p = movedMark cols off a d p

What the displacement check reports.

A register that holds an encoded window

def Complexity.HoldsWindow {j m : ℕ} [NeZero m] (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (r : Fin (j + 1)) (hd : Fin m) (cl : Fin m → Γ) : Prop

The cells of register r, from off + 1 on, spell out the encoding of the window (hd, cl).

Equations

• Complexity.HoldsWindow cols off r hd cl = ∀ (q : ℕ) (hq : q < m * 3), cols (off + q + 1) r = Complexity.Γ.ofBool ((Complexity.tapeCodec m).enc (hd, cl))[q]

theorem Complexity.markOf_of_holds {j m : ℕ} [NeZero m] {cols : ℕ → Fin (j + 1) → Γ} {off : ℕ} {r : Fin (j + 1)} {hd : Fin m} {cl : Fin m → Γ} (h : HoldsWindow cols off r hd cl) (p : Fin m) : markOf cols off r ↑p = decide (p = hd)

The marker a scan reads off an encoded window.

theorem Complexity.symOf_of_holds {j m : ℕ} [NeZero m] {cols : ℕ → Fin (j + 1) → Γ} {off : ℕ} {r : Fin (j + 1)} {hd : Fin m} {cl : Fin m → Γ} (h : HoldsWindow cols off r hd cl) (p : Fin m) : symOf cols off r ↑p = gammaBits (cl p)

The symbol bits a scan reads off an encoded window.

theorem Complexity.gammaBits_injective : Function.Injective gammaBits

theorem Complexity.markCount_eq {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a : Fin (j + 1)) (hd m : ℕ) : (∀ p < m, markOf cols off a p = decide (p = hd)) → markCount cols off a m = if hd < m then 1 else 0

Counting the markers of a register that holds an encoded window.

def Complexity.movedIdx (d : Dir3) (h : ℕ) : ℕ

Where the head lands.

Equations

• Complexity.movedIdx Complexity.Dir3.stay h = h
• Complexity.movedIdx Complexity.Dir3.right h = h + 1
• Complexity.movedIdx Complexity.Dir3.left h = h - 1

theorem Complexity.moved_of_holds {j m : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a b : Fin (j + 1)) (hd hd' : ℕ) (hdm : hd < m) (hdm' : hd' < m) (d : Dir3) (ha : ∀ p < m, markOf cols off a p = decide (p = hd)) (hb : ∀ p < m, markOf cols off b p = decide (p = hd')) (hend : markOf cols off a m = false) : (∀ p < m, markOf cols off b p = movedMark cols off a d p) ↔ hd' = movedIdx d hd

What the displacement condition says about the decoded heads.

theorem Complexity.sym_of_holds {j m : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a b : Fin (j + 1)) (hd : Fin m) (cl cl' : Fin m → Γ) (sym wr : Γ) (ha : ∀ (p : Fin m), markOf cols off a ↑p = decide (p = hd)) (hsa : ∀ (p : Fin m), symOf cols off a ↑p = gammaBits (cl p)) (hsb : ∀ (p : Fin m), symOf cols off b ↑p = gammaBits (cl' p)) : (∀ p < m, symOf cols off b p = wantSym cols off a (gammaBits wr) p ∧ (markOf cols off a p = true → symOf cols off a p = gammaBits sym)) ↔ (∀ (p : Fin m), cl' p = if p = hd ∧ 0 < ↑p then wr else cl p) ∧ cl hd = sym

What the symbol condition says about the decoded windows.

Registers that hold a bitstring

def Complexity.HoldsBits {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (r : Fin (j + 1)) (bits : List Bool) : Prop

The cells of register r, from off + 1 on, spell out bits.

Equations

• Complexity.HoldsBits cols off r bits = ∀ (q : ℕ) (hq : q < bits.length), cols (off + q + 1) r = Complexity.Γ.ofBool bits[q]

theorem Complexity.ofBool_injective : Function.Injective Γ.ofBool

theorem Complexity.HoldsBits.inj {j : ℕ} {cols : ℕ → Fin (j + 1) → Γ} {off : ℕ} {r : Fin (j + 1)} {b₁ b₂ : List Bool} (h₁ : HoldsBits cols off r b₁) (h₂ : HoldsBits cols off r b₂) (hlen : b₁.length = b₂.length) : b₁ = b₂

A register determines the bits it holds.

theorem Complexity.isPrefix_ofFn {L : List Bool} {n : ℕ} (b : ℕ → Bool) (hlen : L.length ≤ n) (hb : ∀ (q : ℕ) (hq : q < L.length), b q = L[q]) : L <+: List.ofFn fun (q : Fin n) => b ↑q

A list is a prefix of the enumeration of a stream that agrees with it.

theorem Complexity.HoldsBits.of_isPrefix {j : ℕ} {cols : ℕ → Fin (j + 1) → Γ} {off : ℕ} {r : Fin (j + 1)} {L L' : List Bool} (h : HoldsBits cols off r L) (hp : L' <+: L) : HoldsBits cols off r L'

Holding a list of bits means holding any prefix of it: a register guessed one bit wider than a field still holds the field.

theorem Complexity.HoldsBits.drop_prefix {j : ℕ} {cols : ℕ → Fin (j + 1) → Γ} {r : Fin (j + 1)} {L M : List Bool} (h : HoldsBits cols 0 r (L ++ M)) : HoldsBits cols L.length r M

Holding a list means holding what follows a prefix of it, read from after that prefix. A register whose field sits after a block of padding is read this way: the scan that checks the field starts where the padding ends.

theorem Complexity.HoldsBits.shift {j : ℕ} {cols : ℕ → Fin (j + 1) → Γ} {off : ℕ} {r : Fin (j + 1)} {L : List Bool} (h : HoldsBits cols off r L) : HoldsBits (fun (t : ℕ) => cols (off + t)) 0 r L

Reading a register from an offset, as a scan that starts there.

theorem Complexity.eq_run_of_holds {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (r r' : Fin (j + 1)) (bits bits' : List Bool) (hlen : bits.length = bits'.length) (h : HoldsBits cols 0 r bits) (h' : HoldsBits cols 0 r' bits') : (Scanner.eq j r r').run cols bits.length = true ↔ bits = bits'

The comparison scan decides equality of what two registers hold.

theorem Complexity.eq_run_state {j : ℕ} {Q : Type} [Fintype Q] [Nonempty Q] (cols : ℕ → Fin (j + 1) → Γ) (r r' : Fin (j + 1)) (q q' : Q) (h : HoldsBits cols 0 r ((qCodec Q).enc q)) (h' : HoldsBits cols 0 r' ((qCodec Q).enc q')) : (Scanner.eq j r r').run cols (qCodec Q).width = true ↔ q = q'

The state check. Two registers holding encoded states agree exactly when the states do.

Reading a register as a number

Complexity.Scanner.plusOne speaks in Complexity.Scanner.valUpTo, the value of the bits a scan has passed; Complexity.finCodec stores a number as Complexity.bitsOfLenLE, whose value is Complexity.binValLE. Both are little-endian, so they agree.

theorem Complexity.binValLE_concat (l : List Bool) (b : Bool) : binValLE (l ++ [b]) = binValLE l + if b = true then 2 ^ l.length else 0

theorem Complexity.valUpTo_of_holds {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (r : Fin (j + 1)) (bits : List Bool) (h : HoldsBits cols 0 r bits) (p : ℕ) : p ≤ bits.length → Scanner.valUpTo (Scanner.bitAt cols r) p = binValLE (List.take p bits)

What a scan reads a register as.

theorem Complexity.plusOne_of_holds {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (r r' : Fin (j + 1)) (w u v : ℕ) (hu : u < 2 ^ w) (hv : v < 2 ^ w) (h : HoldsBits cols 0 r (bitsOfLenLE w u)) (h' : HoldsBits cols 0 r' (bitsOfLenLE w v)) : (Scanner.plusOne j r r').emit ((Scanner.plusOne j r r').run cols w) = true ↔ v = u + 1

The increment check decides the input-head condition.

theorem Complexity.plusOne_of_holds_fin {j m : ℕ} [NeZero m] (cols : ℕ → Fin (j + 1) → Γ) (r r' : Fin (j + 1)) (u v : Fin m) (h : HoldsBits cols 0 r ((finCodec m).enc u)) (h' : HoldsBits cols 0 r' ((finCodec m).enc v)) : (Scanner.plusOne j r r').emit ((Scanner.plusOne j r r').run cols (bitWidth m)) = true ↔ ↑v = ↑u + 1

The same, for registers holding a bounded index.

Reading a value off a register with a scan

def Complexity.tableSlice {s w : ℕ} (table : Fin s → Fin w → Bool) (t : Fin s) (c : ℕ) (hc : c ≤ w) : Fin c → Bool

The leading c bits a scan has read from one register.

Equations

• Complexity.tableSlice table t c hc i = table t ⟨↑i, ⋯⟩

theorem Complexity.tableSlice_eq {j : ℕ} (bits : List Bool) (c : ℕ) (hlen : bits.length = c) (cols : ℕ → Fin (j + 1) → Γ) (off s w : ℕ) (regs : Fin s → Fin (j + 1)) (t : Fin s) (hc : c ≤ w) (x₀ : Fin s → Fin w → Bool) (h : HoldsBits (fun (q : ℕ) => cols (off + q)) 0 (regs t) bits) (i : Fin c) : tableSlice (Scanner.auxRun (⟨0, ⋯⟩, x₀) (Scanner.bitsStep s w regs) (fun (q : ℕ) => cols (off + q)) w).2 t c hc i = bits[↑i]

What a scan has in its table: the bits the register holds.

theorem Complexity.ofTable_of_holdsBits {j : ℕ} {α : Type} (codec : BitCodec α) (bits : List Bool) (hlen : bits.length = codec.width) (cols : ℕ → Fin (j + 1) → Γ) (off s w : ℕ) (regs : Fin s → Fin (j + 1)) (t : Fin s) (hc : codec.width ≤ w) (x₀ : Fin s → Fin w → Bool) (h : HoldsBits (fun (q : ℕ) => cols (off + q)) 0 (regs t) bits) : codec.ofTable (tableSlice (Scanner.auxRun (⟨0, ⋯⟩, x₀) (Scanner.bitsStep s w regs) (fun (q : ℕ) => cols (off + q)) w).2 t codec.width hc) = codec.dec bits

What a scan reads a register as, through a codec, whatever bits it holds.

theorem Complexity.ofTable_of_holds {j : ℕ} {α : Type} (codec : BitCodec α) (val : α) (cols : ℕ → Fin (j + 1) → Γ) (off s w : ℕ) (regs : Fin s → Fin (j + 1)) (t : Fin s) (hc : codec.width ≤ w) (x₀ : Fin s → Fin w → Bool) (h : HoldsBits (fun (q : ℕ) => cols (off + q)) 0 (regs t) (codec.enc val)) : codec.ofTable (tableSlice (Scanner.auxRun (⟨0, ⋯⟩, x₀) (Scanner.bitsStep s w regs) (fun (q : ℕ) => cols (off + q)) w).2 t codec.width hc) = val

The same, when the register holds an encoding.

theorem Complexity.ofTable_of_holds_zero {j : ℕ} {α : Type} (codec : BitCodec α) (val : α) (cols : ℕ → Fin (j + 1) → Γ) (s w : ℕ) (regs : Fin s → Fin (j + 1)) (t : Fin s) (hc : codec.width ≤ w) (x₀ : Fin s → Fin w → Bool) (h : HoldsBits cols 0 (regs t) (codec.enc val)) : codec.ofTable (tableSlice (Scanner.auxRun (⟨0, ⋯⟩, x₀) (Scanner.bitsStep s w regs) cols w).2 t codec.width hc) = val

The same, for a scan that starts at the first cell.

The input head, whichever way it moves

def Complexity.inHeadStep {j : ℕ} (r r' : Fin (j + 1)) (d : Dir3) (x : Bool × Bool) (col : Fin (j + 1) → Γ) : Bool × Bool

The input-head check, in the direction the transition dictates. The three directions share a common state: stay compares, right checks an increment, and left checks one with the registers swapped, since v = u - 1 with u > 0 is u = v + 1.

Equations

• Complexity.inHeadStep r r' Complexity.Dir3.stay x col = ((Complexity.Scanner.eq j r r').stepR x.1 col, x.2)
• Complexity.inHeadStep r r' Complexity.Dir3.right x col = (Complexity.Scanner.plusOne j r r').stepR x col
• Complexity.inHeadStep r r' Complexity.Dir3.left x col = (Complexity.Scanner.plusOne j r' r).stepR x col

def Complexity.inHeadEmit (d : Dir3) (x : Bool × Bool) : Bool

The verdict of the input-head check.

Equations

• Complexity.inHeadEmit Complexity.Dir3.stay x = x.1
• Complexity.inHeadEmit Complexity.Dir3.right x = (!x.1 && x.2)
• Complexity.inHeadEmit Complexity.Dir3.left x = (!x.1 && x.2)

theorem Complexity.inHeadStep_right_eq {j : ℕ} (r r' : Fin (j + 1)) : inHeadStep r r' Dir3.right = (Scanner.plusOne j r r').stepR

theorem Complexity.inHeadStep_left_eq {j : ℕ} (r r' : Fin (j + 1)) : inHeadStep r r' Dir3.left = (Scanner.plusOne j r' r).stepR

theorem Complexity.inHeadStep_stay_fst {j : ℕ} (r r' : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (y : Bool) (p : ℕ) : (Scanner.cellFold (inHeadStep r r' Dir3.stay) cols off (true, y) p).1 = Scanner.cellFold (Scanner.eq j r r').stepR cols off true p

theorem Complexity.bitsOfLenLE_inj {w u v : ℕ} (hu : u < 2 ^ w) (hv : v < 2 ^ w) (h : bitsOfLenLE w u = bitsOfLenLE w v) : u = v

theorem Complexity.inHeadEmit_of_holds {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (r r' : Fin (j + 1)) (d : Dir3) (w u v : ℕ) (hu : u < 2 ^ w) (hv : v < 2 ^ w) (h : HoldsBits (fun (t : ℕ) => cols (off + t)) 0 r (bitsOfLenLE w u)) (h' : HoldsBits (fun (t : ℕ) => cols (off + t)) 0 r' (bitsOfLenLE w v)) (hleft : d = Dir3.left → 0 < u) : inHeadEmit d (Scanner.cellFold (inHeadStep r r' d) cols off (true, true) w) = true ↔ v = movedIdx d u

What the input-head check reports.

The whole check on one block

def Complexity.blockStep {j : ℕ} (a b : Fin (j + 1)) (symB wrB : Bool × Bool) (d : Dir3) (x : (Bool × Bool) × (Bool × Bool) × (Bool × Bool) × Bool × Bool × Bool × Bool) (c1 c2 c3 : Fin (j + 1) → Γ) : (Bool × Bool) × (Bool × Bool) × (Bool × Bool) × Bool × Bool × Bool × Bool

The four checks on one block, run together: the marker counts on each register, the symbols, and the displacement.

Equations

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

def Complexity.blockStart : (Bool × Bool) × (Bool × Bool) × (Bool × Bool) × Bool × Bool × Bool × Bool

Where the combined check starts.

Equations

• Complexity.blockStart = ((false, false), (false, false), (true, false), true, false, false, false)

def Complexity.blockEmit (d : Dir3) (x : (Bool × Bool) × (Bool × Bool) × (Bool × Bool) × Bool × Bool × Bool × Bool) : Bool

The combined verdict: one marker on each register, the symbols right, the head moved right.

Equations

• Complexity.blockEmit d x = (x.1.1 && !x.1.2 && (x.2.1.1 && !x.2.1.2) && x.2.2.1.1 && Complexity.dirEmit d x.2.2.2)

theorem Complexity.blockStep_run {j : ℕ} (a b : Fin (j + 1)) (symB wrB : Bool × Bool) (d : Dir3) (cols : ℕ → Fin (j + 1) → Γ) (off m : ℕ) : Scanner.chunkRun (blockStep a b symB wrB d) cols off blockStart m = (Scanner.chunkRun (markStep a) cols off (false, false) m, Scanner.chunkRun (markStep b) cols off (false, false) m, Scanner.chunkRun (agreeStep a b symB wrB) cols off (true, false) m, Scanner.chunkRun (dirStep a b d) cols off (true, false, false, false) m)

theorem Complexity.blockEmit_run {j : ℕ} (a b : Fin (j + 1)) (symB wrB : Bool × Bool) (d : Dir3) (cols : ℕ → Fin (j + 1) → Γ) (off m : ℕ) (hm : 0 < m) (hend : markOf cols off a m = false) : blockEmit d (Scanner.chunkRun (blockStep a b symB wrB d) cols off blockStart m) = true ↔ markCount cols off a m = 1 ∧ markCount cols off b m = 1 ∧ (∀ p < m, symOf cols off b p = wantSym cols off a wrB p ∧ (markOf cols off a p = true → symOf cols off a p = symB)) ∧ ∀ p < m, markOf cols off b p = movedMark cols off a d p

What the whole block check reports.

theorem Complexity.blockEmit_holds {j m : ℕ} [NeZero m] (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (a b : Fin (j + 1)) (hd hd' : Fin m) (cl cl' : Fin m → Γ) (ha : HoldsWindow cols off a hd cl) (hb : HoldsWindow cols off b hd' cl') (sym wr : Γ) (d : Dir3) (hm : 0 < m) (hend : markOf cols off a m = false) : blockEmit d (Scanner.chunkRun (blockStep a b (gammaBits sym) (gammaBits wr) d) cols off blockStart m) = true ↔ cl hd = sym ∧ (∀ (p : Fin m), cl' p = if p = hd ∧ 0 < ↑p then wr else cl p) ∧ ↑hd' = movedIdx d ↑hd

The block check, as a statement about decoded windows. The scan accepts exactly when the new window is the old one stepped: the symbol under the head is the one the transition was computed from, the cells are unchanged except under the head, where the written symbol appears — save at cell zero, where a write is a no-op — and the head has moved as the direction says.

The parameters a successor check is handed

The check does not guess what the simulated machine does — it guesses only what the machine sees, and computes the transition itself. The state is verified against the old code's state field, and each head symbol by the block check's own symOk conjunct, so nothing here is taken on trust.

structure Complexity.SuccParams (Q : Type) (k : ℕ) : Type

What the simulated machine sees at one step: its choice bit, its state, and the symbol under each of its heads.

• beta : Bool

  The nondeterministic choice.

• q : Q

  The state.

• inSym : Γ

  The symbol under the input head.

• wSym : Fin k → Γ

  The symbol under each work head.

• oSym : Γ

  The symbol under the output head.

def Complexity.succParamsEquiv (Q : Type) (k : ℕ) : SuccParams Q k ≃ Γ × Bool × Q × (Fin k → Γ) × Γ

SuccParams is a plain record, so it lays out as a product. The symbol under the input head comes first: it is the one field a machine checks against its own input tape rather than by scanning, and TM.inMatchTM reads the two cells at the start of the register.

Equations

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

noncomputable def Complexity.succParamsCodec (Q : Type) [Fintype Q] [Nonempty Q] (k : ℕ) : BitCodec (SuccParams Q k)

The layout of a parameter block.

Equations

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

theorem Complexity.succParamsCodec_width (Q : Type) [Fintype Q] [Nonempty Q] (k : ℕ) : (succParamsCodec Q k).width = 2 + (1 + (bitWidth (Fintype.card Q) + (k * 2 + 2)))

def Complexity.succTrans {k : ℕ} (tm : NTM k) (p : SuccParams tm.Q k) : tm.Q × (Fin k → Γw) × Γw × Dir3 × (Fin k → Dir3) × Dir3

What the simulated machine does, given what it sees.

Equations

• Complexity.succTrans tm p = tm.δ p.beta p.q p.inSym p.wSym p.oSym

def Complexity.succWrite {k : ℕ} (tm : NTM k) (p : SuccParams tm.Q k) (i : Fin k) : Γ

The symbol the simulated machine writes on work tape i.

Equations

• Complexity.succWrite tm p i = ((Complexity.succTrans tm p).2.1 i).toΓ

def Complexity.succDir {k : ℕ} (tm : NTM k) (p : SuccParams tm.Q k) (i : Fin k) : Dir3

Which way work head i moves.

Equations

• Complexity.succDir tm p i = (Complexity.succTrans tm p).2.2.2.2.1 i

def Complexity.succState {k : ℕ} (tm : NTM k) (p : SuccParams tm.Q k) : tm.Q

The state the simulated machine moves to.

Equations

• Complexity.succState tm p = (Complexity.succTrans tm p).1

What the successor relation on codes says

Complexity.NTM.codeSucc is cfgCode ∘ stepCfg ∘ decodeCfg. Decoding reads the transition's inputs straight off the code's fields, so a successor is determined by the code and the choice bit — which is what lets the check guess only what the machine sees.

def Complexity.inSymOf {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) : Γ

The symbol under the simulated input head.

Equations

• Complexity.inSymOf tm x S a = (Complexity.Tape.init (List.map Complexity.Γ.ofBool x)).cells ↑a.2.1

def Complexity.wSymOf {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (i : Fin k) : Γ

The symbol under simulated work head i.

Equations

• Complexity.wSymOf tm x S a i = (a.2.2.1 i).2 (a.2.2.1 i).1

def Complexity.oSymOf {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) : Γ

The symbol under the simulated output head.

Equations

• Complexity.oSymOf tm x S a = a.2.2.2.2 a.2.2.2.1

def Complexity.paramsOf {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (β : Bool) : SuccParams tm.Q k

What the simulated machine sees, read off a code.

Equations

• Complexity.paramsOf tm x S a β = { beta := β, q := a.1, inSym := Complexity.inSymOf tm x S a, wSym := Complexity.wSymOf tm x S a, oSym := Complexity.oSymOf tm x S a }

@[simp]

theorem Complexity.decodeCfg_state {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) : (decodeCfg x S a).state = a.1

theorem Complexity.decodeCfg_input_read {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) : (decodeCfg x S a).input.read = inSymOf tm x S a

theorem Complexity.decodeCfg_work_read {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (i : Fin k) : ((decodeCfg x S a).work i).read = wSymOf tm x S a i

theorem Complexity.decodeCfg_output_read {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) : (decodeCfg x S a).output.read = oSymOf tm x S a

theorem Complexity.stepCfg_decodeCfg_delta {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (β : Bool) : tm.δ β (decodeCfg x S a).state (decodeCfg x S a).input.read (fun (i : Fin k) => ((decodeCfg x S a).work i).read) (decodeCfg x S a).output.read = succTrans tm (paramsOf tm x S a β)

The transition a code and a choice bit determine.

def Complexity.succCode {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (β : Bool) (a : Code tm.Q k x.length S) : Code tm.Q k x.length S

The successor of a code under one choice.

Equations

• Complexity.succCode tm x S β a = Complexity.cfgCode x.length S (tm.stepCfg β (Complexity.decodeCfg x S a))

theorem Complexity.mem_codeSucc_iff {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a a' : Code tm.Q k x.length S) : a' ∈ tm.codeSucc x S a ↔ a.1 ≠ tm.qhalt ∧ ∃ (β : Bool), a' = succCode tm x S β a

Membership in codeSucc, unpacked.

theorem Complexity.head_move (t : Tape) (d : Dir3) : (t.move d).head = movedIdx d t.head

theorem Complexity.succCode_state {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (β : Bool) : (succCode tm x S β a).1 = succState tm (paramsOf tm x S a β)

The state of a successor.

theorem Complexity.succCode_inputHead {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (β : Bool) : ↑(succCode tm x S β a).2.1 = min (movedIdx (succTrans tm (paramsOf tm x S a β)).2.2.2.1 ↑a.2.1) (x.length + S + 1)

The input head of a successor.

theorem Complexity.succCode_work_head {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (β : Bool) (i : Fin k) : ↑((succCode tm x S β a).2.2.1 i).1 = min (movedIdx (succDir tm (paramsOf tm x S a β) i) ↑(a.2.2.1 i).1) S

The head of a successor's work window.

theorem Complexity.succCode_work_cells {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (β : Bool) (i : Fin k) (p : Fin (S + 1)) : ((succCode tm x S β a).2.2.1 i).2 p = if p = (a.2.2.1 i).1 ∧ 0 < ↑p then succWrite tm (paramsOf tm x S a β) i else (a.2.2.1 i).2 p

The cells of a successor's work window.

theorem Complexity.succCode_output_head {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (β : Bool) : ↑(succCode tm x S β a).2.2.2.1 = min (movedIdx (succTrans tm (paramsOf tm x S a β)).2.2.2.2.2 ↑a.2.2.2.1) (S + 1)

The head of a successor's output window.

theorem Complexity.succCode_output_cells {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (β : Bool) (p : Fin (S + 2)) : (succCode tm x S β a).2.2.2.2 p = if p = a.2.2.2.1 ∧ 0 < ↑p then (succTrans tm (paramsOf tm x S a β)).2.2.1.toΓ else a.2.2.2.2 p

The cells of a successor's output window.

theorem Complexity.eq_succCode_iff {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a a' : Code tm.Q k x.length S) (β : Bool) (hin : movedIdx (succTrans tm (paramsOf tm x S a β)).2.2.2.1 ↑a.2.1 ≤ x.length + S + 1) (hw : ∀ (i : Fin k), movedIdx (succDir tm (paramsOf tm x S a β) i) ↑(a.2.2.1 i).1 ≤ S) (ho : movedIdx (succTrans tm (paramsOf tm x S a β)).2.2.2.2.2 ↑a.2.2.2.1 ≤ S + 1) : a' = succCode tm x S β a ↔ a'.1 = succState tm (paramsOf tm x S a β) ∧ ↑a'.2.1 = movedIdx (succTrans tm (paramsOf tm x S a β)).2.2.2.1 ↑a.2.1 ∧ (∀ (i : Fin k), ↑(a'.2.2.1 i).1 = movedIdx (succDir tm (paramsOf tm x S a β) i) ↑(a.2.2.1 i).1 ∧ ∀ (p : Fin (S + 1)), (a'.2.2.1 i).2 p = if p = (a.2.2.1 i).1 ∧ 0 < ↑p then succWrite tm (paramsOf tm x S a β) i else (a.2.2.1 i).2 p) ∧ ↑a'.2.2.2.1 = movedIdx (succTrans tm (paramsOf tm x S a β)).2.2.2.2.2 ↑a.2.2.2.1 ∧ ∀ (p : Fin (S + 2)), a'.2.2.2.2 p = if p = a.2.2.2.1 ∧ 0 < ↑p then (succTrans tm (paramsOf tm x S a β)).2.2.1.toΓ else a.2.2.2.2 p

A successor, field by field. Under the space bound the clamps in cfgCode are inert, so a code is the successor of another exactly when every field is what the transition makes it — which is what the scans check.

theorem Complexity.params_eq {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a : Code tm.Q k x.length S) (P : SuccParams tm.Q k) (hq : a.1 = P.q) (hin : P.inSym = inSymOf tm x S a) (hwk : ∀ (i : Fin k), (a.2.2.1 i).2 (a.2.2.1 i).1 = P.wSym i) (hot : a.2.2.2.2 a.2.2.2.1 = P.oSym) : P = paramsOf tm x S a P.beta

The guessed parameters are forced. Each field of what the check was handed is pinned by one of the checks: the state by the comparison against the old code's state field, each head symbol by that block's own symOk conjunct, and the input symbol by the machine reading its own input head.

theorem Complexity.eq_succCode_of_checks {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a b : Code tm.Q k x.length S) (P : SuccParams tm.Q k) (β : Bool) (hbeta : P.beta = β) (hq : a.1 = P.q) (hin : P.inSym = inSymOf tm x S a) (hwsym : ∀ (i : Fin k), (a.2.2.1 i).2 (a.2.2.1 i).1 = P.wSym i) (hosym : a.2.2.2.2 a.2.2.2.1 = P.oSym) (hclampIn : movedIdx (succTrans tm P).2.2.2.1 ↑a.2.1 ≤ x.length + S + 1) (hclampW : ∀ (i : Fin k), movedIdx (succDir tm P i) ↑(a.2.2.1 i).1 ≤ S) (hclampO : movedIdx (succTrans tm P).2.2.2.2.2 ↑a.2.2.2.1 ≤ S + 1) : b = succCode tm x S β a ↔ b.1 = succState tm P ∧ ↑b.2.1 = movedIdx (succTrans tm P).2.2.2.1 ↑a.2.1 ∧ (∀ (i : Fin k), ↑(b.2.2.1 i).1 = movedIdx (succDir tm P i) ↑(a.2.2.1 i).1 ∧ ∀ (p : Fin (S + 1)), (b.2.2.1 i).2 p = if p = (a.2.2.1 i).1 ∧ 0 < ↑p then succWrite tm P i else (a.2.2.1 i).2 p) ∧ ↑b.2.2.2.1 = movedIdx (succTrans tm P).2.2.2.2.2 ↑a.2.2.2.1 ∧ ∀ (p : Fin (S + 2)), b.2.2.2.2 p = if p = a.2.2.2.1 ∧ 0 < ↑p then (succTrans tm P).2.2.1.toΓ else a.2.2.2.2 p

A successor, from the conditions the checks establish.

theorem Complexity.mem_codeSucc_of_checks {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a b : Code tm.Q k x.length S) (P : SuccParams tm.Q k) (hne : a.1 ≠ tm.qhalt) (hq : a.1 = P.q) (hin : P.inSym = inSymOf tm x S a) (hwsym : ∀ (i : Fin k), (a.2.2.1 i).2 (a.2.2.1 i).1 = P.wSym i) (hosym : a.2.2.2.2 a.2.2.2.1 = P.oSym) (hclampIn : movedIdx (succTrans tm P).2.2.2.1 ↑a.2.1 ≤ x.length + S + 1) (hclampW : ∀ (i : Fin k), movedIdx (succDir tm P i) ↑(a.2.2.1 i).1 ≤ S) (hclampO : movedIdx (succTrans tm P).2.2.2.2.2 ↑a.2.2.2.1 ≤ S + 1) (hstate : b.1 = succState tm P) (hhead : ↑b.2.1 = movedIdx (succTrans tm P).2.2.2.1 ↑a.2.1) (hwork : ∀ (i : Fin k), ↑(b.2.2.1 i).1 = movedIdx (succDir tm P i) ↑(a.2.2.1 i).1 ∧ ∀ (p : Fin (S + 1)), (b.2.2.1 i).2 p = if p = (a.2.2.1 i).1 ∧ 0 < ↑p then succWrite tm P i else (a.2.2.1 i).2 p) (hout : ↑b.2.2.2.1 = movedIdx (succTrans tm P).2.2.2.2.2 ↑a.2.2.2.1 ∧ ∀ (p : Fin (S + 2)), b.2.2.2.2 p = if p = a.2.2.2.1 ∧ 0 < ↑p then (succTrans tm P).2.2.1.toΓ else a.2.2.2.2 p) : b ∈ tm.codeSucc x S a

Membership in codeSucc, from the conditions the checks establish.