Relabeling multi-input machines along equivalences

Relabeling the state type or the tape alphabet of a machine does not change its behaviour: MultiInputTM.congrState and MultiInputTM.congrSymbol transport machines, configurations, runs, outputs, space usage and ComputesInTimeAndSpace along State ≃ State' and Symbol ≃ Symbol'. This is the canonicalization glue between machines over arbitrary (finite) types and the Fin-typed shape of coded machines (MIPRE.TM.Code.Semantics): coded machines are born over Fin, and outside results about machines over other types meet them through these lemmas.

Adapted to the multi-input model from Regular.lean on the finite_in_fin branch of Christian Reitwiessner's CSLib fork (https://github.com/crei/cslib, branch tip 4a149e205c99d4636d3a421c8cf3526e47b00f16, 2026-07-19; Apache 2.0), which develops the same API for the one-input MultiTapeTM of an earlier model revision (its configurations still carry an output field, so the file predates upstream #745 and cannot be vendored against the current model). Two deliberate changes besides the multi-input generalization:

• congrState relabels along an equivalence, not an embedding: the fork's embedding-plus-Function.invFun version is noncomputable, and its only use instantiates with an equivalence anyway. Everything here is executable (planning/tm-infrastructure.md, decision D5).
• The fork's DFA simulation and regular-language results are deliberately not ported; they concern the one-input model and can be revisited when CSLib is un-vendored.

Relabeling the state type

None of the dependent structure of a configuration (inputs, head positions, work tapes) mentions the state type, so this direction is straightforward.

def Turing.MultiInputTM.Cfg.congrState {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input : Fin i → List Symbol} (e : State ≃ State') (cfg : Cfg i w Symbol State input) : Cfg i w Symbol State' input

Relabel the state of a configuration along e : State ≃ State'.

Equations

• Turing.MultiInputTM.Cfg.congrState e cfg = { state := Option.map (⇑e) cfg.state, inputPos := cfg.inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos }

@[simp]

theorem Turing.MultiInputTM.Cfg.congrState_state {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input : Fin i → List Symbol} (e : State ≃ State') (cfg : Cfg i w Symbol State input) : (congrState e cfg).state = Option.map (⇑e) cfg.state

@[simp]

theorem Turing.MultiInputTM.Cfg.congrState_inputPos {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input : Fin i → List Symbol} (e : State ≃ State') (cfg : Cfg i w Symbol State input) : (congrState e cfg).inputPos = cfg.inputPos

@[simp]

theorem Turing.MultiInputTM.Cfg.congrState_workTapes {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input : Fin i → List Symbol} (e : State ≃ State') (cfg : Cfg i w Symbol State input) : (congrState e cfg).workTapes = cfg.workTapes

@[simp]

theorem Turing.MultiInputTM.Cfg.congrState_workTapePos {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input : Fin i → List Symbol} (e : State ≃ State') (cfg : Cfg i w Symbol State input) : (congrState e cfg).workTapePos = cfg.workTapePos

@[simp]

theorem Turing.MultiInputTM.Cfg.congrState_inputSymbols {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input : Fin i → List Symbol} (e : State ≃ State') (cfg : Cfg i w Symbol State input) : (congrState e cfg).inputSymbols = cfg.inputSymbols

@[simp]

theorem Turing.MultiInputTM.Cfg.congrState_workTapeSymbols {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input : Fin i → List Symbol} (e : State ≃ State') (cfg : Cfg i w Symbol State input) : (congrState e cfg).workTapeSymbols = cfg.workTapeSymbols

def Turing.MultiInputTM.congrState {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} (e : State ≃ State') (tm : MultiInputTM i w Symbol State) : MultiInputTM i w Symbol State'

Relabel the state type of a machine along an equivalence e : State ≃ State'.

Equations

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

@[simp]

theorem Turing.MultiInputTM.step_congrState {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} {input : Fin i → List Symbol} (e : State ≃ State') (tm : MultiInputTM i w Symbol State) (cfg : Cfg i w Symbol State input) : step (Cfg.congrState e cfg) = Cfg.congrState e (step cfg)

The step function commutes with state relabeling.

Relabeling the symbol type

This direction touches the dependent structure of a configuration: each input head position lives in Fin ((input j).length + 2), so mapping the inputs transports the positions along List.length_map via Fin.cast.

def Turing.MultiInputTM.Cfg.congrSymbol {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} {input : Fin i → List Symbol} (e : Symbol ≃ Symbol') (cfg : Cfg i w Symbol State input) : Cfg i w Symbol' State fun (j : Fin i) => List.map (⇑e) (input j)

Relabel the symbols of a configuration along e : Symbol ≃ Symbol'.

Equations

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

@[simp]

theorem Turing.MultiInputTM.Cfg.congrSymbol_state {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} {input : Fin i → List Symbol} (e : Symbol ≃ Symbol') (cfg : Cfg i w Symbol State input) : (congrSymbol e cfg).state = cfg.state

@[simp]

theorem Turing.MultiInputTM.Cfg.congrSymbol_workTapePos {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} {input : Fin i → List Symbol} (e : Symbol ≃ Symbol') (cfg : Cfg i w Symbol State input) : (congrSymbol e cfg).workTapePos = cfg.workTapePos

@[simp]

theorem Turing.MultiInputTM.Cfg.congrSymbol_inputPos_val {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} {input : Fin i → List Symbol} (e : Symbol ≃ Symbol') (cfg : Cfg i w Symbol State input) (j : Fin i) : ↑((congrSymbol e cfg).inputPos j) = ↑(cfg.inputPos j)

@[simp]

theorem Turing.MultiInputTM.Cfg.congrSymbol_workTapeSymbols {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} {input : Fin i → List Symbol} (e : Symbol ≃ Symbol') (cfg : Cfg i w Symbol State input) (d : Fin w) : (congrSymbol e cfg).workTapeSymbols d = Option.map (⇑e) (cfg.workTapeSymbols d)

@[simp]

theorem Turing.MultiInputTM.Cfg.congrSymbol_inputSymbol {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} {input : Fin i → List Symbol} (e : Symbol ≃ Symbol') (cfg : Cfg i w Symbol State input) (j : Fin i) : (congrSymbol e cfg).inputSymbol j = Option.map (⇑e) (cfg.inputSymbol j)

def Turing.MultiInputTM.congrSymbol {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} (e : Symbol ≃ Symbol') (tm : MultiInputTM i w Symbol State) : MultiInputTM i w Symbol' State

Relabel the tape alphabet of a machine along an equivalence e : Symbol ≃ Symbol'.

Equations

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