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.

theorem Turing.MultiInputTM.configs_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) (t : ℕ) : configs (Cfg.congrState e cfg) t = Cfg.congrState e (configs cfg t)

The configuration sequence commutes with state relabeling.

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

theorem Turing.MultiInputTM.outputSymbol_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) : outputSymbol (Cfg.congrState e cfg) = outputSymbol cfg

The emitted symbol is unchanged by state relabeling.

theorem Turing.MultiInputTM.outputString_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) (t : ℕ) : (congrState e tm).outputString (Cfg.congrState e cfg) t = tm.outputString cfg t

The output string is unchanged by state relabeling.

theorem Turing.MultiInputTM.spaceUsed_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) (t : ℕ) : spaceUsed (Cfg.congrState e cfg) t = spaceUsed cfg t

The space usage is unchanged by state relabeling.

theorem Turing.MultiInputTM.computesInTimeAndSpace_congrState {i w : ℕ} {State : Type u_1} {State' : Type u_2} {Symbol : Type u_3} (e : State ≃ State') (tm : MultiInputTM i w Symbol State) (input : Fin i → List Symbol) (output : List Symbol) (t s : ℕ) (h : tm.ComputesInTimeAndSpace input output t s) : (congrState e tm).ComputesInTimeAndSpace input output t s

Relabeling the state type preserves computations: the relabeled machine computes the same input/output pairs in the same time and space.

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)

theorem Turing.MultiInputTM.Cfg.congrSymbol_inputSymbols {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).inputSymbols = fun (j : Fin i) => 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.

theorem Turing.MultiInputTM.moveInputPos_cast {n m : ℕ} (h : n + 2 = m + 2) (pos : Fin (n + 2)) (mv : SignType) : MultiTapeTM.moveInputPos (Fin.cast h pos) mv = Fin.cast h (MultiTapeTM.moveInputPos pos mv)

Moving an input head commutes with transporting the position along an equal tape length.

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

The step function commutes with symbol relabeling.

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

The configuration sequence commutes with symbol relabeling.

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

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

The emitted symbol is relabeled along with the machine.

theorem Turing.MultiInputTM.outputString_congrSymbol {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} {input : Fin i → List Symbol} (e : Symbol ≃ Symbol') (tm : MultiInputTM i w Symbol State) (cfg : Cfg i w Symbol State input) (t : ℕ) : (congrSymbol e tm).outputString (Cfg.congrSymbol e cfg) t = List.map (⇑e) (tm.outputString cfg t)

The output string is relabeled along with the machine.

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

The space usage is unchanged by symbol relabeling.

theorem Turing.MultiInputTM.computesInTimeAndSpace_congrSymbol {i w : ℕ} {State : Type u_1} {Symbol : Type u_3} {Symbol' : Type u_4} (e : Symbol ≃ Symbol') (tm : MultiInputTM i w Symbol State) (input : Fin i → List Symbol) (output : List Symbol) (t s : ℕ) (h : tm.ComputesInTimeAndSpace input output t s) : (congrSymbol e tm).ComputesInTimeAndSpace (fun (j : Fin i) => List.map (⇑e) (input j)) (List.map (⇑e) output) t s

Relabeling the tape alphabet transports computations: the relabeled machine computes the relabeled input/output pairs in the same time and space.