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

The finite transition function is compiled as a decision tree. The program first loads the symbols under all named heads, dispatches on the finite-state code and the n + 2 four-symbol codes, then performs the selected transition using indirect stores into the bounded tape blocks.

The construction is fixed once tm and the cell-window bound are fixed. It does not install or consult an untrusted transition-table oracle.

def Complexity.RAM.TMConfig.Step.inputTape (n : ℕ) : Fin (n + 2)

Input tape index.

Equations

• Complexity.RAM.TMConfig.Step.inputTape n = ⟨0, ⋯⟩

def Complexity.RAM.TMConfig.Step.workTape {n : ℕ} (i : Fin n) : Fin (n + 2)

Work-tape index in the named input/work/output order.

Equations

• Complexity.RAM.TMConfig.Step.workTape i = ⟨↑i + 1, ⋯⟩

def Complexity.RAM.TMConfig.Step.outputTape (n : ℕ) : Fin (n + 2)

Output tape index.

Equations

• Complexity.RAM.TMConfig.Step.outputTape n = ⟨n + 1, ⋯⟩

def Complexity.RAM.TMConfig.Step.headReg {n : ℕ} (tape : Fin (n + 2)) : ℕ

Direct head register for one named tape.

Equations

• Complexity.RAM.TMConfig.Step.headReg tape = 1 + ↑tape

def Complexity.RAM.TMConfig.Step.cellBase (n bound : ℕ) (tape : Fin (n + 2)) : ℕ

First cell register of one named tape's bounded block.

Equations

• Complexity.RAM.TMConfig.Step.cellBase n bound tape = 1 + (n + 2) + ↑tape * (bound + 1)

def Complexity.RAM.TMConfig.Step.scratchBase (n bound : ℕ) : ℕ

First scratch register beyond the represented configuration.

Equations

• Complexity.RAM.TMConfig.Step.scratchBase n bound = Complexity.RAM.TMConfig.registerCount n bound

def Complexity.RAM.TMConfig.Step.zeroReg (n bound : ℕ) : ℕ

Constant-zero scratch register.

Equations

• Complexity.RAM.TMConfig.Step.zeroReg n bound = Complexity.RAM.TMConfig.Step.scratchBase n bound

def Complexity.RAM.TMConfig.Step.oneReg (n bound : ℕ) : ℕ

Constant-one scratch register used by decrementing switches and head moves.

Equations

• Complexity.RAM.TMConfig.Step.oneReg n bound = Complexity.RAM.TMConfig.Step.scratchBase n bound + 1

def Complexity.RAM.TMConfig.Step.stateScratchReg (n bound : ℕ) : ℕ

Destructive copy of the finite-state code used by the outer switch.

Equations

• Complexity.RAM.TMConfig.Step.stateScratchReg n bound = Complexity.RAM.TMConfig.Step.scratchBase n bound + 2

def Complexity.RAM.TMConfig.Step.addressReg (n bound : ℕ) : ℕ

Scratch register holding an indirect cell address.

Equations

• Complexity.RAM.TMConfig.Step.addressReg n bound = Complexity.RAM.TMConfig.Step.scratchBase n bound + 3

def Complexity.RAM.TMConfig.Step.valueReg (n bound : ℕ) : ℕ

Scratch register holding a writable symbol code.

Equations

• Complexity.RAM.TMConfig.Step.valueReg n bound = Complexity.RAM.TMConfig.Step.scratchBase n bound + 4

def Complexity.RAM.TMConfig.Step.symbolReg (n bound : ℕ) (tape : Fin (n + 2)) : ℕ

Scratch register holding the symbol loaded under one named head.

Equations

• Complexity.RAM.TMConfig.Step.symbolReg n bound tape = Complexity.RAM.TMConfig.Step.scratchBase n bound + 5 + ↑tape

def Complexity.RAM.TMConfig.Step.registerLimit (n bound : ℕ) : ℕ

Exclusive upper bound on every configuration and scratch register.

