Fixed RAM transition blocks for bounded Turing-machine configurations

The public layer exposes the exact register layout, verified loading and action phases, and the composed nested state/symbol dispatcher. Thus the fixed structured program has exact one-step source semantics; its common resource envelope and compiled-RAM transfer are the next M6 layer.

theorem Complexity.RAM.TMConfig.Step.symbolCode_lt (symbol : Γ) : symbolCode symbol < 4

Every alphabet symbol is a valid four-way dispatch code.

theorem Complexity.RAM.TMConfig.Step.symbolAt_code (symbol : Γ) : symbolAt ⟨symbolCode symbol, ⋯⟩ = symbol

Dispatching on an encoded alphabet symbol recovers that symbol.

theorem Complexity.RAM.TMConfig.Step.stateCode_lt {n : ℕ} (tm : TM n) (state : tm.Q) : stateCode tm state < Fintype.card tm.Q

Every canonical state code is valid for the machine's finite state count.

theorem Complexity.RAM.TMConfig.Step.headReg_eq_fieldReg {n bound : ℕ} (tape : Fin (n + 2)) : headReg tape = fieldReg (headField tape)

The arithmetic head address agrees with the configuration-field layout.

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

A tape-block base plus an in-window position agrees with the corresponding configuration-field address.

theorem Complexity.RAM.TMConfig.Step.encodeRegs_storeBounded {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) (hheads : HeadsBounded cfg bound) : StoreBounded tm bound (encodeRegs tm bound cfg)

The canonical register encoding fits the one-step program's explicit store envelope whenever all represented heads lie in the chosen window.

theorem Complexity.RAM.TMConfig.Step.loadOps_correct {n : ℕ} {tm : TM n} {bound : ℕ} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm bound cfg store) (hheads : HeadsBounded cfg bound) : have final := Structured.Basic.execList (loadOps n bound) store; Represents tm bound cfg final ∧ final (zeroReg n bound) = 0 ∧ final (oneReg n bound) = 1 ∧ final (stateScratchReg n bound) = stateCode tm cfg.state ∧ ∀ (tape : Fin (n + 2)), final (symbolReg n bound tape) = symbolCode (readSymbols cfg tape)

The generated load block preserves the represented configuration and loads the state and every symbol needed by the finite transition dispatcher.

theorem Complexity.RAM.TMConfig.Step.actionOps_correct {n : ℕ} {tm : TM n} {bound : ℕ} {cfg next : Complexity.Cfg n tm.Q} {store : Structured.Store} (hstep : tm.step cfg = some next) (hrepresents : Represents tm bound cfg store) (hheads : HeadsBounded cfg bound) (hworkStart : ∀ (i : Fin n), (cfg.work i).cells 0 = Γ.start) (houtputStart : cfg.output.cells 0 = Γ.start) (hone : store (oneReg n bound) = 1) : Represents tm bound next (Structured.Basic.execList (actionOps tm bound cfg.state (readSymbols cfg)) store)

Once the state and head symbols select a concrete transition, its generated straight-line action maps any represented configuration to the exact TM successor. The assumptions are precisely those needed by the bounded tape layout: all heads are in range, writable tapes retain the left-end marker, and the loading phase has initialized the constant-one scratch register.

theorem Complexity.RAM.TMConfig.Step.program_correct {n : ℕ} {tm : TM n} {bound : ℕ} {cfg next : Complexity.Cfg n tm.Q} {store : Structured.Store} (hstep : tm.step cfg = some next) (hrepresents : Represents tm bound cfg store) (hwindow : WithinWindow cfg bound) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (program tm bound) store final (stepCount tm bound cfg) cost space ∧ Represents tm bound next final

The complete fixed structured program performs exactly one nonhalting TM transition. The source execution has the advertised exact instruction count and its final store represents the successor configuration.

theorem Complexity.RAM.TMConfig.Step.program_decodes {n : ℕ} {tm : TM n} {bound : ℕ} {cfg next : Complexity.Cfg n tm.Q} {store : Structured.Store} (hstep : tm.step cfg = some next) (hrepresents : Represents tm bound cfg store) (hwindow : WithinWindow cfg bound) (hnextBounded : Bounded next bound) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (program tm bound) store final (stepCount tm bound cfg) cost space ∧ decode tm bound final = next

If the successor also fits the chosen cell window, decoding the complete program's final store returns that successor exactly.

theorem Complexity.RAM.TMConfig.Step.program_performance {n : ℕ} {tm : TM n} {bound : ℕ} {cfg next : Complexity.Cfg n tm.Q} {store : Structured.Store} (hstep : tm.step cfg = some next) (hrepresents : Represents tm bound cfg store) (hwindow : WithinWindow cfg bound) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) (hstore : StoreBounded tm bound store) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (program tm bound) store final (stepCount tm bound cfg) cost space ∧ cost ≤ timeBound tm bound cfg ∧ space ≤ spaceBound tm bound ∧ Represents tm bound next final ∧ StoreBounded tm bound final

The complete one-step source block satisfies its exact transition count, explicit logarithmic-cost bound, and peak-space bound while preserving both the successor representation and the store envelope needed for composition.

theorem Complexity.RAM.TMConfig.Step.compiled_correct {n : ℕ} {tm : TM n} {bound : ℕ} {cfg next : Complexity.Cfg n tm.Q} {store : Structured.Store} (hstep : tm.step cfg = some next) (hrepresents : Represents tm bound cfg store) (hwindow : WithinWindow cfg bound) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) (hstore : StoreBounded tm bound store) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (program tm bound) store final (stepCount tm bound cfg) cost space ∧ run (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := store } = { pc := (program tm bound).codeSize, regs := final } ∧ Halted (compiled tm bound) (run (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := store }) ∧ logTimeUpto (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := store } ≤ timeBound tm bound cfg ∧ spaceUpto (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := store } ≤ spaceBound tm bound ∧ Represents tm bound next final ∧ StoreBounded tm bound final

End-to-end transfer of the measured source theorem to the concrete compiled RAM block. After the exact step count, the RAM is stopped at the compiler's terminal halt instruction with the successor represented in its registers.

theorem Complexity.RAM.TMConfig.Step.compiled_encode_decodes {n : ℕ} {tm : TM n} {bound : ℕ} {cfg next : Complexity.Cfg n tm.Q} (hstep : tm.step cfg = some next) (hwindow : WithinWindow cfg bound) (hnextBounded : Bounded next bound) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) : have initial := encodeRegs tm bound cfg; ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (program tm bound) initial final (stepCount tm bound cfg) cost space ∧ run (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := initial } = { pc := (program tm bound).codeSize, regs := final } ∧ Halted (compiled tm bound) (run (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := initial }) ∧ logTimeUpto (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := initial } ≤ timeBound tm bound cfg ∧ spaceUpto (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := initial } ≤ spaceBound tm bound ∧ decode tm bound (run (compiled tm bound) (stepCount tm bound cfg) { pc := 0, regs := initial }).regs = next

The canonical encoded configuration therefore runs through the concrete compiled block and decodes to the exact TM successor.