Encoding machine configurations as bitstrings — proof internals

The completeness direction of Cobham's theorem simulates a polynomial-time machine inside the function algebra, so a configuration has to become a single bitstring. This module fixes that encoding and proves the arithmetic facts about it; the algebra-side operations that act on it live in Complexitylib.Classes.P.Cobham.Internal.StepAlgebra.

The two design choices

Two bits per symbol, with blank = 00. Fixed-width blocks are padded with zeros (Complexity.padTo), so making blank the all-zero code means padding a tape block with zeros is extending it with blanks — the padding needs no special treatment anywhere.

Tapes split at the head. A tape is stored as its cells to the left of the head, nearest first, and its cells from the head rightwards. Then a head move is transferring one symbol between the two sides, i.e. a take/drop/append of two bits, rather than arithmetic on a position index. Reading is the first two bits of the right part.

Cell 0 is the only ▷ (the writable alphabet Γw excludes it), so "the head is at cell 0" is exactly "the read symbol is ▷" — and in that case TM.δ_right_of_start forces a move right. The left part is therefore never consulted when it is empty, which is why it needs no emptiness test.

Main definitions

• Complexity.Cobham.symCode — two-bit code for Γ
• Complexity.Cobham.cellsCode — a window of cells as a bitstring
• Complexity.Cobham.leftCode, Complexity.Cobham.rightCode — a tape split at its head

Main results

The six lemmas that make the split representation simulate Tape.writeAndMove, each expressing one head move as two bits crossing the split:

• leftCode_write_stay, rightCode_write_stay
• leftCode_write_right, rightCode_write_right
• leftCode_write_left, rightCode_write_left

Every right-hand side is built from take 2, drop 2, ++ and the constant symCode s — all of which the algebra has (Cobham.takeFn, Cobham.dropFn, Cobham.appendFn, Cobham.const).

The symbol code

def Complexity.Cobham.symCode : Γ → List Bool

Two-bit code for the tape alphabet. Blank is 00, so zero-padding a block is blank-padding it.

Equations

• Complexity.Cobham.symCode Complexity.Γ.blank = [false, false]
• Complexity.Cobham.symCode Complexity.Γ.start = [false, true]
• Complexity.Cobham.symCode Complexity.Γ.zero = [true, false]
• Complexity.Cobham.symCode Complexity.Γ.one = [true, true]

def Complexity.Cobham.symDecode : List Bool → Γ

Decode the leading two bits of a string as a tape symbol; anything shorter than two bits reads as blank.

Equations

• Complexity.Cobham.symDecode (false :: false :: tail) = Complexity.Γ.blank
• Complexity.Cobham.symDecode (false :: true :: tail) = Complexity.Γ.start
• Complexity.Cobham.symDecode (true :: false :: tail) = Complexity.Γ.zero
• Complexity.Cobham.symDecode (true :: true :: tail) = Complexity.Γ.one
• Complexity.Cobham.symDecode x✝ = Complexity.Γ.blank

@[simp]

theorem Complexity.Cobham.symCode_length (g : Γ) : (symCode g).length = 2

@[simp]

theorem Complexity.Cobham.symCode_blank : symCode Γ.blank = [false, false]

@[simp]

theorem Complexity.Cobham.symDecode_symCode (g : Γ) (rest : List Bool) : symDecode (symCode g ++ rest) = g

The code round-trips, even with arbitrary trailing bits — which is what lets the decoder read a symbol off the front of a longer block.

theorem Complexity.Cobham.symDecode_take_two (l : List Bool) : symDecode (List.take 2 l) = symDecode l

The decoder only ever looks at two bits, so truncating first changes nothing.

theorem Complexity.Cobham.symDecode_replicate_false {n : ℕ} (h : 2 ≤ n) : symDecode (List.replicate n false) = Γ.blank

Zero padding decodes as blank: the reason symCode Γ.blank = [0,0].

theorem Complexity.Cobham.symCode_injective : Function.Injective symCode

The code is injective.

The control state

The state is stored one-hot: |Q| bits with a single 1. Fixed width and injective, and — the point — every state's code is a constant for a fixed machine, so the transition table is finitely many Cobham.matchPrefixFn tests against constants (Cobham.tableFn). Binary would need arithmetic; one-hot needs none.

