The universal machine satisfies the generic universality interface -- internals

The concrete utmTM is connected to TM.IsEfficientlyUniversal through three exact simulations, each proved in both directions:

1. a k-work-tape machine is simulated by a single-work-tape machine under the identity compiler (singleTapeSim, or pad0 when k = 0);
2. a single-work-tape machine is simulated step for step by the interpreted description descOfTM;
3. the interpreted description of α is simulated by utmTM under the compiler pair α.

Each stage supplies two facts to one generic engine (simulates_and_simulatesInTime_of_forward): a forward simulation of halting runs that preserves the exact output, and unbounded simulator runs on every program where the source diverges. Determinism then reflects halting and output: a simulator run that halts at time T admits no run longer than T.

The divergence facts are the new content. For the single-tape stage they come from the macro-step correspondence corr_trace_macroPos, which holds on non-halting runs; for the universal machine they come from loop_iteration, which simulates one source step from an arbitrary configuration and takes at least one step.

theorem Complexity.TM.exists_reachesIn_of_not_halts {sourceTapes : ℕ} {source : TM sourceTapes} {program : List Bool} (hdiv : ¬source.Halts program) (n : ℕ) : ∃ (c : Cfg sourceTapes source.Q), source.reachesIn n (source.initCfg program) c

A machine that never halts on program has a run of every length.

theorem Complexity.TM.hasOutput_iff_of_agree_through_blank {tape reference : Tape} {m : ℕ} (hblank : reference.cells (m + 1) = Γ.blank) (hnonblank : ∀ j < m, reference.cells (j + 1) ≠ Γ.blank) (hagree : ∀ j ≤ m, tape.cells (j + 1) = reference.cells (j + 1)) (output : List Bool) : tape.HasOutput output ↔ reference.HasOutput output

Two tapes that agree through the first blank of the second one have the same exact outputs.

theorem Complexity.TM.simulates_and_simulatesInTime_of_forward {simulatorTapes sourceTapes : ℕ} {simulator : TM simulatorTapes} {source : TM sourceTapes} (compile : List Bool → List Bool) (clock : TimeOverhead) (hmono : ∀ (program : List Bool), Monotone (clock program)) (hforward : ∀ (program : List Bool) (time : ℕ) (c : Cfg sourceTapes source.Q), source.reachesIn time (source.initCfg program) c → source.halted c → ∃ (d : Cfg simulatorTapes simulator.Q), ∃ steps ≤ clock program time, simulator.reachesIn steps (simulator.initCfg (compile program)) d ∧ simulator.halted d ∧ ∀ (output : List Bool), d.output.HasOutput output ↔ c.output.HasOutput output) (hdiverge : ∀ (program : List Bool), ¬source.Halts program → ∀ (n : ℕ), ∃ (steps : ℕ) (d : Cfg simulatorTapes simulator.Q), n ≤ steps ∧ simulator.reachesIn steps (simulator.initCfg (compile program)) d) : simulator.Simulates source compile ∧ simulator.SimulatesInTime source compile clock

Simulation from forward runs and divergence. A compiler and a monotone clock yield an exact semantic simulation and a timed simulation when

• every halting source run is reproduced within the clock by a halting simulator run with the same exact outputs, and
• on every program where the source diverges, the simulator has runs of unbounded length.

Reflection of halting and of outputs is by determinism: a simulator run that halts at time T admits no longer run, and halted endpoints are unique.

theorem Complexity.NTM.Deterministic.toTM_reachesIn_trace_of_ne_halt {n : ℕ} {N : NTM n} (hdet : N.Deterministic) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n N.Q) : (N.trace T choices c).state ≠ N.qhalt → N.toTM.reachesIn T c (N.trace T choices c)

A non-halted trace configuration of a deterministic NTM is reached by toTM in exactly the trace length.

def Complexity.TM.singleTapeClock (k : ℕ) : TimeOverhead

The single-tape stage's clock: the quadratic overhead of NTM.singleTapeSimTime at a fixed source budget.

Equations

• Complexity.TM.singleTapeClock k program time = 16 * (k + 1) * (time + program.length + 1) ^ 2

theorem Complexity.TM.singleTapeClock_mono (k : ℕ) (program : List Bool) : Monotone (singleTapeClock k program)

theorem Complexity.TM.exists_singleTape_simulates_internal {k : ℕ} (M : TM k) : ∃ (M₁ : TM 1), M₁.Simulates M id ∧ M₁.SimulatesInTime M id (singleTapeClock k)

