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

Unlike the bounded dense block, this program is determined solely by tm. It computes an interleaved tape-cell address as cellBase + head * (n + 2) + tape, so the same finite RAM program can follow an unbounded computation.

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

Input tape slot.

Equations

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

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

Work-tape slot.

Equations

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

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

Output tape slot.

Equations

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

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

Symbols currently read by all named TM heads.

Equations

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

def Complexity.RAM.TMConfig.Sparse.addressOps (n : ℕ) (tape : Fin (n + 2)) : List Structured.Basic

Compute the indirect address of the cell under one named head. valueReg temporarily holds the tape-specific base constant.

Equations

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

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

Load the symbol under one named head.

Equations

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

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

Initialize fixed constants and copy the finite-state code.

Equations

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

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

Initialize scratch state and load every named head symbol.

Equations

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

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

Update one represented head.

Equations

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

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

Write the cell under one represented head and restore its immutable cell zero to the left-end marker.

Equations

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

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

Write and move one represented work/output tape.

Equations

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

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

Straight-line operations for one statically selected transition.

Equations

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

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

Structured selected-transition command.

Equations

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

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

Recursively dispatch on loaded tape symbols.

Equations

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

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

Dispatch on the state code and every loaded symbol.

Equations

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

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

Fixed uniform structured-RAM block for one nonhalting TM transition.

Equations

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

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

Concrete compiled uniform transition block.

Equations

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

def Complexity.RAM.TMConfig.Sparse.runningFlag {n : ℕ} (tm : TM n) (state : tm.Q) : ℕ

Runtime loop flag: zero exactly in the designated halt state.

Equations

• Complexity.RAM.TMConfig.Sparse.runningFlag tm state = if state = tm.qhalt then 0 else 1

noncomputable def Complexity.RAM.TMConfig.Sparse.continueDispatch {n : ℕ} (tm : TM n) : Structured.Cmd

Finite-state branch that writes the runtime loop flag.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Sparse.continueCheck {n : ℕ} (tm : TM n) : Structured.Cmd

Reload the represented state and set the runtime loop flag. The full load prelude is deliberately reused so this fixed controller inherits its framing theorem.

Equations

• Complexity.RAM.TMConfig.Sparse.continueCheck tm = (Complexity.RAM.Structured.Cmd.basics (Complexity.RAM.TMConfig.Sparse.loadOps n)).seq (Complexity.RAM.TMConfig.Sparse.continueDispatch tm)

noncomputable def Complexity.RAM.TMConfig.Sparse.loopBody {n : ℕ} (tm : TM n) : Structured.Cmd

One loop iteration: perform one TM transition, then recompute whether the successor is halted.

Equations

• Complexity.RAM.TMConfig.Sparse.loopBody tm = (Complexity.RAM.TMConfig.Sparse.program tm).seq (Complexity.RAM.TMConfig.Sparse.continueCheck tm)

noncomputable def Complexity.RAM.TMConfig.Sparse.runUntilHalt {n : ℕ} (tm : TM n) : Structured.Cmd

Fixed structured program that repeats transitions until the represented TM enters qhalt.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Sparse.compiledUntilHalt {n : ℕ} (tm : TM n) : Program

Concrete compiled fixed program that simulates until qhalt.

Equations

• Complexity.RAM.TMConfig.Sparse.compiledUntilHalt tm = (Complexity.RAM.TMConfig.Sparse.runUntilHalt tm).compile

noncomputable def Complexity.RAM.TMConfig.Sparse.continueSteps {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) : ℕ

Exact instruction count of one continuation check.

Equations

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

def Complexity.RAM.TMConfig.Sparse.registerBound (n bound : ℕ) : ℕ

Largest cell-register index needed when heads stay at most bound.

Equations

• Complexity.RAM.TMConfig.Sparse.registerBound n bound = Complexity.RAM.TMConfig.Sparse.cellReg n (Complexity.RAM.TMConfig.Sparse.outputTape n) bound + 1

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