noncomputable def Complexity.Cobham.stateCode {Q : Type} [Fintype Q] [DecidableEq Q] (q : Q) : List Bool

One-hot code for a control state: one bit per element of Q, set exactly at the state itself.

Noncomputable only because Finset.toList picks an enumeration order; the code appears solely in specifications, never in a machine that must run.

Equations

• Complexity.Cobham.stateCode q = List.map (fun (p : Q) => decide (p = q)) Finset.univ.toList

@[simp]

theorem Complexity.Cobham.stateCode_length {Q : Type} [Fintype Q] [DecidableEq Q] (q : Q) : (stateCode q).length = Fintype.card Q

theorem Complexity.Cobham.stateCode_injective {Q : Type} [Fintype Q] [DecidableEq Q] : Function.Injective stateCode

Distinct states get distinct codes.

Windows of cells

def Complexity.Cobham.cellsCode (t : Tape) (i w : ℕ) : List Bool

The w cells of t starting at cell i, two bits each.

Equations

• Complexity.Cobham.cellsCode t i w = List.flatMap (fun (j : ℕ) => Complexity.Cobham.symCode (t.cells (i + j))) (List.range w)

@[simp]

theorem Complexity.Cobham.cellsCode_zero (t : Tape) (i : ℕ) : cellsCode t i 0 = []

@[simp]

theorem Complexity.Cobham.cellsCode_length (t : Tape) (i w : ℕ) : (cellsCode t i w).length = 2 * w

theorem Complexity.Cobham.cellsCode_succ_left (t : Tape) (i w : ℕ) : cellsCode t i (w + 1) = symCode (t.cells i) ++ cellsCode t (i + 1) w

Peeling the first cell off a window.

Tapes split at the head

def Complexity.Cobham.leftCodeFrom (t : Tape) : ℕ → List Bool

The cells n-1, n-2, …, 0 of t, nearest first.

Equations

• Complexity.Cobham.leftCodeFrom t 0 = []
• Complexity.Cobham.leftCodeFrom t n.succ = Complexity.Cobham.symCode (t.cells n) ++ Complexity.Cobham.leftCodeFrom t n

def Complexity.Cobham.leftCode (t : Tape) : List Bool

The cells strictly left of the head, nearest first.

Equations

• Complexity.Cobham.leftCode t = Complexity.Cobham.leftCodeFrom t t.head

@[simp]

theorem Complexity.Cobham.leftCodeFrom_zero (t : Tape) : leftCodeFrom t 0 = []

@[simp]

theorem Complexity.Cobham.leftCodeFrom_succ (t : Tape) (n : ℕ) : leftCodeFrom t (n + 1) = symCode (t.cells n) ++ leftCodeFrom t n

@[simp]

theorem Complexity.Cobham.leftCodeFrom_length (t : Tape) (n : ℕ) : (leftCodeFrom t n).length = 2 * n

theorem Complexity.Cobham.leftCodeFrom_congr {t t' : Tape} {n : ℕ} (h : ∀ j < n, t.cells j = t'.cells j) : leftCodeFrom t n = leftCodeFrom t' n

The nearest-left window depends only on the cells it covers.

def Complexity.Cobham.rightCode (t : Tape) (W : ℕ) : List Bool

The cells from the head rightwards, out to cell W.

The width is W + 1 - head, complementary to leftCode's head, so the two parts always account for exactly the cells 0 … W: their total width is the constant 2 · (W + 1) and a head move just shifts two bits across the split.

Equations

• Complexity.Cobham.rightCode t W = Complexity.Cobham.cellsCode t t.head (W + 1 - t.head)

@[simp]

theorem Complexity.Cobham.leftCode_length (t : Tape) : (leftCode t).length = 2 * t.head

@[simp]

theorem Complexity.Cobham.rightCode_length (t : Tape) (W : ℕ) : (rightCode t W).length = 2 * (W + 1 - t.head)

theorem Complexity.Cobham.leftCode_rightCode_length (t : Tape) {W : ℕ} (h : t.head ≤ W + 1) : (leftCode t).length + (rightCode t W).length = 2 * (W + 1)

