RAM-to-TM time-class containment

The fixed twenty-work-tape simulators transfer logarithmic-cost RAM deciders to deterministic Turing deciders. The sparse fallback gives the original quartic polynomial envelope; the dense-input overlay gives the sharp quadratic parametric containment. Together with the sparse TM-to-RAM compiler, these establish machine-model robustness of polynomial time.

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

Evaluating the packaged simulator polynomial gives its concrete runtime envelope with the supplied polynomial RAM-time bound.

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

Every RAM decider transfers to the fixed sparse Turing simulator with the explicit fourth-degree envelope around its logarithmic-time bound.

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

Every RAM decider transfers to the optimized fixed dense-input simulator with an explicit quadratic envelope in input length plus RAM time.

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

Under the standard assumption that the RAM time bound dominates reading the input, logarithmic-cost RAM time T is contained in deterministic Turing time T².

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

Every polynomial logarithmic-cost RAM language is in deterministic polynomial Turing time.

theorem Complexity.RAM.RegisterStore.Machine.RAM_P_eq_P : P = Complexity.P

Polynomial time is invariant between the concrete multitape TM and logarithmic-cost RAM models formalized in the library.