Stage 1. Every k-work-tape machine is simulated exactly by a single-work-tape machine under the identity compiler, with quadratic overhead.

theorem Complexity.TM.descOfTM_simulates_internal (M : TM 1) : M.descOfTM.toTM.Simulates M id ∧ M.descOfTM.toTM.SimulatesInTime M id fun (x : List Bool) (time : ℕ) => time

Stage 2. The interpreted description of a single-work-tape machine simulates it step for step.

def Complexity.TM.UTMBody.loopCfg (c : Cfg 6 (bodyTM.loopTM haltTestTM).Q) : Cfg 6 utmTM.Q

Embed a loop configuration into utmTM: phase two of the outer sequence, phase one of the inner loop/extract sequence.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.UTMBody.utmTM_reachesIn_loopCfg {t : ℕ} {c c' : Cfg 6 (bodyTM.loopTM haltTestTM).Q} (h : (bodyTM.loopTM haltTestTM).reachesIn t c c') : utmTM.reachesIn t (loopCfg c) (loopCfg c')

Loop runs lift to utmTM runs.

theorem Complexity.TM.UTMBody.utmTM_reachesIn_loop_start (α x : List Bool) : ∃ (t : ℕ) (inp : Tape) (work : Fin 6 → Tape) (out : Tape), SimInv α ((decodeDesc α).toTM.initCfg x) inp work out ∧ out.cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) ∧ out.head = 1 ∧ utmTM.reachesIn t (utmTM.initCfg (pair α x)) (loopCfg { state := (bodyTM.loopTM haltTestTM).qstart, input := inp, work := work, output := out })

After initialization, utmTM reaches the loop's start state with the standing invariant at the interpreted machine's initial configuration.

theorem Complexity.TM.UTMBody.utmTM_diverges (α x : List Bool) (hterm : TerminatedRegion α) (hdiv : ¬(decodeDesc α).toTM.Halts x) (n : ℕ) : ∃ (steps : ℕ) (d : Cfg 6 utmTM.Q), n ≤ steps ∧ utmTM.reachesIn steps (utmTM.initCfg (pair α x)) d

On a divergent interpreted run, utmTM has runs of every length: each loop iteration simulates one more source step and takes at least one step.

theorem Complexity.TM.UTMBody.utmTime_mono (α : List Bool) (n : ℕ) : Monotone fun (T : ℕ) => utmTime α T n

theorem Complexity.TM.UTMBody.utmTM_simulates_decodeDesc_internal (α : List Bool) (hterm : TerminatedRegion α) : utmTM.Simulates (decodeDesc α).toTM (pair α) ∧ utmTM.SimulatesInTime (decodeDesc α).toTM (pair α) fun (program : List Bool) (time : ℕ) => utmTime α time program.length

Stage 3. For a canonical description α, utmTM simulates the interpreted machine exactly under the compiler pair α, within utmTime.

def Complexity.TM.UTMBody.utmClock (α : List Bool) (k : ℕ) : TimeOverhead

The composed clock: single-tape overhead followed by universal simulation of the extracted description α.

Equations

• Complexity.TM.UTMBody.utmClock α k program time = Complexity.TM.UTMBody.utmTime α (Complexity.TM.singleTapeClock k program time) program.length

theorem Complexity.TM.UTMBody.utmTM_simulates_pair_internal {k : ℕ} (M : TM k) : ∃ (α : List Bool), utmTM.Simulates M (pair α) ∧ utmTM.SimulatesInTime M (pair α) (utmClock α k)

utmTM simulates every machine through a fixed description. For every k-work-tape machine there is a description α such that utmTM simulates it exactly under the uniform compiler pair α, within utmClock α k.

theorem Complexity.TM.UTMBody.pair_isComputable (α : List Bool) : IsComputable (pair α)

The compiler pair α is computable; indeed it is polynomial-time.

theorem Complexity.TM.UTMBody.pair_additiveProgramOverhead (α : List Bool) : HasAdditiveProgramOverhead (pair α) (2 * α.length + 2)

pair α adds exactly 2|α| + 2 bits.

theorem Complexity.TM.UTMBody.utmClock_polynomial (α : List Bool) (k : ℕ) : PolynomialTimeOverhead (utmClock α k)

The composed clock is polynomial in program length plus source time.

theorem Complexity.TM.UTMBody.utmTM_isEfficientlyUniversal_internal : utmTM.IsEfficientlyUniversal

The concrete universal machine is polynomially efficiently universal.