The two halves together always span the same window.

theorem Complexity.Cobham.symDecode_rightCode (t : Tape) {W : ℕ} (hw : t.head ≤ W) : symDecode (rightCode t W) = t.read

The read symbol is the first two bits of the right part.

Congruence

Both halves read only the cells in their own window, so an update outside that window is invisible to them. These are the lemmas that let a single-cell write be localized.

theorem Complexity.Cobham.cellsCode_congr {t t' : Tape} {i w : ℕ} (h : ∀ j < w, t.cells (i + j) = t'.cells (i + j)) : cellsCode t i w = cellsCode t' i w

A window depends only on the cells it covers.

theorem Complexity.Cobham.leftCode_congr {t t' : Tape} (hh : t.head = t'.head) (h : ∀ j < t.head, t.cells j = t'.cells j) : leftCode t = leftCode t'

The left half depends only on the head and the cells strictly below it.

Writing and moving

Tape.write never touches cell 0 (the model makes writing there a no-op), and Γw cannot produce ▷, so cell 0 is permanently the unique ▷. Hence "the head is at 0" is exactly "the read symbol is ▷", and TM.δ_right_of_start then forces a right move — which is why the left half is never consulted while empty.

theorem Complexity.Cobham.write_cells_of_ne {t : Tape} {s : Γ} {j : ℕ} (h : j ≠ t.head) : (t.write s).cells j = t.cells j

Writing at the head leaves every other cell alone.

theorem Complexity.Cobham.write_cells_head {t : Tape} {s : Γ} (hs : t.head = 0 → s = t.cells t.head) : (t.write s).cells t.head = s

Writing at the head sets exactly that cell — except at cell 0, where the model makes the write a no-op, so callers must establish that the modeled symbol already agrees with what is there. A raw TM transition writes only Γw, which excludes ▷; the encoded simulator later supplies the corrected symbol through correctWrite.

theorem Complexity.Cobham.write_cells_self {t : Tape} {s : Γ} (h : t.head ≠ 0) : (t.write s).cells t.head = s

Writing at the head sets exactly that cell, away from cell 0.

theorem Complexity.Cobham.leftCode_write_stay {t : Tape} {s : Γ} : leftCode ((t.write s).move Dir3.stay) = leftCode t

Staying put: the left half is untouched and the right half gets its leading symbol replaced.

theorem Complexity.Cobham.leftCode_write_right {t : Tape} {s : Γ} (h : t.head = 0 → s = t.cells t.head) : leftCode ((t.write s).move Dir3.right) = symCode s ++ leftCode t

Moving right: the written symbol crosses over to the left half. This is the one direction a head at cell 0 can take, so it is stated with the weaker hypothesis that the write agrees with cell 0 when the head is there.

theorem Complexity.Cobham.leftCode_write_left {t : Tape} {s : Γ} (h : t.head ≠ 0) : leftCode ((t.write s).move Dir3.left) = List.drop 2 (leftCode t)

Moving left: the nearest left symbol crosses over to the right half, so the left half loses its first two bits.

theorem Complexity.Cobham.rightCode_write_stay {t : Tape} {s : Γ} {W : ℕ} (h : t.head ≠ 0) (hW : t.head ≤ W) : rightCode ((t.write s).move Dir3.stay) W = symCode s ++ List.drop 2 (rightCode t W)

Staying put, right half: the leading symbol is replaced.

theorem Complexity.Cobham.rightCode_write_right {t : Tape} {s : Γ} {W : ℕ} (hW : t.head ≤ W) : rightCode ((t.write s).move Dir3.right) W = List.drop 2 (rightCode t W)

Moving right, right half: the leading symbol is consumed.

theorem Complexity.Cobham.rightCode_write_left {t : Tape} {s : Γ} {W : ℕ} (h : t.head ≠ 0) (hW : t.head ≤ W) : rightCode ((t.write s).move Dir3.left) W = List.take 2 (leftCode t) ++ symCode s ++ List.drop 2 (rightCode t W)

Moving left, right half: the nearest left symbol and the written symbol both join it.

Whole configurations

Every field occupies a block of the same width, so field i is recovered by Cobham.blockFn … i — the algebra never needs a self-delimiting decoder. A tape costs two blocks (its two halves); the state costs one, padded to the same width.

def Complexity.Cobham.blockWidth (W : ℕ) : ℕ

The block width used throughout: wide enough for either half of a tape whose head stays within 0 … W.

Equations

• Complexity.Cobham.blockWidth W = 2 * (W + 1)

def Complexity.Cobham.blockRuler (W : ℕ) : List Bool

The canonical ruler of one block's width.

Equations

• Complexity.Cobham.blockRuler W = List.replicate (Complexity.Cobham.blockWidth W) false

@[simp]

theorem Complexity.Cobham.blockRuler_length (W : ℕ) : (blockRuler W).length = blockWidth W

def Complexity.Cobham.tapeBlocks (W : ℕ) (t : Tape) : List (List Bool)

A tape as two padded half-blocks: the cells left of the head (nearest first) and the cells from the head rightwards.

Equations

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

theorem Complexity.Cobham.tapeBlocks_width (W : ℕ) (t : Tape) (b : List Bool) : b ∈ tapeBlocks W t → b.length = (blockRuler W).length

Both halves of a tape occupy one block each.

@[simp]

theorem Complexity.Cobham.tapeBlocks_length (W : ℕ) (t : Tape) : (tapeBlocks W t).length = 2

def Complexity.Cobham.tapeCode (W : ℕ) (t : Tape) : List Bool

A tape as a bitstring: its two half-blocks concatenated.

Equations

• Complexity.Cobham.tapeCode W t = (Complexity.Cobham.tapeBlocks W t).flatten

@[simp]

theorem Complexity.Cobham.tapeCode_length (W : ℕ) (t : Tape) : (tapeCode W t).length = 2 * blockWidth W

def Complexity.Cobham.worksCode {k : ℕ} (W : ℕ) (work : Fin k → Tape) : List Bool

The work tapes, one after another.

Equations

• Complexity.Cobham.worksCode W work = List.flatMap (fun (i : Fin k) => Complexity.Cobham.tapeCode W (work i)) (List.finRange k)

@[simp]

theorem Complexity.Cobham.worksCode_length {k : ℕ} (W : ℕ) (work : Fin k → Tape) : (worksCode W work).length = k * (2 * blockWidth W)

The window invariant

A head moves at most one cell per step and starts at cell 0, so after t steps every head is within 0 … t. Taking the window W to be the machine's time bound therefore discharges the head ≤ W side condition of every encoding lemma — the simulated machine can never reach outside the encoded window.

theorem Complexity.Cobham.heads_le_of_reachesIn {k : ℕ} (tm : TM k) {x : List Bool} {t : ℕ} {c : Cfg k tm.Q} (h : tm.reachesIn t (tm.initCfg x) c) : c.input.head ≤ t ∧ c.output.head ≤ t ∧ ∀ (i : Fin k), (c.work i).head ≤ t

After t steps from the initial configuration every head is at most t.

theorem Complexity.Cobham.symDecode_take_padTo_rightCode {W : ℕ} (t : Tape) (hW : t.head ≤ W) : symDecode (List.take 2 (padTo (blockRuler W) (rightCode t W))) = t.read

Reading a symbol out of an encoded tape. The head symbol is the first two bits of the padded right half-block — one takeFn in the algebra.

One tape's step

The encoded step on a tape's two half-blocks. Every right-hand side is take 2 / drop 2 / ++ / a constant and a re-pad, so the algebra realizes it with Cobham.takeFn, Cobham.dropFn, Cobham.appendFn, Cobham.const and Cobham.padFn — and within one branch of Cobham.tableFn the symbol s and the direction d are constants.

def Complexity.Cobham.tapeStepBlocks (R : List Bool) (s : Γ) (d : Dir3) (L Rt : List Bool) : List Bool × List Bool

The two half-blocks of a tape after writing s and moving d.

Equations

• Complexity.Cobham.tapeStepBlocks R s Complexity.Dir3.stay L Rt = (L, Complexity.padTo R (Complexity.Cobham.symCode s ++ List.drop 2 Rt))
• Complexity.Cobham.tapeStepBlocks R s Complexity.Dir3.right L Rt = (Complexity.padTo R (Complexity.Cobham.symCode s ++ L), Complexity.padTo R (List.drop 2 Rt))
• Complexity.Cobham.tapeStepBlocks R s Complexity.Dir3.left L Rt = (Complexity.padTo R (List.drop 2 L), Complexity.padTo R (List.take 2 L ++ Complexity.Cobham.symCode s ++ List.drop 2 Rt))

theorem Complexity.Cobham.tapeStepBlocks_eq {W : ℕ} (t : Tape) (s : Γ) (d : Dir3) (hs : t.head = 0 → s = t.cells t.head) (hne : d ≠ Dir3.right → t.head ≠ 0) (hW : t.head ≤ W) : tapeStepBlocks (blockRuler W) s d (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W)) = (padTo (blockRuler W) (leftCode ((t.write s).move d)), padTo (blockRuler W) (rightCode ((t.write s).move d) W))

