Dense-overlay RAM decision-machine resource bounds

This surface exposes the selected-width one-step bound, the amortized quadratic loop bound, and the complete quadratic decision bound for the optimized dense-input RAM simulator.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramStepTime_le_envelope {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (snapshot : DenseOverlay.Snapshot) (hvalid : DenseOverlay.Valid snapshot.overlay) (hpc : snapshot.pc ≤ programResourceMagnitude program) : denseProgramStepTime tapes program input snapshot.pc snapshot.overlay ≤ denseStepEnvelope program input snapshot

One selected dense RAM instruction is simulated in time proportional to the live serialized volume times that instruction's actual charged width.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramLoopTime_le_envelope {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : DenseOverlay.Snapshot) (hvalid : DenseOverlay.Valid snapshot.overlay) (hpc : snapshot.pc ≤ programResourceMagnitude program) : denseProgramLoopTime tapes program input fuel snapshot ≤ denseProgramLoopEnvelope program input fuel snapshot

The complete conservative dense loop timer is bounded by the square of a potential containing live data, remaining fuel, and remaining RAM cost.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramDecisionTime_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)) : denseProgramDecisionTime tapes program input fuel ≤ denseProgramDecisionEnvelope program input.length (logTimeUpto program fuel (initCfg input))

A halted dense RAM run whose fuel is charged by logarithmic time is simulated within a quadratic envelope in input length plus charged RAM time.

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

Increasing the charged RAM-time argument can only enlarge the optimized quadratic decision envelope.