Generic proof tools for TM combinators

This file provides reusable proof infrastructure for TM combinator proofs, eliminating duplication across SeqInternal, IfInternal, LoopInternal, and ComplementInternal.

Main results

• reachesIn_map — generic simulation lifting: if a state embedding commutes with step, then reachesIn lifts through the embedding
• exists_reachesIn_of_rewindStep_tape — generic rewind loop for an arbitrary tape accessor: stepping from a "rewind state" moves the head left (preserving cells) until cell 0, then enters a "target state" at head 1
• exists_reachesIn_of_rewindStep_output — the same rewind loop specialized to the output tape
• exists_reachesIn_of_rewindStep_frame — the output-tape rewind loop, additionally proving the input and work tapes are unchanged
• transitionTape / transitionInput — the standard tape operations applied at combinator phase boundaries, with cell-preservation and head-bound lemmas (transitionTape_cells, transitionInput_cells, one_le_head_transitionTape, transitionInput_head_ge, head_transitionTape_le)
• transitionTape_eq_self / transitionInput_eq_self — frame rules: both operations are no-ops on tapes reading a non-▷ symbol

Shared tape stability lemmas

These lemmas were previously duplicated across multiple Internal files.

theorem Complexity.TM.toΓ_readBackWrite_of_ne_start {g : Γ} (h : g ≠ Γ.start) : (readBackWrite g).toΓ = g

readBackWrite recovers the original symbol for non-start symbols.

theorem Complexity.TM.tape_writeAndMove_stable (t : Tape) (hhead : t.head ≥ 1) (hns : ∀ j ≥ 1, t.cells j ≠ Γ.start) : t.writeAndMove (readBackWrite t.read).toΓ (idleDir t.read) = t

A tape with head ≥ 1 and cells ≥ 1 ≠ start is stable under writeAndMove(readBackWrite(read).toΓ, idleDir(read)).

theorem Complexity.TM.tape_move_idleDir_stable (t : Tape) (hhead : t.head ≥ 1) (hns : ∀ j ≥ 1, t.cells j ≠ Γ.start) : t.move (idleDir t.read) = t

A tape with head ≥ 1 and cells ≥ 1 ≠ start is stable under move(idleDir(read)).

theorem Complexity.TM.tape_readBackWrite_preserves (t : Tape) (d : Dir3) (h : t.head = 0 ∨ t.read ≠ Γ.start) : (t.writeAndMove (readBackWrite t.read).toΓ d).cells = t.cells

Helper: readBackWrite preserves tape cells when head = 0 or read ≠ start.

