Online witness equivalence: proof internals

The existing guess-tape simulation identifies the visible endpoints of witness runs with NTM traces at each exact clock. Halting, acceptance, and prefix-space bounds then transfer without changing either resource bound.

theorem Complexity.WitnessTM.run_congr_prefix_internal {k : ℕ} (W : WitnessTM k) (x : List Bool) (t : ℕ) (g h : ℕ → Bool) (hprefix : ∀ i < t, g i = h i) : NTM.dropChoice (W.run x g t) = NTM.dropChoice (W.run x h t)

The visible result of a bounded witness run depends only on the corresponding finite Boolean prefix. Unread witness tails need not agree.

theorem Complexity.WitnessTM.exists_run_eq_trace_internal {k : ℕ} (W : WitnessTM k) (x : List Bool) (t : ℕ) (choices : Fin t → Bool) : ∃ (g : ℕ → Bool), NTM.dropChoice (W.run x g t) = W.toNTM.trace t choices (W.toNTM.initCfg x)

theorem Complexity.WitnessTM.exists_trace_eq_run_internal {k : ℕ} (W : WitnessTM k) (x : List Bool) (t : ℕ) (g : ℕ → Bool) : ∃ (choices : Fin t → Bool), W.toNTM.trace t choices (W.toNTM.initCfg x) = NTM.dropChoice (W.run x g t)

theorem Complexity.WitnessTM.exists_run_iff_internal {k : ℕ} (W : WitnessTM k) (x : List Bool) (t : ℕ) (P : Cfg k W.machine.Q → Prop) : (∃ (g : ℕ → Bool), P (NTM.dropChoice (W.run x g t))) ↔ ∃ (choices : Fin t → Bool), P (W.toNTM.trace t choices (W.toNTM.initCfg x))

theorem Complexity.WitnessTM.forall_run_iff_internal {k : ℕ} (W : WitnessTM k) (x : List Bool) (t : ℕ) (P : Cfg k W.machine.Q → Prop) : (∀ (g : ℕ → Bool), P (NTM.dropChoice (W.run x g t))) ↔ ∀ (choices : Fin t → Bool), P (W.toNTM.trace t choices (W.toNTM.initCfg x))

theorem Complexity.WitnessTM.decidesInTime_iff_internal {k : ℕ} (W : WitnessTM k) (L : Language) (T : ℕ → ℕ) : W.DecidesInTime L T ↔ W.toNTM.DecidesInTime L T

theorem Complexity.WitnessTM.decidesInTimeSpace_iff_internal {k : ℕ} (W : WitnessTM k) (L : Language) (T S : ℕ → ℕ) : W.DecidesInTimeSpace L T S ↔ W.toNTM.DecidesInTimeSpace L T S

theorem Complexity.NTM.toNTM_toWitnessTM_internal {k : ℕ} (N : NTM k) : N.toWitnessTM.toNTM = N