A fixed sparse-RAM block for one Turing-machine transition

The generated program depends only on the Turing machine. Its interleaved layout computes cell addresses at runtime, so no tape or time bound is baked into the program. The exact address/loading layers, selected action, complete nested dispatch, fixed iteration controller, and transfer to concrete compiled RAM execution are checked. The separate Sparse.ABI surface supplies the public input/output marshalling layer.

theorem Complexity.RAM.TMConfig.Sparse.addressOps_correct {n : ℕ} {tm : TM n} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm cfg store) (tape : Fin (n + 2)) (htapeCount : store (tapeCountReg n) = n + 2) : have final := Structured.Basic.execList (addressOps n tape) store; Represents tm cfg final ∧ final (addressReg n) = cellReg n tape (tapeAt cfg tape).head

Computing a named tape's current-cell address preserves the represented configuration and returns the exact sparse cell register.

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

The fixed loading prelude preserves the complete sparse representation, initializes its constants, and recovers the state and every head symbol.

theorem Complexity.RAM.TMConfig.Sparse.actionOps_correct {n : ℕ} {tm : TM n} {cfg next : Complexity.Cfg n tm.Q} {store : Structured.Store} (hstep : tm.step cfg = some next) (hrepresents : Represents tm cfg store) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) (hone : store (oneReg n) = 1) (htapeCount : store (tapeCountReg n) = n + 2) : Represents tm next (Structured.Basic.execList (actionOps tm cfg.state (readSymbols cfg)) store)

Once the loaded finite state and symbols select an action, the fixed sparse operations represent the exact TM successor.

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

The fixed structured program, determined solely by tm, performs exactly one nonhalting TM transition with the advertised source instruction count.

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

The complete fixed source block decodes to the exact successor without a tape-window premise.

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

Exact transfer of the uniform one-step theorem to the concrete compiled RAM block, including the compiler's logarithmic cost and peak space.

theorem Complexity.RAM.TMConfig.Sparse.runUntilHalt_correct {n : ℕ} {tm : TM n} {steps : ℕ} {cfg halted : Complexity.Cfg n tm.Q} {store : Structured.Store} (hreach : tm.reachesIn steps cfg halted) (hhalted : tm.halted halted) (hrepresents : Represents tm cfg store) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (runUntilHalt tm) store final (runSteps tm steps cfg) cost space ∧ Represents tm halted final

The fixed loop controller follows any exact halting TM run and retains a complete representation of its halted configuration.

theorem Complexity.RAM.TMConfig.Sparse.runUntilHalt_decodes {n : ℕ} {tm : TM n} {steps : ℕ} {cfg halted : Complexity.Cfg n tm.Q} {store : Structured.Store} (hreach : tm.reachesIn steps cfg halted) (hhalted : tm.halted halted) (hrepresents : Represents tm cfg store) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (runUntilHalt tm) store final (runSteps tm steps cfg) cost space ∧ decode tm final = halted

The same fixed loop decodes to the exact halted TM configuration.

theorem Complexity.RAM.TMConfig.Sparse.compiledUntilHalt_correct {n : ℕ} {tm : TM n} {steps : ℕ} {cfg halted : Complexity.Cfg n tm.Q} {store : Structured.Store} (hreach : tm.reachesIn steps cfg halted) (hhalted : tm.halted halted) (hrepresents : Represents tm cfg store) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (runUntilHalt tm) store final (runSteps tm steps cfg) cost space ∧ run (compiledUntilHalt tm) (runSteps tm steps cfg) { pc := 0, regs := store } = { pc := (runUntilHalt tm).codeSize, regs := final } ∧ Halted (compiledUntilHalt tm) (run (compiledUntilHalt tm) (runSteps tm steps cfg) { pc := 0, regs := store }) ∧ logTimeUpto (compiledUntilHalt tm) (runSteps tm steps cfg) { pc := 0, regs := store } = cost ∧ spaceUpto (compiledUntilHalt tm) (runSteps tm steps cfg) { pc := 0, regs := store } = space ∧ decode tm final = halted