Equations

• Complexity.RAM.TMConfig.Step.registerLimit n bound = Complexity.RAM.TMConfig.Step.scratchBase n bound + n + 7

def Complexity.RAM.TMConfig.Step.wordBound {n : ℕ} (tm : TM n) (bound : ℕ) : ℕ

A uniform value bound large enough for addresses, states, symbols, and a single rightward head move.

Equations

• Complexity.RAM.TMConfig.Step.wordBound tm bound = max (Complexity.RAM.TMConfig.Step.registerLimit n bound) (max (Fintype.card tm.Q) (bound + 1))

def Complexity.RAM.TMConfig.Step.wordWidth {n : ℕ} (tm : TM n) (bound : ℕ) : ℕ

One-bit-cushioned width used in logarithmic-cost bounds.

Equations

• Complexity.RAM.TMConfig.Step.wordWidth tm bound = Complexity.RAM.bitlen (Complexity.RAM.TMConfig.Step.wordBound tm bound) + 1

def Complexity.RAM.TMConfig.Step.spaceBound {n : ℕ} (tm : TM n) (bound : ℕ) : ℕ

Peak-space envelope for one transition block.

Equations

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

def Complexity.RAM.TMConfig.Step.StoreBounded {n : ℕ} (tm : TM n) (bound : ℕ) (store : Structured.Store) : Prop

A store fits the explicit register/value envelope used by one transition block. This public predicate states the concrete boundary directly without exposing the internal resource-certificate structure.

Equations

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

def Complexity.RAM.TMConfig.Step.symbolAt (code : Fin 4) : Γ

Decode one valid four-way switch branch as a tape symbol.

Equations

• Complexity.RAM.TMConfig.Step.symbolAt code = Complexity.RAM.TMConfig.symbolDecode ↑code

def Complexity.RAM.TMConfig.Step.readSymbols {n : ℕ} {Q : Type} (cfg : Complexity.Cfg n Q) : Fin (n + 2) → Γ

Symbols currently read by all named TM heads.

Equations

• Complexity.RAM.TMConfig.Step.readSymbols cfg tape = (Complexity.RAM.TMConfig.tapeAt cfg tape).read

def Complexity.RAM.TMConfig.Step.loadTapeOps (n bound : ℕ) (tape : Fin (n + 2)) : List Structured.Basic

Load the symbol under one represented head into its dedicated scratch register.

Equations

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

def Complexity.RAM.TMConfig.Step.setupOps (n bound : ℕ) : List Structured.Basic

Initialize constants and copy the represented finite-state code.

Equations

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

def Complexity.RAM.TMConfig.Step.loadOps (n bound : ℕ) : List Structured.Basic

Initialize scratch state and load every represented head symbol.

Equations

• Complexity.RAM.TMConfig.Step.loadOps n bound = Complexity.RAM.TMConfig.Step.setupOps n bound ++ List.flatMap (Complexity.RAM.TMConfig.Step.loadTapeOps n bound) (List.finRange (n + 2))

def Complexity.RAM.TMConfig.Step.writeCode (symbol : Γw) : ℕ

Encode a writable tape symbol with the same zero-blank convention as the configuration representation.

Equations

• Complexity.RAM.TMConfig.Step.writeCode symbol = Complexity.RAM.TMConfig.symbolCode symbol.toΓ

def Complexity.RAM.TMConfig.Step.moveOps (n bound : ℕ) (tape : Fin (n + 2)) : Dir3 → List Structured.Basic

Update a represented head in the indicated direction.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.TMConfig.Step.moveOps n bound tape Complexity.Dir3.stay = []

def Complexity.RAM.TMConfig.Step.writeOps (n bound : ℕ) (tape : Fin (n + 2)) (write : Γw) : List Structured.Basic

Write one represented work/output tape and restore the left-end marker.

Equations

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

def Complexity.RAM.TMConfig.Step.writeMoveOps (n bound : ℕ) (tape : Fin (n + 2)) (write : Γw) (direction : Dir3) : List Structured.Basic