Uniform value bound for a transition whose input heads are at most bound; it includes a possible right move.

Equations

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

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

One-bit-cushioned resource width.

Equations

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

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

Peak sparse-store space envelope through one transition.

Equations

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

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

Exact transition count through symbol dispatch.

Equations

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

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

Exact source/compiled instruction count for one sparse TM step.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Sparse.loopSteps {n : ℕ} (tm : TM n) : ℕ → Complexity.Cfg n tm.Q → ℕ

Exact instruction count of the while-loop suffix along steps TM transitions. The none branch is unreachable in the corresponding simulation theorem.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.TMConfig.Sparse.loopSteps tm 0 x✝ = 1

noncomputable def Complexity.RAM.TMConfig.Sparse.runSteps {n : ℕ} (tm : TM n) (steps : ℕ) (cfg : Complexity.Cfg n tm.Q) : ℕ

Exact instruction count of the complete fixed simulator along a known halting run.

Equations

• Complexity.RAM.TMConfig.Sparse.runSteps tm steps cfg = Complexity.RAM.TMConfig.Sparse.continueSteps tm cfg + Complexity.RAM.TMConfig.Sparse.loopSteps tm steps cfg

noncomputable def Complexity.RAM.TMConfig.Sparse.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.Sparse.dispatchCost tm bound state actual [] = 4 * (Complexity.RAM.TMConfig.Sparse.actionOps tm state actual).length * Complexity.RAM.TMConfig.Sparse.wordWidth tm bound

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

Explicit logarithmic cost bound for one sparse TM step.

Equations

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

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

Explicit logarithmic cost bound for one continuation check under a fixed store envelope.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Sparse.loopTimeBound {n : ℕ} (tm : TM n) : ℕ → ℕ → Complexity.Cfg n tm.Q → ℕ

Accumulated logarithmic cost bound for the while-loop suffix. base bounds the current heads; the remaining-step allowance supplies the common envelope.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.TMConfig.Sparse.loopTimeBound tm x✝¹ 0 x✝ = Complexity.RAM.TMConfig.Sparse.wordWidth tm x✝¹

noncomputable def Complexity.RAM.TMConfig.Sparse.runTimeBound {n : ℕ} (tm : TM n) (base steps : ℕ) (cfg : Complexity.Cfg n tm.Q) : ℕ

Accumulated logarithmic cost bound for the complete fixed simulator.

Equations

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

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

Width multiplier through the symbol-dispatch suffix.

Equations

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

noncomputable def Complexity.RAM.TMConfig.Sparse.stepFactor {n : ℕ} (tm : TM n) : ℕ

Configuration-independent multiplier for one sparse transition, obtained by taking the finite maximum over states and currently scanned symbols.

Equations

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

def Complexity.RAM.TMConfig.Sparse.continueFactor {n : ℕ} (tm : TM n) : ℕ

Configuration-independent multiplier for one continuation check.

Equations

• Complexity.RAM.TMConfig.Sparse.continueFactor tm = 4 * (Complexity.RAM.TMConfig.Sparse.loadOps n).length + (7 * Fintype.card tm.Q + 5)

noncomputable def Complexity.RAM.TMConfig.Sparse.iterationFactor {n : ℕ} (tm : TM n) : ℕ

Per-iteration multiplier including loop control, transition, and continuation check.

Equations

• Complexity.RAM.TMConfig.Sparse.iterationFactor tm = 3 + Complexity.RAM.TMConfig.Sparse.stepFactor tm + Complexity.RAM.TMConfig.Sparse.continueFactor tm

noncomputable def Complexity.RAM.TMConfig.Sparse.runFactor {n : ℕ} (tm : TM n) : ℕ

Coarse multiplier for a complete run, including the initial continuation check and final zero test.

Equations

• Complexity.RAM.TMConfig.Sparse.runFactor tm = Complexity.RAM.TMConfig.Sparse.continueFactor tm + Complexity.RAM.TMConfig.Sparse.iterationFactor tm + 1