RAM-to-TM time-class containment -- proof internals

The concrete sparse simulator is applied at the first halting fuel. Minimality makes that fuel equal to unit-cost time, hence no larger than logarithmic RAM time. This discharges the quantitative side condition of the checked runtime envelope and lifts the simulation to deterministic polynomial time.

theorem Complexity.RAM.RegisterStore.Machine.programDecisionPolynomial_eval_internal (program : Program) (p : Polynomial ℕ) (inputLength : ℕ) : Polynomial.eval inputLength (programDecisionPolynomial program p) = programDecisionEnvelope program inputLength (Polynomial.eval inputLength p)

theorem Complexity.RAM.RegisterStore.Machine.programDecision_decidesInTime_internal {L : Language} {T : ℕ → ℕ} (program : Program) (hdecides : program.DecidesInTime L T) : (programDecisionTM standardControlInstructionTapes program).DecidesInTime L fun (inputLength : ℕ) => programDecisionEnvelope program inputLength (T inputLength)

theorem Complexity.RAM.RegisterStore.Machine.denseProgramDecision_decidesInTime_internal {L : Language} {T : ℕ → ℕ} (program : Program) (hdecides : program.DecidesInTime L T) : (denseProgramDecisionTM standardControlInstructionTapes program).DecidesInTime L fun (inputLength : ℕ) => denseProgramDecisionEnvelope program inputLength (T inputLength)

theorem Complexity.RAM.RegisterStore.Machine.DTIME_subset_DTIME_sq_internal (T : ℕ → ℕ) (hinput : BigO (fun (inputLength : ℕ) => inputLength + 1) T) : DTIME T ⊆ Complexity.DTIME fun (inputLength : ℕ) => T inputLength ^ 2

theorem Complexity.RAM.RegisterStore.Machine.P_subset_internal : P ⊆ Complexity.P