Documentation

Complexitylib.Models.TuringMachine.SingleTape.Internal

Single-tape simulation — encoding internals #

Foundations for NTM.singleTapeSim (see docs/A4-SingleTapeSimulation.md): the binary symbol codec and the block-index arithmetic for laying k work tapes onto one. These are path-independent: any single-work-tape encoding over the fixed alphabet Γ = {0,1,□,▷} needs a binary code (so that literal □ can serve as the end-of-used-region sentinel) and a per-position block layout. Proof internals only — correctness of the full simulation is established downstream.

Binary symbol codec #

A writable symbol Γw = {0,1,□} is stored in two cells over {0,1} (never □), so that a literal □ inside the used region is impossible and can mark its end. Code: □ ↦ 00, 0 ↦ 01, 1 ↦ 10.

def Complexity.NTM.SingleTape.encSym :

Γw → Γ × Γ

Encode a writable symbol as a 2-cell binary code.

Equations

Instances For

def Complexity.NTM.SingleTape.encSymW :

Γw → Γw × Γw

Encode a writable symbol into a 2-cell writable code (for SCATTER's symbol writes; agrees with encSym under Γw.toΓ, see encSymW_toΓ).

Equations

Instances For

def Complexity.NTM.SingleTape.decSym :

Γ → Γ → Γw

Decode a 2-cell code back to a writable symbol (any non-code pair ↦ □).

Equations

Instances For

theorem Complexity.NTM.SingleTape.encSymW_toΓ (s : Γw) :

((encSymW s).1.toΓ, (encSymW s).2.toΓ) = encSym s

The writable codec agrees with the Γ-valued one under Γw.toΓ.

@[simp]

theorem Complexity.NTM.SingleTape.decSym_encSym (s : Γw) :

decSym (encSym s).1 (encSym s).2 = s

The codec round-trips.

theorem Complexity.NTM.SingleTape.encSym_ne_blank (s : Γw) :

(encSym s).1 ≠ Γ.blank ∧ (encSym s).2 ≠ Γ.blank

No active code cell is □: encoded symbols use only {0,1}. This is what lets a literal □ mark the end of the used region.

theorem Complexity.NTM.SingleTape.encSym_ne_start (s : Γw) :

(encSym s).1 ≠ Γ.start ∧ (encSym s).2 ≠ Γ.start

An encoded code cell is never ▷ either, so the global ▷ at cell 0 stays unique within the work tape.

def Complexity.NTM.SingleTape.encSymΓ :

Γ → Γ × Γ

Codec on the full read alphabet Γ, used by the invariant (which ranges over work-tape cells of type Γ). ▷ ↦ 00 is junk: ▷ never occurs at a work-tape position ≥ 1, so the round-trip below excludes it.

Equations

Instances For

def Complexity.NTM.SingleTape.decSymΓ :

Γ → Γ → Γ

Decode a 2-cell code over Γ (any non-code pair ↦ □).

Equations

Instances For

theorem Complexity.NTM.SingleTape.decSymΓ_encSymΓ {s : Γ} (hs : s ≠ Γ.start) :

decSymΓ (encSymΓ s).1 (encSymΓ s).2 = s

The full-alphabet codec round-trips on every non-▷ symbol.

theorem Complexity.NTM.SingleTape.encSymΓ_toΓ (s : Γw) :

encSymΓ s.toΓ = encSym s

Bridge: encoding a writable symbol agrees with the full-alphabet codec on its image. Lets δ' write via encSym while the invariant reads encSymΓ.

theorem Complexity.NTM.SingleTape.encSymΓ_ne_start (s : Γ) :

(encSymΓ s).1 ≠ Γ.start ∧ (encSymΓ s).2 ≠ Γ.start

Both code cells are writable (≠ ▷), so encoding never introduces a second ▷ (holds even for the junk ▷ ↦ 00 case).

theorem Complexity.NTM.SingleTape.encSymΓ_ne_blank (s : Γ) :

(encSymΓ s).1 ≠ Γ.blank ∧ (encSymΓ s).2 ≠ Γ.blank

Neither code cell is □: codes use only {0,1}, so a literal □ can mark the end of the used region.

Block layout #

Position-major: super-position p ≥ 1 occupies a block of blockWidth k = 3*k cells starting at blockStart k p = 1 + (p-1)*3k. Within a block, tape j uses offsets 3j, 3j+1 (symbol code) and 3j+2 (head-present bit). Cell 0 is the global ▷.

def Complexity.NTM.SingleTape.blockWidth (k : ℕ) :

Cells per super-position block: 2 symbol cells + 1 head bit, per tape.

Equations

Complexity.NTM.SingleTape.blockWidth k = 3 * k

Instances For

def Complexity.NTM.SingleTape.blockStart (k p : ℕ) :

First cell of the block for super-position p ≥ 1.

Equations

Complexity.NTM.SingleTape.blockStart k p = 1 + (p - 1) * Complexity.NTM.SingleTape.blockWidth k

Instances For

@[simp]

theorem Complexity.NTM.SingleTape.blockStart_one (k : ℕ) :

blockStart k 1 = 1

The first super-position's block starts at cell 1, directly after the ▷.

theorem Complexity.NTM.SingleTape.blockStart_succ (k p : ℕ) (hp : 1 ≤ p) :

blockStart k (p + 1) = blockStart k p + blockWidth k

Consecutive blocks are exactly blockWidth k apart.

theorem Complexity.NTM.SingleTape.one_le_blockStart (k p : ℕ) :

1 ≤ blockStart k p

Blocks start at or after cell 1 (never the ▷ cell 0).

theorem Complexity.NTM.SingleTape.blockStart_lt_blockStart {k : ℕ} (hk : 1 ≤ k) {p q : ℕ} (hp : 1 ≤ p) (hpq : p < q) :

blockStart k p < blockStart k q

For positive width, block starts are strictly increasing in the position.

def Complexity.NTM.SingleTape.headBitCell (k p : ℕ) (j : Fin k) :

The cell holding tape j's head-present bit within block p (offset 0 of the triple: head-bit-first, so a sweep learns "head here" before passing the symbol cells).

Equations

Complexity.NTM.SingleTape.headBitCell k p j = Complexity.NTM.SingleTape.blockStart k p + 3 * ↑j

Instances For

def Complexity.NTM.SingleTape.symCell (k p : ℕ) (j : Fin k) :

The first (high) symbol cell of tape j within block p (offset 1; the low symbol cell is symCell + 1 at offset 2).

Equations

Complexity.NTM.SingleTape.symCell k p j = Complexity.NTM.SingleTape.blockStart k p + 3 * ↑j + 1

Instances For

theorem Complexity.NTM.SingleTape.headBitCell_lt_blockStart_succ (k p : ℕ) (j : Fin k) (hp : 1 ≤ p) :

headBitCell k p j < blockStart k (p + 1)

Within a block, tape j's three cells stay inside [blockStart, blockStart+3k).

theorem Complexity.NTM.SingleTape.blockStart_le (k : ℕ) {p q : ℕ} (hpq : p ≤ q) :

blockStart k p ≤ blockStart k q

Block starts are monotone (non-strict) in the position.

theorem Complexity.NTM.SingleTape.headBitCell_add_three_le_blockStart_succ (k p : ℕ) (j : Fin k) (hp : 1 ≤ p) :

headBitCell k p j + 3 ≤ blockStart k (p + 1)

Tape j's whole triple fits strictly before the next block: headBitCell + 3 ≤ blockStart (p+1) (the +2 cell is the last of the triple).

The simulation invariant #

SimInvAt k t w M asserts that the single work tape t encodes the k work tapes w, with the used region materialized up to super-position M (the maximum position any head has reached). This is the relation preserved by one simulated macro-step; the two behavioural lemmas of singleTapeSim follow from base case + preservation + iteration. See docs/A4-SingleTapeSimulation.md.

structure Complexity.NTM.SingleTape.SimInvAt (k : ℕ) (t : Tape) (w : Fin k → Tape) (M : ℕ) :

The single tape t encodes the k work tapes w, materialized up to M.

cell0 : t.cells 0 = Γ.start
Cell 0 is the global start marker ▷.
wfStart (j : Fin k) : (w j).cells 0 = Γ.start
Each encoded work tape has ▷ at its own cell 0.
noStart (j : Fin k) (p : ℕ) : 1 ≤ p → (w j).cells p ≠ Γ.start
No encoded work tape has ▷ at a position ≥ 1 (writes use Γw).
heads_le (j : Fin k) : (w j).head ≤ M
Every head is within the materialized region.
headBit (p : ℕ) : 1 ≤ p → p ≤ M → ∀ (j : Fin k), t.cells (headBitCell k p j) = if (w j).head = p then Γ.one else Γ.zero
Head-present bit at (p, j) is set iff tape j's head is at position p.
sym (p : ℕ) : 1 ≤ p → p ≤ M → ∀ (j : Fin k), t.cells (symCell k p j) = (encSymΓ ((w j).cells p)).1 ∧ t.cells (symCell k p j + 1) = (encSymΓ ((w j).cells p)).2
The two symbol cells at (p, j) hold the code of tape j's symbol at p.
sentinel (c : ℕ) : blockStart k (M + 1) ≤ c → t.cells c = Γ.blank
Everything from block M+1 onward is blank — the □ sentinel region.

Instances For

theorem Complexity.NTM.SingleTape.simInvAt_init (k : ℕ) :

SimInvAt k (Tape.init []) (fun (x : Fin k) => Tape.init []) 0

Base case. The initial single tape Tape.init [] encodes the initial k-tape configuration (all heads at 0, all blank), materialized to M = 0 (empty used region — the sentinel □ starts right at cell 1).

theorem Complexity.NTM.SingleTape.SimInvAt.cells_congr {k : ℕ} {t t' : Tape} {w : Fin k → Tape} {M : ℕ} (h : SimInvAt k t w M) (hc : t'.cells = t.cells) :

SimInvAt k t' w M

SimInvAt depends on the encoding tape only through its cells (never its head), so it transfers along any cell-preserving change (e.g. a head move).

theorem Complexity.NTM.SingleTape.SimInvAt.decSymΓ_symCell_head {k : ℕ} {t : Tape} {w : Fin k → Tape} {M : ℕ} (h : SimInvAt k t w M) (j : Fin k) (hp1 : 1 ≤ (w j).head) (hpM : (w j).head ≤ M) :

decSymΓ (t.cells (symCell k (w j).head j)) (t.cells (symCell k (w j).head j + 1)) = (w j).read

GATHER decode kernel (head off cell 0). When tape j's head is in the materialized region, decoding its two symbol cells recovers exactly the symbol under that head — what the sweep accumulates.

theorem Complexity.NTM.SingleTape.SimInvAt.read_eq_start_of_head_eq_zero {k : ℕ} {t : Tape} {w : Fin k → Tape} {M : ℕ} (h : SimInvAt k t w M) (j : Fin k) (h0 : (w j).head = 0) :

(w j).read = Γ.start

GATHER decode kernel (head on cell 0). A head at position 0 reads ▷; the sweep finds no marker for it and records ▷.

theorem Complexity.NTM.SingleTape.SimInvAt.materialized_ne_blank {k : ℕ} {t : Tape} {w : Fin k → Tape} {M : ℕ} (h : SimInvAt k t w M) {c : ℕ} (hc1 : 1 ≤ c) (hc2 : c < blockStart k (M + 1)) :

t.cells c ≠ Γ.blank

No □ inside the materialized region. Every cell strictly between the ▷ (cell 0) and the sentinel block is a code or head-bit cell, hence in {0,1} — so the first □ a rightward sweep meets is exactly the sentinel at blockStart k (M+1). (Holds vacuously for k = 0.)

theorem Complexity.NTM.SingleTape.SimInvAt.materialized_ne_start {k : ℕ} {t : Tape} {w : Fin k → Tape} {M : ℕ} (h : SimInvAt k t w M) {c : ℕ} (hc1 : 1 ≤ c) (hc2 : c < blockStart k (M + 1)) :

t.cells c ≠ Γ.start

No ▷ inside the materialized region. Every cell strictly between the ▷ (cell 0) and the sentinel block is a code or head-bit cell (in {0,1}), hence never ▷ — so ▷ uniquely marks cell 0. The REWIND sweep's precondition.