Sparse RAM decision-machine resource bounds

theorem Complexity.RAM.RegisterStore.Machine.programResourceMagnitude_pos (program : Program) : 1 ≤ programResourceMagnitude program

The fixed program magnitude is positive.

theorem Complexity.RAM.RegisterStore.Machine.program_length_le_resourceMagnitude (program : Program) : List.length program ≤ programResourceMagnitude program

The fixed program length is absorbed by its resource magnitude.

theorem Complexity.RAM.RegisterStore.Machine.programStaticWidth_le_resourceMagnitude (program : Program) : programStaticWidth program ≤ programResourceMagnitude program

Every fixed program literal width is absorbed by the resource magnitude.

theorem Complexity.RAM.RegisterStore.Machine.programDecisionScale_pos (program : Program) (inputLength cost : ℕ) : 1 ≤ programDecisionScale program inputLength cost

The common run scale is positive.

theorem Complexity.RAM.RegisterStore.Machine.programDecisionTime_le_envelope {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (fuel : ℕ) (hhalted : Halted program (run program fuel (initCfg input))) (hfuel : fuel ≤ logTimeUpto program fuel (initCfg input)) : programDecisionTime tapes program input fuel ≤ programDecisionEnvelope program input.length (logTimeUpto program fuel (initCfg input))

A fuel-bounded halted RAM run whose fuel is charged by logarithmic time is simulated by the concrete decision TM within the checked fourth-degree envelope.

theorem Complexity.RAM.RegisterStore.Machine.programDecisionEnvelope_mono_cost (program : Program) (inputLength left right : ℕ) (hle : left ≤ right) : programDecisionEnvelope program inputLength left ≤ programDecisionEnvelope program inputLength right

Increasing the charged RAM-time argument can only increase the concrete simulation envelope.