Exact compiled-RAM transfer for the complete fixed simulation loop.

theorem Complexity.RAM.TMConfig.Sparse.program_resourceBound {n : ℕ} {tm : TM n} {bound : ℕ} {cfg next : Complexity.Cfg n tm.Q} {store : Structured.Store} (hstep : tm.step cfg = some next) (hrepresents : Represents tm cfg store) (hheads : HeadsBounded cfg bound) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) (henvelope : StepEnvelope tm bound store) : ∃ (final : Structured.Store), Structured.Internal.MeasuredRuns (program tm) store final (stepCount tm cfg) (timeBound tm bound cfg) (spaceBound tm bound) ∧ Represents tm next final ∧ StepEnvelope tm bound final

Quantitative one-step theorem for the fixed sparse program. The exact source step count, logarithmic time, and peak sparse-store space are all checked against one explicit envelope.

theorem Complexity.RAM.TMConfig.Sparse.runUntilHalt_resourceBound {n : ℕ} {tm : TM n} {steps base : ℕ} {cfg halted : Complexity.Cfg n tm.Q} {store : Structured.Store} (hreach : tm.reachesIn steps cfg halted) (hhalted : tm.halted halted) (hrepresents : Represents tm cfg store) (hheads : HeadsBounded cfg base) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) (henvelope : StepEnvelope tm (base + steps) store) : ∃ (final : Structured.Store), Structured.Internal.MeasuredRuns (runUntilHalt tm) store final (runSteps tm steps cfg) (runTimeBound tm base steps cfg) (spaceBound tm (base + steps)) ∧ Represents tm halted final ∧ StepEnvelope tm (base + steps) final

Quantitative iteration theorem for the fixed sparse simulator. Starting with heads bounded by base, steps transitions fit one envelope at base + steps; costs compose into runTimeBound.

theorem Complexity.RAM.TMConfig.Sparse.runTimeBound_le_linear {n : ℕ} (tm : TM n) (base steps : ℕ) (cfg : Complexity.Cfg n tm.Q) : runTimeBound tm base steps cfg ≤ (steps + 1) * runFactor tm * wordWidth tm (base + steps)

The accumulated exact cost expression is linear in the number of simulated steps and logarithmic in the common sparse word bound.

theorem Complexity.RAM.TMConfig.Sparse.wordWidth_bigO_log {n : ℕ} (tm : TM n) : BigO (fun (bound : ℕ) => wordWidth tm bound) fun (bound : ℕ) => Nat.log 2 bound

Sparse word width is logarithmic in the head allowance; all dependence on the fixed machine is absorbed into the big-O constant.

theorem Complexity.RAM.TMConfig.Sparse.compiledUntilHalt_resourceBound {n : ℕ} {tm : TM n} {steps base : ℕ} {cfg halted : Complexity.Cfg n tm.Q} (hreach : tm.reachesIn steps cfg halted) (hhalted : tm.halted halted) (hbounded : Bounded cfg base) (hheads : HeadsBounded cfg base) (hworkStart : ∀ (i : Fin n), (cfg.work i).StartInvariant) (houtputStart : cfg.output.StartInvariant) : have store := encodeRegs tm cfg; ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (runUntilHalt tm) store final (runSteps tm steps cfg) cost space ∧ cost ≤ runTimeBound tm base steps cfg ∧ space ≤ spaceBound tm (base + steps) ∧ run (compiledUntilHalt tm) (runSteps tm steps cfg) { pc := 0, regs := store } = { pc := (runUntilHalt tm).codeSize, regs := final } ∧ Halted (compiledUntilHalt tm) (run (compiledUntilHalt tm) (runSteps tm steps cfg) { pc := 0, regs := store }) ∧ decode tm final = halted

Concrete compiled-RAM resource transfer from a canonical sparse encoding. This is the finite, directly checkable core of the forward containment: a steps-step halting TM run is simulated by one program depending only on tm, with the stated logarithmic time and sparse-store space bounds.