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

This module lifts the checked public-ABI sparse simulation from one halting run to deciders and then discharges the polynomial-bound arithmetic needed for the forward machine-model robustness theorem.

theorem Complexity.RAM.TMConfig.Sparse.compiledDecision_decidesInTime_internal {n : ℕ} {tm : TM n} {L : Language} {T : ℕ → ℕ} (hdecides : tm.DecidesInTime L T) : (compiledDecision tm).DecidesInTime L fun (inputLength : ℕ) => decisionTimeBound tm inputLength (T inputLength)

theorem Complexity.RAM.TMConfig.Sparse.mem_DTIME_of_decidesInTime_internal {n : ℕ} {tm : TM n} {L : Language} {T : ℕ → ℕ} (hdecides : tm.DecidesInTime L T) : L ∈ DTIME fun (inputLength : ℕ) => decisionTimeBound tm inputLength (T inputLength)

def Complexity.RAM.TMConfig.Sparse.PolyBound (f : ℕ → ℕ) : Prop

Pointwise domination by the evaluation of a natural polynomial.

Equations

• Complexity.RAM.TMConfig.Sparse.PolyBound f = ∃ (p : Polynomial ℕ), ∀ (inputLength : ℕ), f inputLength ≤ Polynomial.eval inputLength p

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.const (value : ℕ) : PolyBound fun (x : ℕ) => value

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.id : PolyBound fun (inputLength : ℕ) => inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.add {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) : PolyBound fun (inputLength : ℕ) => f inputLength + g inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.mul {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) : PolyBound fun (inputLength : ℕ) => f inputLength * g inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.mono {f g : ℕ → ℕ} (hg : PolyBound g) (hle : ∀ (inputLength : ℕ), f inputLength ≤ g inputLength) : PolyBound f

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.max {f g : ℕ → ℕ} (hf : PolyBound f) (hg : PolyBound g) : PolyBound fun (inputLength : ℕ) => Max.max (f inputLength) (g inputLength)

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.eval (p : Polynomial ℕ) : PolyBound fun (inputLength : ℕ) => Polynomial.eval inputLength p

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.width {f : ℕ → ℕ} (hf : PolyBound f) : PolyBound fun (inputLength : ℕ) => bitlen (f inputLength) + 1

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.registerBound (workTapes : ℕ) {f : ℕ → ℕ} (hf : PolyBound f) : PolyBound fun (inputLength : ℕ) => Sparse.registerBound workTapes (f inputLength)

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.wordBound {n : ℕ} (tm : TM n) {f : ℕ → ℕ} (hf : PolyBound f) : PolyBound fun (inputLength : ℕ) => Sparse.wordBound tm (f inputLength)

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.wordWidth {n : ℕ} (tm : TM n) {f : ℕ → ℕ} (hf : PolyBound f) : PolyBound fun (inputLength : ℕ) => Sparse.wordWidth tm (f inputLength)

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.marshalBaseBound (workTapes : ℕ) : PolyBound fun (inputLength : ℕ) => Sparse.marshalBaseBound workTapes inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.marshalBound (workTapes : ℕ) : PolyBound fun (inputLength : ℕ) => Sparse.marshalBound workTapes inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.marshalBaseWidth (workTapes : ℕ) : PolyBound fun (inputLength : ℕ) => Sparse.marshalBaseWidth workTapes inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.marshalWidth (workTapes : ℕ) : PolyBound fun (inputLength : ℕ) => Sparse.marshalWidth workTapes inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.marshalLoopTimeBound (workTapes : ℕ) : PolyBound fun (inputLength : ℕ) => Sparse.marshalLoopTimeBound workTapes inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.marshalLeafTimeBound {n : ℕ} (tm : TM n) : PolyBound fun (inputLength : ℕ) => Sparse.marshalLeafTimeBound tm inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.marshalTimeBound {n : ℕ} (tm : TM n) : PolyBound fun (inputLength : ℕ) => Sparse.marshalTimeBound tm inputLength

theorem Complexity.RAM.TMConfig.Sparse.PolyBound.decisionTimeBound {n : ℕ} (tm : TM n) {T : ℕ → ℕ} (hT : PolyBound T) : PolyBound fun (inputLength : ℕ) => Sparse.decisionTimeBound tm inputLength (T inputLength)

theorem Complexity.RAM.TMConfig.Sparse.P_subset_internal : Complexity.P ⊆ P