Bounded Turing-machine configurations in RAM registers

This module exposes the first representation layer of the Turing-machine to RAM simulation. The register layout is explicit, blank cells use value zero, and decode_encode states the exact condition under which bounded decoding loses no information.

@[simp]

theorem Complexity.RAM.TMConfig.fieldReg_state {n bound : ℕ} : fieldReg stateField = 0

The state field is register zero.

@[simp]

theorem Complexity.RAM.TMConfig.fieldReg_head {n bound : ℕ} (tape : Fin (n + 2)) : fieldReg (headField tape) = 1 + ↑tape

Head registers immediately follow the state, in input/work/output order.

@[simp]

theorem Complexity.RAM.TMConfig.fieldReg_cell {n bound : ℕ} (tape : Fin (n + 2)) (position : Fin (bound + 1)) : fieldReg (cellField tape position) = 1 + (n + 2) + ↑tape * (bound + 1) + ↑position

Cell blocks follow all head registers, ordered by tape and position.

theorem Complexity.RAM.TMConfig.symbolDecode_code (symbol : Γ) : symbolDecode (symbolCode symbol) = symbol

Symbol coding is lossless on the four-symbol tape alphabet.

theorem Complexity.RAM.TMConfig.stateDecode_code {n : ℕ} (tm : TM n) (state : tm.Q) : stateDecode tm (stateCode tm state) = state

Canonical finite-state coding is lossless.

theorem Complexity.RAM.TMConfig.encodeRegs_field {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (field : Field n bound) : encodeRegs tm bound cfg (fieldReg field) = fieldValue tm bound cfg field

Reading an encoded field returns exactly that field's value.

theorem Complexity.RAM.TMConfig.fieldReg_lt {n bound : ℕ} (field : Field n bound) : fieldReg field < registerCount n bound

Every field address lies inside the explicit configuration prefix.

theorem Complexity.RAM.TMConfig.fieldReg_injective {n bound : ℕ} : Function.Injective fieldReg

Distinct configuration fields occupy distinct registers.

theorem Complexity.RAM.TMConfig.Represents.update_outside {n : ℕ} {tm : TM n} {bound reg value : ℕ} {cfg : Complexity.Cfg n tm.Q} {regs : ℕ → ℕ} (hrepresents : Represents tm bound cfg regs) (hreg : registerCount n bound ≤ reg) : Represents tm bound cfg (Function.update regs reg value)

Updating a scratch register beyond the configuration prefix preserves every represented field.

theorem Complexity.RAM.TMConfig.encodeRegs_represents {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) : Represents tm bound cfg (encodeRegs tm bound cfg)

The canonical bounded encoding represents every one of its fields.

theorem Complexity.RAM.TMConfig.decode_of_represents {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (regs : ℕ → ℕ) (hrepresents : Represents tm bound cfg regs) (hbounded : Bounded cfg bound) : decode tm bound regs = cfg

Any representing store decodes to its configuration when the omitted tape suffixes are blank. Scratch registers do not affect decoding.

theorem Complexity.RAM.TMConfig.decode_encode {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (hbounded : Bounded cfg bound) : decode tm bound (encode tm bound cfg).regs = cfg

Decoding an encoded bounded configuration recovers it exactly.

theorem Complexity.RAM.TMConfig.encodeRegs_outside {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) {reg : ℕ} (hreg : registerCount n bound ≤ reg) : encodeRegs tm bound cfg reg = 0

Registers beyond the explicit bounded layout are zero.