The encoded step simulates Tape.writeAndMove on both half-blocks.

The hypotheses are exactly what the corrected encoded action supplies. hs: at cell 0 the write is a no-op, so correctWrite replaces the raw Γw symbol by the existing ▷. hne: TM.δ_right_of_start ensures that a head at cell 0 can only move right, so the stay and left cases never arise there.

All the tapes at once

TM.step writes and moves on every tape independently, so the encoded step is the same operation applied tapewise. Treating the tapes as one list — input, output, then work tapes, the order the encoding uses — makes that a List.zipWith against the transition's per-tape actions, with no positional index arithmetic.

theorem Complexity.Cobham.write_read_self (t : Tape) : t.write t.read = t

Writing back the symbol already under the head changes nothing. This is what lets the read-only input tape take part in the uniform tapewise step: its action is "write what you read, then move".

def Complexity.Cobham.cfgTapes {k : ℕ} {Q : Type} (c : Cfg k Q) : List Tape

All of a configuration's tapes in encoding order.

Equations

• Complexity.Cobham.cfgTapes c = c.input :: c.output :: List.ofFn c.work

@[simp]

theorem Complexity.Cobham.cfgTapes_length {k : ℕ} {Q : Type} (c : Cfg k Q) : (cfgTapes c).length = k + 2

