Complement TM: proof internals

This file provides the simulation lemmas for TM.complementTM, showing that the complement machine correctly flips the output of the original TM.

def Complexity.TM.complementCfg {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : Cfg n tm.complementTM.Q

Embed a configuration of tm into tm.complementTM by tagging the state with Sum.inl and keeping all tapes unchanged.

Equations

• tm.complementCfg c = { state := Sum.inl c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.compCfg_initCfg {n : ℕ} (tm : TM n) (x : List Bool) : tm.complementCfg (tm.initCfg x) = tm.complementTM.initCfg x

Embedding the initial configuration of tm on input x yields the initial configuration of tm.complementTM on x.

theorem Complexity.TM.compCfg_qstart {n : ℕ} (tm : TM n) (inp : Tape) (work : Fin n → Tape) (out : Tape) : tm.complementCfg { state := tm.qstart, input := inp, work := work, output := out } = { state := tm.complementTM.qstart, input := inp, work := work, output := out }

The embedding sends configurations in tm's start state to configurations in tm.complementTM's start state, preserving all tapes.

theorem Complexity.TM.complementTM_simulation {n : ℕ} (tm : TM n) {c c' : Cfg n tm.Q} {t : ℕ} (hreach : tm.reachesIn t c c') : tm.complementTM.reachesIn t (tm.complementCfg c) (tm.complementCfg c')

tm.complementTM simulates tm step-for-step on embedded configurations: a t-step run of tm lifts to a t-step run of the complement machine.

theorem Complexity.TM.complementTM_rewind_and_flip {n : ℕ} (tm : TM n) (c_halt : Cfg n tm.Q) (hhalt : tm.halted c_halt) (hcell0 : c_halt.output.cells 0 = Γ.start) (hnostart : ∀ j ≥ 1, c_halt.output.cells j ≠ Γ.start) : ∃ (c_done : Cfg n tm.complementTM.Q) (t_rw : ℕ), tm.complementTM.reachesIn t_rw (tm.complementCfg c_halt) c_done ∧ tm.complementTM.halted c_done ∧ c_done.output.cells 1 = (flipBit (c_halt.output.cells 1)).toΓ ∧ t_rw ≤ c_halt.output.head + 4

From halted complementCfg, reach done state with flipped output. Takes ≤ output.head + 4 steps.

theorem Complexity.TM.complementTM_decidesInTime {n : ℕ} (tm : TM n) {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInTime L f) : tm.complementTM.DecidesInTime Lᶜ fun (n : ℕ) => 2 * f n + 4

If tm decides L in time f, then complementTM tm decides Lᶜ in time 2 * f + 4.