Virtual tapes: the +1 shift representation

The δ_right_of_start discipline forces every head reading ▷ to move right on every step, so a simulated head resting at cell 0 cannot be shadowed at the same position across many UTM steps. Instead the universal machine stores each simulated tape shifted one cell right on one of its own work tapes:

• simulated cell j lives at UTM cell j + 1;
• UTM cell 1 is permanently □ (it shadows the simulated ▷, which cannot be written);
• simulated head p is shadowed at UTM head p + 1 ≥ 1 — never on ▷, hence stable across steps and phase transitions.

Under this shift the one-sided tape dynamics correspond exactly:

• a simulated right/left/stay move is the same physical move one cell up (left moves from simulated position 0 never occur in sanitized dynamics);
• a simulated write at position p ≥ 1 is the same write at p + 1;
• a simulated write at position 0 is a structural no-op, shadowed by writing □ over the permanent □ at UTM cell 1;
• "simulated head on ▷" ⟺ "UTM head at cell 1", detectable by a left-peek.

Main definitions

• VShift sim utm — the shift correspondence
• Tape.StartInvariant — cell 0 is ▷ and nowhere else (preserved by all writes)

Main results

• VShift.read_eq / VShift.read_blank — reads under the shift
• VShift.writeAndMove — one full simulated tape action corresponds
• VShift.init — the initial correspondence

def Complexity.Tape.HoldsExact (t : Tape) (syms : List Γw) : Prop

The tape holds exactly syms after ▷: cell i+1 is syms[i] for i < |syms| and □ beyond. Used for the UTM's state, description, and scratch tapes, whose contents are fully determined.

Equations

• t.HoldsExact syms = (t.cells 0 = Complexity.Γ.start ∧ ∀ (i : ℕ), t.cells (i + 1) = if h : i < syms.length then syms[i].toΓ else Complexity.Γ.blank)

theorem Complexity.Tape.HoldsExact.startInvariant {t : Tape} {syms : List Γw} (h : t.HoldsExact syms) : t.StartInvariant

theorem Complexity.Tape.HoldsExact.cells_lt {t : Tape} {syms : List Γw} (h : t.HoldsExact syms) {i : ℕ} (hi : i < syms.length) : t.cells (i + 1) = syms[i].toΓ

Cells within the contents.

theorem Complexity.Tape.HoldsExact.cells_ge {t : Tape} {syms : List Γw} (h : t.HoldsExact syms) {i : ℕ} (hi : syms.length ≤ i) : t.cells (i + 1) = Γ.blank

Cells beyond the contents are blank.

theorem Complexity.Tape.HoldsExact.nil_iff {t : Tape} : t.HoldsExact [] ↔ t.cells 0 = Γ.start ∧ ∀ (i : ℕ), t.cells (i + 1) = Γ.blank

The all-blank (cleared) tape characterization.

theorem Complexity.Tape.HoldsExact.init_nil : (init []).HoldsExact []

A freshly initialized (empty) tape holds [].

def Complexity.TM.VShift (sim utm : Tape) : Prop

The shift correspondence: utm stores sim shifted one cell right, with □ shadowing the simulated ▷ at UTM cell 1, and the head one cell up.

Equations

• Complexity.TM.VShift sim utm = ((utm.cells = fun (k : ℕ) => if k = 0 then Complexity.Γ.start else if k = 1 then Complexity.Γ.blank else sim.cells (k - 1)) ∧ utm.head = sim.head + 1)

theorem Complexity.TM.VShift.head_eq {sim utm : Tape} (h : VShift sim utm) : utm.head = sim.head + 1

theorem Complexity.TM.VShift.head_pos {sim utm : Tape} (h : VShift sim utm) : 1 ≤ utm.head

theorem Complexity.TM.VShift.read_eq {sim utm : Tape} (h : VShift sim utm) (hp : 1 ≤ sim.head) : utm.read = sim.read

Away from the simulated origin, the shadow reads the simulated symbol.

theorem Complexity.TM.VShift.read_blank {sim utm : Tape} (h : VShift sim utm) (hp : sim.head = 0) : utm.read = Γ.blank

At the simulated origin, the shadow reads the permanent □.

theorem Complexity.TM.VShift.read_ne_start {sim utm : Tape} (h : VShift sim utm) (hsim : sim.StartInvariant) : utm.read ≠ Γ.start

The shadow never reads ▷ (given the simulated tape is well-formed).

theorem Complexity.TM.VShift.startInvariant {sim utm : Tape} (h : VShift sim utm) (hsim : sim.StartInvariant) : utm.StartInvariant

The shadow's cells beyond 1 never hold ▷ (given the simulated tape is well-formed).

theorem Complexity.TM.VShift.move {sim utm : Tape} (h : VShift sim utm) (d : Dir3) (hd : sim.head = 0 → d = Dir3.right) : VShift (sim.move d) (utm.move d)

Moves correspond, provided a left move never happens at the simulated origin (sanitized dynamics guarantee this).

theorem Complexity.TM.VShift.write {sim utm : Tape} (h : VShift sim utm) (s : Γw) (hp : 1 ≤ sim.head) : VShift (sim.write s.toΓ) (utm.write s.toΓ)

Writes away from the simulated origin correspond.

theorem Complexity.TM.VShift.write_origin {sim utm : Tape} (h : VShift sim utm) (hp : sim.head = 0) : VShift sim (utm.write Γ.blank)

A simulated write at the origin is a no-op; the shadow writes □ over the permanent □ at cell 1 — also a no-op on cells.

theorem Complexity.TM.VShift.writeAndMove {sim utm : Tape} (h : VShift sim utm) (s : Γw) (d : Dir3) (hd : sim.head = 0 → d = Dir3.right) : VShift (sim.writeAndMove s.toΓ d) (utm.writeAndMove (if sim.head = 0 then Γ.blank else s.toΓ) d)

One full simulated tape action corresponds: writing s and moving d on the simulated tape is shadowed by writing if at-origin then □ else s and moving d, provided the sanitized direction discipline (▷ ⇒ right) holds.

theorem Complexity.TM.VShift.init (l : List Γ) : VShift (Tape.init l) { head := 1, cells := fun (k : ℕ) => if k = 0 then Γ.start else if k = 1 then Γ.blank else l[k - 2]?.getD Γ.blank }

The initial correspondence: the simulated initial tape (contents l) is shadowed by ▷ □ l ⋯ with head at cell 1.