The transition key

The transition function is indexed by the current state together with the symbol under every head. Packing those into one string turns the whole finite case analysis into Cobham.tableFn: each (state, symbols) combination is a constant pattern, and there are finitely many of them for a fixed machine.

noncomputable def Complexity.Cobham.keyCode {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (c : Cfg k Q) : List Bool

The state and the symbols under every head, in tape order.

Equations

• Complexity.Cobham.keyCode c = Complexity.Cobham.stateCode c.state ++ List.flatMap (fun (t : Complexity.Tape) => Complexity.Cobham.symCode t.read) (Complexity.Cobham.cfgTapes c)

@[simp]

theorem Complexity.Cobham.keyCode_length {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (c : Cfg k Q) : (keyCode c).length = Fintype.card Q + 2 * (k + 2)

theorem Complexity.Cobham.take_rightCode (t : Tape) {W : ℕ} (hW : t.head ≤ W) : List.take 2 (rightCode t W) = symCode t.read

The first two bits of a tape's right half-block are its read symbol.

def Complexity.Cobham.tapesBlocks (W : ℕ) (ts : List Tape) : List (List Bool)

The blocks of a list of tapes: two per tape.

Equations

• Complexity.Cobham.tapesBlocks W ts = List.flatMap (Complexity.Cobham.tapeBlocks W) ts

@[simp]

theorem Complexity.Cobham.tapesBlocks_length (W : ℕ) (ts : List Tape) : (tapesBlocks W ts).length = 2 * ts.length

def Complexity.Cobham.tapesStep (acts : List (Γ × Dir3)) (ts : List Tape) : List Tape

The tapes after one step, given each tape's write and move.

Equations

• Complexity.Cobham.tapesStep acts ts = List.zipWith (fun (a : Complexity.Γ × Complexity.Dir3) (t : Complexity.Tape) => (t.write a.1).move a.2) acts ts

def Complexity.Cobham.correctWriteSym (r s : Γ) : Γ

The write a transition really performs: at cell 0 the model makes the write a no-op, and this records that. Under Tape.StartInvariant the test is on the read symbol, which the transition table already branches on — so the correction costs the algebra nothing, it just picks a different constant in the ▷ branch.

Equations

• Complexity.Cobham.correctWriteSym r s = if r = Complexity.Γ.start then Complexity.Γ.start else s

def Complexity.Cobham.correctWrite (t : Tape) (s : Γ) : Γ

The corrected write on a tape — a function of its read symbol alone, which is what puts it inside the transition key.

Equations

• Complexity.Cobham.correctWrite t s = Complexity.Cobham.correctWriteSym t.read s

theorem Complexity.Cobham.write_correctWrite {t : Tape} (s : Γ) (h : t.StartInvariant) : t.write (correctWrite t s) = t.write s

Correcting the write does not change what the write does.

theorem Complexity.Cobham.correctWrite_at_zero {t : Tape} (s : Γ) (h : t.StartInvariant) (hh : t.head = 0) : correctWrite t s = t.cells t.head

Under the invariant, the corrected write agrees with cell 0 when the head is there — the hypothesis tapeStepBlocks_eq needs.

def Complexity.Cobham.stepActs {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) : List (Γ × Dir3)

The per-tape (write, move) actions a transition prescribes, in encoding order. The input tape's "write" is the symbol it just read, which by write_read_self leaves it unchanged — so the read-only input tape fits the uniform tapewise step with no special case.

Equations

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

The transition key determines the step

Everything the successor configuration depends on — the new state and every tape's write and direction — is a function of the state together with the symbol under each head. That is exactly what a Cobham.tableFn entry can be indexed by, and it is why any entry matching a configuration's key carries the right branch.

def Complexity.Cobham.cfgReads {k : ℕ} {Q : Type} (c : Cfg k Q) : Fin (k + 2) → Γ

The symbols under a configuration's heads, in cfgTapes order.

Equations

• Complexity.Cobham.cfgReads c = Fin.cons c.input.read (Fin.cons c.output.read fun (i : Fin k) => (c.work i).read)

noncomputable def Complexity.Cobham.keyPattern {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (p : Q × (Fin (k + 2) → Γ)) : List Bool

A transition key's pattern string: the state's one-hot code followed by the symbol under each head. Constant for each key, so it is what a Cobham.tableFn entry matches against.

Equations

• Complexity.Cobham.keyPattern p = Complexity.Cobham.stateCode p.1 ++ List.flatMap Complexity.Cobham.symCode (List.ofFn p.2)

@[simp]

theorem Complexity.Cobham.keyPattern_length {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (p : Q × (Fin (k + 2) → Γ)) : (keyPattern p).length = Fintype.card Q + 2 * (k + 2)

theorem Complexity.Cobham.keyPattern_injective {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] : Function.Injective keyPattern

Distinct keys get distinct patterns. Together with the fact that all patterns have the same length, this is what makes at most one table entry match a given key.

theorem Complexity.Cobham.cfgTapes_map_read {k : ℕ} {Q : Type} (c : Cfg k Q) : List.map Tape.read (cfgTapes c) = List.ofFn (cfgReads c)

The tapes' read symbols, listed, are the configuration's read tuple.

theorem Complexity.Cobham.keyCode_eq {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (c : Cfg k Q) : keyCode c = keyPattern (c.state, cfgReads c)

A configuration's key is its key's pattern. So the table entry indexed by (state, reads) is the one that matches.

def Complexity.Cobham.stepActsOf {k : ℕ} (tm : TM k) (q : tm.Q) (syms : Fin (k + 2) → Γ) : List (Γ × Dir3)

The per-tape actions determined by a transition key.

Equations

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

def Complexity.Cobham.stepStateOf {k : ℕ} (tm : TM k) (q : tm.Q) (syms : Fin (k + 2) → Γ) : tm.Q

The successor state determined by a transition key.

Equations

• Complexity.Cobham.stepStateOf tm q syms = (tm.δ q (syms 0) (fun (i : Fin k) => syms i.succ.succ) (syms 1)).1

theorem Complexity.Cobham.stepActs_eq_stepActsOf {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) : stepActs tm c = stepActsOf tm c.state (cfgReads c)

The actions a configuration prescribes are the ones its key prescribes.

theorem Complexity.Cobham.step_state_eq {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} (h : tm.step c = some c') : c'.state = stepStateOf tm c.state (cfgReads c)

The successor state is the one the key prescribes.

theorem Complexity.Cobham.cfgTapes_step {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} (h : tm.step c = some c') (hout : c.output.StartInvariant) (hwork : ∀ (i : Fin k), (c.work i).StartInvariant) : cfgTapes c' = tapesStep (stepActs tm c) (cfgTapes c)

TM.step is the tapewise action. Every tape writes and moves according to stepActs, so the whole configuration's tapes step uniformly.

theorem Complexity.Cobham.tapeBlocks_step {W : ℕ} (a : Γ × Dir3) (t : Tape) (hs : t.head = 0 → a.1 = t.cells t.head) (hne : a.2 ≠ Dir3.right → t.head ≠ 0) (hW : t.head ≤ W) : tapeBlocks W ((t.write a.1).move a.2) = [(tapeStepBlocks (blockRuler W) a.1 a.2 (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W))).1, (tapeStepBlocks (blockRuler W) a.1 a.2 (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W))).2]

One tape's blocks after a step. Immediate from tapeStepBlocks_eq; this is the form that lifts tapewise across a whole configuration.

theorem Complexity.Cobham.tapesBlocks_tapesStep {W : ℕ} (acts : List (Γ × Dir3)) (ts : List Tape) : List.Forall₂ (fun (a : Γ × Dir3) (t : Tape) => (t.head = 0 → a.1 = t.cells t.head) ∧ (a.2 ≠ Dir3.right → t.head ≠ 0) ∧ t.head ≤ W) acts ts → tapesBlocks W (tapesStep acts ts) = (List.zipWith (fun (a : Γ × Dir3) (t : Tape) => [(tapeStepBlocks (blockRuler W) a.1 a.2 (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W))).1, (tapeStepBlocks (blockRuler W) a.1 a.2 (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W))).2]) acts ts).flatten

The tapewise step acts blockwise on the encoding.

noncomputable def Complexity.Cobham.cfgBlocks {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : List (List Bool)

A whole configuration as a list of equal-width blocks: the one-hot state padded to a block, then the input tape, the output tape, and the work tapes, each as two half-blocks.

Equations

• Complexity.Cobham.cfgBlocks W c = Complexity.padTo (Complexity.Cobham.blockRuler W) (Complexity.Cobham.stateCode c.state) :: Complexity.Cobham.tapesBlocks W (Complexity.Cobham.cfgTapes c)

theorem Complexity.Cobham.cfgBlocks_eq {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : cfgBlocks W c = padTo (blockRuler W) (stateCode c.state) :: tapesBlocks W (cfgTapes c)

theorem Complexity.Cobham.cfgBlocks_width {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) (b : List Bool) : b ∈ cfgBlocks W c → b.length = (blockRuler W).length

Every field of a configuration occupies exactly one block.

noncomputable def Complexity.Cobham.cfgCode {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : List Bool

A whole configuration as a bitstring.

Equations

• Complexity.Cobham.cfgCode W c = (Complexity.Cobham.cfgBlocks W c).flatten

theorem Complexity.Cobham.blockAt_cfgCode {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) (i : ℕ) (hi : i < (cfgBlocks W c).length) : blockAt (blockRuler W) (cfgCode W c) i = (cfgBlocks W c)[i]

Field access. Block i of an encoded configuration is field i — so Cobham.blockFn … i reads it, and no self-delimiting decoder is ever needed.

@[simp]

theorem Complexity.Cobham.cfgBlocks_length {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : (cfgBlocks W c).length = 2 * (k + 2) + 1

A configuration has 2(k+2) + 1 blocks: one per tape half plus the state.

theorem Complexity.Cobham.cfgBlocks_step {k : ℕ} (tm : TM k) {c c' : Cfg k tm.Q} {W : ℕ} (h : tm.step c = some c') (hout : c.output.StartInvariant) (hwork : ∀ (i : Fin k), (c.work i).StartInvariant) (hgood : List.Forall₂ (fun (a : Γ × Dir3) (t : Tape) => (t.head = 0 → a.1 = t.cells t.head) ∧ (a.2 ≠ Dir3.right → t.head ≠ 0) ∧ t.head ≤ W) (stepActs tm c) (cfgTapes c)) : cfgBlocks W c' = padTo (blockRuler W) (stateCode c'.state) :: (List.zipWith (fun (a : Γ × Dir3) (t : Tape) => [(tapeStepBlocks (blockRuler W) a.1 a.2 (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W))).1, (tapeStepBlocks (blockRuler W) a.1 a.2 (padTo (blockRuler W) (leftCode t)) (padTo (blockRuler W) (rightCode t W))).2]) (stepActs tm c) (cfgTapes c)).flatten

The encoded configuration steps blockwise. Composing cfgTapes_step (TM.step is the tapewise action) with tapesBlocks_tapesStep (that action is blockwise on the encoding): the successor's blocks are the new state block followed by the old blocks transformed two at a time by tapeStepBlocks.

The Forall₂ hypothesis pairs each tape with its own action, which is what a run supplies: δ_right_of_start constrains a tape at cell 0 only through its own transition entry.

theorem Complexity.Cobham.stepActs_forall₂ {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) {W : ℕ} (hinv : ∀ t ∈ cfgTapes c, t.StartInvariant) (hW : ∀ t ∈ cfgTapes c, t.head ≤ W) : List.Forall₂ (fun (a : Γ × Dir3) (t : Tape) => (t.head = 0 → a.1 = t.cells t.head) ∧ (a.2 ≠ Dir3.right → t.head ≠ 0) ∧ t.head ≤ W) (stepActs tm c) (cfgTapes c)

The step's side conditions hold in any run. The write-agreement at cell 0 is correctWrite_at_zero, and "a head at cell 0 can only move right" is exactly TM.δ_right_of_start read through the invariant: at cell 0 the tape reads ▷, which is the hypothesis that rule fires on.

theorem Complexity.Cobham.getElem?_tapesBlocks (W : ℕ) (ts : List Tape) (j : ℕ) : (tapesBlocks W ts)[2 * j]? = Option.map (fun (t : Tape) => padTo (blockRuler W) (leftCode t)) ts[j]? ∧ (tapesBlocks W ts)[2 * j + 1]? = Option.map (fun (t : Tape) => padTo (blockRuler W) (rightCode t W)) ts[j]?

Tape j lives in blocks 2j and 2j+1 of the tape-block list. Combined with the state block at the front of cfgBlocks, tape j of a configuration occupies blocks 2j+1 and 2j+2 — which is how Cobham.blockFn addresses them.

Field accessors

The first three blocks — the state and the input tape's two halves — read out directly. Each is one Cobham.blockFn on the algebra side.

theorem Complexity.Cobham.blockAt_cfgCode_state {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : blockAt (blockRuler W) (cfgCode W c) 0 = padTo (blockRuler W) (stateCode c.state)

Block 0 holds the state.

theorem Complexity.Cobham.state_of_cfgCode {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) (hW : Fintype.card Q ≤ blockWidth W) : List.take (Fintype.card Q) (blockAt (blockRuler W) (cfgCode W c) 0) = stateCode c.state

Unpadding block 0 recovers the one-hot state code, which the transition table then matches against its finitely many constants.

theorem Complexity.Cobham.blockAt_cfgCode_inputLeft {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : blockAt (blockRuler W) (cfgCode W c) 1 = padTo (blockRuler W) (leftCode c.input)

Block 1 is the input tape's left half.

theorem Complexity.Cobham.blockAt_cfgCode_inputRight {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) : blockAt (blockRuler W) (cfgCode W c) 2 = padTo (blockRuler W) (rightCode c.input W)

Block 2 is the input tape's right half — the one the read symbol comes from.

theorem Complexity.Cobham.inputRead_of_cfgCode {k : ℕ} {Q : Type} [Fintype Q] [DecidableEq Q] (W : ℕ) (c : Cfg k Q) (hW : c.input.head ≤ W) : symDecode (List.take 2 (blockAt (blockRuler W) (cfgCode W c) 2)) = c.input.read

The input head's symbol, read straight out of the encoding.