Sparse RAM decision-machine resource-bound proof internals

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

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

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

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

theorem Complexity.RAM.RegisterStore.Machine.programDecisionTime_le_envelope_internal {m : ℕ} (tapes : ControlInstructionTapes m) (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))

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