Resource envelopes for the fixed sparse TM simulator -- proof internals

The semantic simulation already records exact source steps, cost, and space. This layer supplies the uniform finite-store envelope needed to turn those measurements into explicit bounds depending only on input length and TM steps.

@[reducible, inline]

abbrev Complexity.RAM.TMConfig.Sparse.StepEnvelope {n : ℕ} (tm : TM n) (bound : ℕ) (store : Structured.Store) : Prop

Shared envelope used by marshalling and repeated sparse simulation.

Equations

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

theorem Complexity.RAM.TMConfig.Sparse.bound_lt_registerBound_internal (n bound : ℕ) : bound < registerBound n (bound + 1)

theorem Complexity.RAM.TMConfig.Sparse.control_lt_registerBound_internal (n bound : ℕ) : cellBase n < registerBound n (bound + 1)

theorem Complexity.RAM.TMConfig.Sparse.cellReg_lt_registerBound_internal {n : ℕ} (tape : Fin (n + 2)) {position bound : ℕ} (hposition : position ≤ bound + 1) : cellReg n tape position < registerBound n (bound + 1)

theorem Complexity.RAM.TMConfig.Sparse.cellReg_decode_internal (n reg : ℕ) (hreg : cellBase n ≤ reg) : cellReg n (decodeCellTape n reg) (decodeCellPosition n reg) = reg

theorem Complexity.RAM.TMConfig.Sparse.registerBound_le_wordBound_internal {n : ℕ} (tm : TM n) (bound : ℕ) : registerBound n (bound + 1) ≤ wordBound tm bound

theorem Complexity.RAM.TMConfig.Sparse.card_le_wordBound_internal {n : ℕ} (tm : TM n) (bound : ℕ) : Fintype.card tm.Q ≤ wordBound tm bound

theorem Complexity.RAM.TMConfig.Sparse.bound_succ_le_wordBound_internal {n : ℕ} (tm : TM n) (bound : ℕ) : bound + 1 ≤ wordBound tm bound

theorem Complexity.RAM.TMConfig.Sparse.initRegs_envelope_internal {n : ℕ} (tm : TM n) (x : List Bool) (bound : ℕ) (hlength : x.length ≤ bound) : StepEnvelope tm bound (initRegs x)

The public RAM input store fits every sparse execution envelope whose bound contains the input length.

theorem Complexity.RAM.TMConfig.Sparse.encodeRegs_envelope_internal {n : ℕ} (tm : TM n) (cfg : Complexity.Cfg n tm.Q) (bound : ℕ) (hbounded : Bounded cfg bound) (hheads : HeadsBounded cfg bound) : StepEnvelope tm bound (encodeRegs tm cfg)

The canonical sparse encoding fits the common execution envelope whenever all heads and nonblank tape cells lie within the chosen bound.

theorem Complexity.RAM.TMConfig.Sparse.loadOps_measured_internal {n : ℕ} {tm : TM n} {bound : ℕ} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm cfg store) (hheads : HeadsBounded cfg bound) (henvelope : StepEnvelope tm bound store) : have final := Structured.Basic.execList (loadOps n) store; Structured.Internal.MeasuredRuns (Structured.Cmd.basics (loadOps n)) store final (loadOps n).length (4 * (loadOps n).length * wordWidth tm bound) (spaceBound tm bound) ∧ StepEnvelope tm bound final

theorem Complexity.RAM.TMConfig.Sparse.continueCheck_measured_internal {n : ℕ} {tm : TM n} {bound : ℕ} {cfg : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm cfg store) (hheads : HeadsBounded cfg bound) (henvelope : StepEnvelope tm bound store) : ∃ (final : Structured.Store), Structured.Internal.MeasuredRuns (continueCheck tm) store final (continueSteps tm cfg) (continueTimeBound tm bound cfg) (spaceBound tm bound) ∧ Represents tm cfg final ∧ final (valueReg n) = runningFlag tm cfg.state ∧ final (oneReg n) = 1 ∧ final (tapeCountReg n) = n + 2 ∧ StepEnvelope tm bound final

theorem Complexity.RAM.TMConfig.Sparse.headsBounded_step_internal {n : ℕ} {tm : TM n} {bound : ℕ} {cfg next : Complexity.Cfg n tm.Q} (hstep : tm.step cfg = some next) (hheads : HeadsBounded cfg bound) : HeadsBounded next (bound + 1)

theorem Complexity.RAM.TMConfig.Sparse.program_measured_internal {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).cells 0 = Γ.start) (houtputStart : cfg.output.cells 0 = Γ.start) (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

theorem Complexity.RAM.TMConfig.Sparse.loop_measured_internal {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) (hflag : store (valueReg n) = runningFlag tm cfg.state) (hheads : HeadsBounded cfg base) (hworkStart : ∀ (i : Fin n), (cfg.work i).cells 0 = Γ.start) (houtputStart : cfg.output.cells 0 = Γ.start) (henvelope : StepEnvelope tm (base + steps) store) : ∃ (final : Structured.Store), Structured.Internal.MeasuredRuns (Structured.Cmd.whileNonzero (valueReg n) (loopBody tm)) store final (loopSteps tm steps cfg) (loopTimeBound tm base steps cfg) (spaceBound tm (base + steps)) ∧ Represents tm halted final ∧ StepEnvelope tm (base + steps) final

theorem Complexity.RAM.TMConfig.Sparse.runUntilHalt_measured_internal {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).cells 0 = Γ.start) (houtputStart : cfg.output.cells 0 = Γ.start) (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

theorem Complexity.RAM.TMConfig.Sparse.timeBound_le_stepFactor_internal {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) : timeBound tm bound cfg ≤ stepFactor tm * wordWidth tm bound

theorem Complexity.RAM.TMConfig.Sparse.continueTimeBound_le_factor_internal {n : ℕ} (tm : TM n) (bound : ℕ) (cfg : Complexity.Cfg n tm.Q) : continueTimeBound tm bound cfg ≤ continueFactor tm * wordWidth tm bound

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

theorem Complexity.RAM.TMConfig.Sparse.runTimeBound_le_linear_internal {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)