Pointwise output semantics for deterministic oracle TMs

These relations treat the finite input as a program and the Boolean oracle as a separate parameter. The ordinary-TM embedding preserves bounded production exactly, so the oracle semantics is a conservative extension.

theorem Complexity.OracleTM.HaltsInTime.mono {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {program : List Bool} {first second : ℕ} (hbound : first ≤ second) (hhalt : machine.HaltsInTime oracle program first) : machine.HaltsInTime oracle program second

Increasing the clock preserves bounded oracle-machine halting.

theorem Complexity.OracleTM.halts_of_haltsInTime {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {program : List Bool} {time : ℕ} (hhalt : machine.HaltsInTime oracle program time) : machine.Halts oracle program

Forgetting a clock turns bounded oracle-machine halting into eventual halting.

theorem Complexity.OracleTM.ProducesInTime.mono {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {program output : List Bool} {first second : ℕ} (hbound : first ≤ second) (hproduce : machine.ProducesInTime oracle program output first) : machine.ProducesInTime oracle program output second

Increasing the clock preserves bounded oracle-machine production.

theorem Complexity.OracleTM.produces_of_producesInTime {n : ℕ} {machine : OracleTM n} {oracle : BooleanOracle} {program output : List Bool} {time : ℕ} (hproduce : machine.ProducesInTime oracle program output time) : machine.Produces oracle program output

Forgetting a clock turns bounded oracle production into eventual production.

theorem Complexity.TM.toOracleTM_producesInTime_iff {n : ℕ} (machine : TM n) (oracle : BooleanOracle) (program output : List Bool) (time : ℕ) : machine.toOracleTM.ProducesInTime oracle program output time ↔ machine.ProducesInTime program output time

The ordinary-machine embedding preserves exact bounded production for every oracle.