unionTM simulation — proof internals

This file contains the simulation lemmas needed to prove that unionTM tm₁ tm₂ correctly decides L₁ ∪ L₂ when tm₁ decides L₁ and tm₂ decides L₂.

Strategy

The proof proceeds in three phases:

1. Phase 1 simulation: Show that the union machine faithfully simulates tm₁ for t₁ steps, with tm₁'s output redirected to the fake output tape (work tape n₁).

2. Transition phase: After Phase 1, the machine rewinds the fake output to check tm₁'s result. If tm₁ accepted (cell 1 = Γ.one), write Γ.one to the real output and halt. Otherwise, rewind the input and start Phase 2.

3. Phase 2 simulation: Simulate tm₂ using the real output tape.

Key definitions

• unionIdleTape — the steady-state of an idle tape (head at 1, cells from Tape.init [])
• unionPhase1Cfg — embedding of a tm₁ config into the union machine's config space

def Complexity.TM.unionIdleTape : Tape

The steady-state tape for an idle tape during Phase 1. After the first step (where δ_right_of_start forces a right move from cell 0), idle tapes remain at head position 1 with blank cells.

Equations

• Complexity.TM.unionIdleTape = { head := 1, cells := (Complexity.Tape.init []).cells }

def Complexity.TM.unionPhase1Cfg {n₁ n₂ : ℕ} (tm₁ : TM n₁) (tm₂ : TM n₂) (c : Cfg n₁ tm₁.Q) : Cfg (n₁ + 1 + n₂) (UnionQ tm₁.Q tm₂.Q)

Embed a tm₁ configuration into the union machine's config space. Active tapes (input, work 0..n₁-1, fake output at n₁) come from c. Idle tapes (work n₁+1..n₁+n₂ and real output) use unionIdleTape.

Equations

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

theorem Complexity.TM.unionTM_phase1_simulation {n₁ n₂ : ℕ} (tm₁ : TM n₁) (tm₂ : TM n₂) (x : List Bool) {t₁ : ℕ} {c₁ : Cfg n₁ tm₁.Q} (hreach : tm₁.reachesIn t₁ (tm₁.initCfg x) c₁) (ht₁ : t₁ ≥ 1) : (tm₁.unionTM tm₂).reachesIn t₁ ((tm₁.unionTM tm₂).initCfg x) (tm₁.unionPhase1Cfg tm₂ c₁)

Phase 1 simulation: if tm₁ reaches c₁ from initCfg x in t₁ ≥ 1 steps, the union machine reaches the embedded config unionPhase1Cfg c₁ from its own initCfg x in the same number of steps.

theorem Complexity.TM.unionTM_transition_accept {n₁ n₂ : ℕ} (tm₁ : TM n₁) (tm₂ : TM n₂) {c₁ : Cfg n₁ tm₁.Q} (hhalt : tm₁.halted c₁) (haccept : c₁.output.cells 1 = Γ.one) (hcell0 : c₁.output.cells 0 = Γ.start) (hnostart : ∀ i ≥ 1, c₁.output.cells i ≠ Γ.start) : ∃ (t_tr : ℕ) (c_final : Cfg (n₁ + 1 + n₂) (UnionQ tm₁.Q tm₂.Q)), (tm₁.unionTM tm₂).reachesIn t_tr (tm₁.unionPhase1Cfg tm₂ c₁) c_final ∧ (tm₁.unionTM tm₂).halted c_final ∧ c_final.output.cells 1 = Γ.one ∧ t_tr ≤ c₁.output.head + 4

After Phase 1, if tm₁ accepted (output cell 1 = Γ.one), the union machine rewinds the fake output, checks the result, writes Γ.one to the real output, and halts.

theorem Complexity.TM.unionTM_transition_reject {n₁ n₂ : ℕ} (tm₁ : TM n₁) (tm₂ : TM n₂) (x : List Bool) {c₁ : Cfg n₁ tm₁.Q} (hhalt : tm₁.halted c₁) (hreject : c₁.output.cells 1 = Γ.zero) (hcell0_out : c₁.output.cells 0 = Γ.start) (hnostart_out : ∀ i ≥ 1, c₁.output.cells i ≠ Γ.start) (hinput_cells : c₁.input.cells = (Tape.init (List.map Γ.ofBool x)).cells) : ∃ (t_tr : ℕ) (c_mid : Cfg (n₁ + 1 + n₂) (UnionQ tm₁.Q tm₂.Q)), (tm₁.unionTM tm₂).reachesIn t_tr (tm₁.unionPhase1Cfg tm₂ c₁) c_mid ∧ c_mid.state = Sum.inr (Sum.inr tm₂.qstart) ∧ c_mid.input = Tape.init (List.map Γ.ofBool x) ∧ (∀ (j : Fin n₂), c_mid.work ⟨n₁ + 1 + ↑j, ⋯⟩ = Tape.init []) ∧ c_mid.output = Tape.init [] ∧ t_tr ≤ c₁.output.head + c₁.input.head + 7

After Phase 1, if tm₁ rejected, the union machine transitions to a config ready for Phase 2: state is Sum.inr (Sum.inr tm₂.qstart), input/output/active work tapes match tm₂.initCfg x.

structure Complexity.TM.UnionPhase2Compat {n₁ n₂ : ℕ} (tm₁ : TM n₁) (tm₂ : TM n₂) (c_u : Cfg (n₁ + 1 + n₂) (UnionQ tm₁.Q tm₂.Q)) (c₂ : Cfg n₂ tm₂.Q) : Prop

Phase 2 compatibility: a union machine config agrees with a tm₂ config on the active components (state, input, Phase 2 work tapes, output).

• state_eq : c_u.state = Sum.inr (Sum.inr c₂.state)
• input_eq : c_u.input = c₂.input
• work_eq (j : Fin n₂) : c_u.work ⟨n₁ + 1 + ↑j, ⋯⟩ = c₂.work j
• output_eq : c_u.output = c₂.output

theorem Complexity.TM.unionTM_phase2_simulation {n₁ n₂ : ℕ} (tm₁ : TM n₁) (tm₂ : TM n₂) (x : List Bool) {t₂ : ℕ} {c₂ : Cfg n₂ tm₂.Q} (hreach : tm₂.reachesIn t₂ (tm₂.initCfg x) c₂) {c_start : Cfg (n₁ + 1 + n₂) (UnionQ tm₁.Q tm₂.Q)} (hss : c_start.state = Sum.inr (Sum.inr tm₂.qstart)) (hsi : c_start.input = Tape.init (List.map Γ.ofBool x)) (hsw : ∀ (j : Fin n₂), c_start.work ⟨n₁ + 1 + ↑j, ⋯⟩ = Tape.init []) (hso : c_start.output = Tape.init []) : ∃ (c_end : Cfg (n₁ + 1 + n₂) (tm₁.unionTM tm₂).Q), (tm₁.unionTM tm₂).reachesIn t₂ c_start c_end ∧ c_end.state = Sum.inr (Sum.inr c₂.state) ∧ c_end.output = c₂.output

Phase 2 simulation: if tm₂ reaches c₂ from initCfg x in t₂ steps, and the starting union config is compatible with initCfg x, then the union machine reaches a config compatible with c₂ in t₂ steps.