theorem Complexity.TM.reachesIn_map {n : ℕ} {tm tm' : TM n} (wrap : Cfg n tm.Q → Cfg n tm'.Q) (h_step : ∀ (c c' : Cfg n tm.Q), tm.step c = some c' → tm'.step (wrap c) = some (wrap c')) {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') : tm'.reachesIn t (wrap c) (wrap c')

If wrap commutes with step (i.e., one step of tm corresponds to one step of tm' through the embedding), then reachesIn lifts.

theorem Complexity.TM.exists_reachesIn_of_rewindStep_tape {n : ℕ} (tm : TM n) (tape : Cfg n tm.Q → Tape) {rewindState targetState : tm.Q} (h_step_left : ∀ (c : Cfg n tm.Q), c.state = rewindState → (tape c).read ≠ Γ.start → (tape c).cells 0 = Γ.start → (∀ j ≥ 1, (tape c).cells j ≠ Γ.start) → ∃ (c' : Cfg n tm.Q), tm.step c = some c' ∧ c'.state = rewindState ∧ (tape c').head = (tape c).head - 1 ∧ (tape c').cells = (tape c).cells) (h_step_base : ∀ (c : Cfg n tm.Q), c.state = rewindState → (tape c).read = Γ.start → (tape c).cells 0 = Γ.start → (∀ j ≥ 1, (tape c).cells j ≠ Γ.start) → ∃ (c' : Cfg n tm.Q), tm.step c = some c' ∧ c'.state = targetState ∧ (tape c').head = 1 ∧ (tape c').cells = (tape c).cells) (p : ℕ) (c : Cfg n tm.Q) : c.state = rewindState → (tape c).cells 0 = Γ.start → (∀ j ≥ 1, (tape c).cells j ≠ Γ.start) → (tape c).head = p → ∃ (c_target : Cfg n tm.Q), tm.reachesIn (p + 1) c c_target ∧ c_target.state = targetState ∧ (tape c_target).head = 1 ∧ (tape c_target).cells = (tape c).cells

Generic rewind loop (abstract tape accessor).

For any TM with a designated "rewind state" where stepping:

• At head > 0: stays in rewind, moves head left by 1, preserves cells
• At head = 0: enters target state, moves head to 1, preserves cells

Then from rewind state with tape head at p, the machine reaches the target state with tape head at 1 in exactly p + 1 steps.

The tape parameter selects which tape to track (output, work, etc.). This captures the common rewind pattern used in complementTM, ifTM, loopTM, writeTM, and rewindWorkTM.

theorem Complexity.TM.exists_reachesIn_of_rewindStep_output {n : ℕ} (tm : TM n) {rewindState targetState : tm.Q} (h_step_left : ∀ (c : Cfg n tm.Q), c.state = rewindState → c.output.read ≠ Γ.start → c.output.cells 0 = Γ.start → (∀ j ≥ 1, c.output.cells j ≠ Γ.start) → ∃ (c' : Cfg n tm.Q), tm.step c = some c' ∧ c'.state = rewindState ∧ c'.output.head = c.output.head - 1 ∧ c'.output.cells = c.output.cells) (h_step_base : ∀ (c : Cfg n tm.Q), c.state = rewindState → c.output.read = Γ.start → c.output.cells 0 = Γ.start → (∀ j ≥ 1, c.output.cells j ≠ Γ.start) → ∃ (c' : Cfg n tm.Q), tm.step c = some c' ∧ c'.state = targetState ∧ c'.output.head = 1 ∧ c'.output.cells = c.output.cells) (p : ℕ) (c : Cfg n tm.Q) : c.state = rewindState → c.output.cells 0 = Γ.start → (∀ j ≥ 1, c.output.cells j ≠ Γ.start) → c.output.head = p → ∃ (c_target : Cfg n tm.Q), tm.reachesIn (p + 1) c c_target ∧ c_target.state = targetState ∧ c_target.output.head = 1 ∧ c_target.output.cells = c.output.cells

Specialization of exists_reachesIn_of_rewindStep_tape for the output tape.

theorem Complexity.TM.exists_reachesIn_of_rewindStep_frame {n : ℕ} (tm : TM n) {rewindState targetState : tm.Q} (h_step_left : ∀ (c : Cfg n tm.Q), c.state = rewindState → c.output.read ≠ Γ.start → c.output.cells 0 = Γ.start → (∀ j ≥ 1, c.output.cells j ≠ Γ.start) → c.input.head ≥ 1 → (∀ j ≥ 1, c.input.cells j ≠ Γ.start) → (∀ (i : Fin n), (c.work i).head ≥ 1) → (∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) → ∃ (c' : Cfg n tm.Q), tm.step c = some c' ∧ c'.state = rewindState ∧ c'.output.head = c.output.head - 1 ∧ c'.output.cells = c.output.cells ∧ c'.input = c.input ∧ c'.work = c.work) (h_step_base : ∀ (c : Cfg n tm.Q), c.state = rewindState → c.output.read = Γ.start → c.output.cells 0 = Γ.start → (∀ j ≥ 1, c.output.cells j ≠ Γ.start) → c.input.head ≥ 1 → (∀ j ≥ 1, c.input.cells j ≠ Γ.start) → (∀ (i : Fin n), (c.work i).head ≥ 1) → (∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) → ∃ (c' : Cfg n tm.Q), tm.step c = some c' ∧ c'.state = targetState ∧ c'.output.head = 1 ∧ c'.output.cells = c.output.cells ∧ c'.input = c.input ∧ c'.work = c.work) (p : ℕ) (c : Cfg n tm.Q) : c.state = rewindState → c.output.cells 0 = Γ.start → (∀ j ≥ 1, c.output.cells j ≠ Γ.start) → c.output.head = p → c.input.head ≥ 1 → (∀ j ≥ 1, c.input.cells j ≠ Γ.start) → (∀ (i : Fin n), (c.work i).head ≥ 1) → (∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) → ∃ (c_target : Cfg n tm.Q), tm.reachesIn (p + 1) c c_target ∧ c_target.state = targetState ∧ c_target.output.head = 1 ∧ c_target.output.cells = c.output.cells ∧ c_target.input = c.input ∧ c_target.work = c.work

Generic rewind loop (full tape tracking).

Same as exists_reachesIn_of_rewindStep_output, but the step hypotheses also guarantee that input and work tapes are preserved (given stability conditions: head ≥ 1 and cells ≥ 1 ≠ start). The conclusion additionally proves c_target.input = c.input and c_target.work = c.work.

def Complexity.TM.transitionTape (t : Tape) : Tape

The standard tape transformation applied at combinator phase boundaries (work tapes and output tape). Writes back the current symbol (preserving cells) and stays in place; if at cell 0, δ_right_of_start forces a right move to cell 1.

Used by all combinators (seqTM, ifTM, loopTM, complementTM) at transitions between phases.

Equations

• Complexity.TM.transitionTape t = t.writeAndMove (Complexity.TM.readBackWrite t.read).toΓ (Complexity.TM.idleDir t.read)

def Complexity.TM.transitionInput (t : Tape) : Tape

The standard input-tape transformation at combinator phase boundaries. The input tape is read-only (no write), so only the head moves: stay in place unless at cell 0, where δ_right_of_start forces right.

Equations

• Complexity.TM.transitionInput t = t.move (Complexity.TM.idleDir t.read)

theorem Complexity.TM.transitionTape_cells (t : Tape) (hns : ∀ j ≥ 1, t.cells j ≠ Γ.start) : (transitionTape t).cells = t.cells

transitionTape preserves cells when cells ≥ 1 ≠ start.

theorem Complexity.TM.transitionInput_cells (t : Tape) : (transitionInput t).cells = t.cells

transitionInput preserves cells (always, since input has no write).

theorem Complexity.TM.one_le_head_transitionTape (t : Tape) (h0 : t.cells 0 = Γ.start) : (transitionTape t).head ≥ 1

After transitionTape, head ≥ 1 when cell 0 = start.

theorem Complexity.TM.transitionInput_head_ge (t : Tape) (h0 : t.cells 0 = Γ.start) : (transitionInput t).head ≥ 1

After transitionInput, head ≥ 1 when cell 0 = start.

theorem Complexity.TM.head_transitionTape_le {t : Tape} {p_bound : ℕ} (hcell0 : t.cells 0 = Γ.start) (hhead : t.head ≤ p_bound) : (transitionTape t).head ≤ p_bound + 1

Bound on transitionTape output head: ≤ original head + 1.

theorem Complexity.TM.transitionTape_eq_self {t : Tape} (hread : t.read ≠ Γ.start) : transitionTape t = t

Frame rule: transitionTape is the identity when the tape reads a non-▷ symbol. This is the key lemma for threading invariants through seqTM / loopTM / ifTM composition: tapes that are "stable" (head not at cell 0) pass through phase transitions unchanged.

theorem Complexity.TM.transitionInput_eq_self {t : Tape} (hread : t.read ≠ Γ.start) : transitionInput t = t

Frame rule: transitionInput is the identity when the tape reads a non-▷ symbol.