Write one represented work/output tape and move its head.

The direct write restoring cell zero to ▷ makes this branch-free while matching Tape.write, whose write at head zero is a no-op.

Equations

• Complexity.RAM.TMConfig.Step.writeMoveOps n bound tape write direction = Complexity.RAM.TMConfig.Step.writeOps n bound tape write ++ Complexity.RAM.TMConfig.Step.moveOps n bound tape direction

noncomputable def Complexity.RAM.TMConfig.Step.actionOps {n : ℕ} (tm : TM n) (bound : ℕ) (state : tm.Q) (symbols : Fin (n + 2) → Γ) : List Structured.Basic

Straight-line register operations implementing a statically selected TM transition case.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Step.action {n : ℕ} (tm : TM n) (bound : ℕ) (state : tm.Q) (symbols : Fin (n + 2) → Γ) : Structured.Cmd

Structured command for one statically selected transition case.

Equations

• Complexity.RAM.TMConfig.Step.action tm bound state symbols = Complexity.RAM.Structured.Cmd.basics (Complexity.RAM.TMConfig.Step.actionOps tm bound state symbols)

noncomputable def Complexity.RAM.TMConfig.Step.dispatchSymbols {n : ℕ} (tm : TM n) (bound : ℕ) (state : tm.Q) : List (Fin (n + 2)) → (Fin (n + 2) → Γ) → Structured.Cmd

Recursively dispatch on the loaded symbols for the listed named tapes.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.TMConfig.Step.dispatchSymbols tm bound state [] x✝ = Complexity.RAM.TMConfig.Step.action tm bound state x✝

noncomputable def Complexity.RAM.TMConfig.Step.dispatchState {n : ℕ} (tm : TM n) (bound : ℕ) : Structured.Cmd

Dispatch on the finite-state code, then on every loaded tape symbol.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Step.program {n : ℕ} (tm : TM n) (bound : ℕ) : Structured.Cmd

Fixed structured-RAM program implementing one nonhalting TM transition.

Equations

• Complexity.RAM.TMConfig.Step.program tm bound = (Complexity.RAM.Structured.Cmd.basics (Complexity.RAM.TMConfig.Step.loadOps n bound)).seq (Complexity.RAM.TMConfig.Step.dispatchState tm bound)

noncomputable def Complexity.RAM.TMConfig.Step.compiled {n : ℕ} (tm : TM n) (bound : ℕ) : Program

Concrete compiled RAM block for one nonhalting TM transition.

Equations

• Complexity.RAM.TMConfig.Step.compiled tm bound = (Complexity.RAM.TMConfig.Step.program tm bound).compile

noncomputable def Complexity.RAM.TMConfig.Step.dispatchSteps {n : ℕ} (tm : TM n) (bound : ℕ) (state : tm.Q) (actual : Fin (n + 2) → Γ) : List (Fin (n + 2)) → ℕ

Exact transition count through symbol dispatch for the actually read case.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.TMConfig.Step.dispatchSteps tm bound state actual [] = (Complexity.RAM.TMConfig.Step.actionOps tm bound state actual).length

noncomputable def Complexity.RAM.TMConfig.Step.stepCount {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) : ℕ

Exact source/compiled transition count for one represented TM step.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Step.dispatchCost {n : ℕ} (tm : TM n) (bound : ℕ) (state : tm.Q) (actual : Fin (n + 2) → Γ) : List (Fin (n + 2)) → ℕ

Logarithmic-cost bound through symbol dispatch.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.TMConfig.Step.dispatchCost tm bound state actual [] = 4 * (Complexity.RAM.TMConfig.Step.actionOps tm bound state actual).length * Complexity.RAM.TMConfig.Step.wordWidth tm bound

noncomputable def Complexity.RAM.TMConfig.Step.timeBound {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) : ℕ

Explicit logarithmic-cost bound for one represented TM step.

Equations

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