Witness machines and nondeterministic machines

An online witness machine is equivalent to an NTM with exactly the same time and charged-space bounds. The witness is external, read-only, and consumed left to right; nonconsuming steps cannot inspect it. This theorem does not identify a free two-way certificate tape with ordinary nondeterminism.

NTM.toWitnessTM supplies a witness-machine instance for every NTM. WitnessTM.toNTM removes the distinguished tape. The round trip recovers the original NTM, and both translations preserve acceptance and all-path resource bounds. Bounds are arbitrary functions, with no polynomial or constructibility hypotheses. Witness loading is part of initialization, not a charged computation. run_congr_prefix shows that the first t bits determine the visible t-step run, so infinite streams are only a representation of finite certificates.

theorem Complexity.WitnessTM.run_congr_prefix {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 first t witness bits determine the visible result of t steps. Unread tails need not agree, so a finite certificate of length t suffices.

theorem Complexity.WitnessTM.exists_run_eq_trace {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)

Every NTM trace has a witness run with exactly the same visible endpoint.

theorem Complexity.WitnessTM.exists_trace_eq_run {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)

Every witness run has an NTM trace with exactly the same visible endpoint.

theorem Complexity.WitnessTM.allWitnessesHaltIn_iff {k : ℕ} (W : WitnessTM k) (T : ℕ → ℕ) : W.AllWitnessesHaltIn T ↔ W.toNTM.AllPathsHaltIn T

Uniform halting bounds agree exactly in the two models.

theorem Complexity.WitnessTM.acceptsInTime_iff {k : ℕ} (W : WitnessTM k) (x : List Bool) (t : ℕ) : W.AcceptsInTime x t ↔ W.toNTM.AcceptsInTime x t

Existential acceptance agrees at the same clock, including clock zero.

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

Time-bounded deciding agrees without changing the time bound.

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

A single machine's time and space bounds are preserved simultaneously.

theorem Complexity.WitnessTM.decidesInSpace_iff {k : ℕ} (W : WitnessTM k) (L : Language) (S : ℕ → ℕ) : W.DecidesInSpace L S ↔ W.toNTM.DecidesInSpace L S

Uniformly halting, space-bounded deciding agrees without extra charged space.

theorem Complexity.NTM.decidesInSpace_iff_exists_decidesInTimeSpace {k : ℕ} (N : NTM k) (L : Language) (S : ℕ → ℕ) : N.DecidesInSpace L S ↔ ∃ (T : ℕ → ℕ), N.DecidesInTimeSpace L T S

The simultaneous predicate recovers the existing space-only definition.

@[simp]

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

Supplying then removing the witness stream recovers the original NTM.

theorem Complexity.NTM.toWitnessTM_decidesInTime_iff {k : ℕ} (N : NTM k) (L : Language) (T : ℕ → ℕ) : N.toWitnessTM.DecidesInTime L T ↔ N.DecidesInTime L T

Every NTM has an online witness presentation with the exact same time bound.

theorem Complexity.NTM.toWitnessTM_decidesInTimeSpace_iff {k : ℕ} (N : NTM k) (L : Language) (T S : ℕ → ℕ) : N.toWitnessTM.DecidesInTimeSpace L T S ↔ N.DecidesInTimeSpace L T S

Every NTM has an online witness presentation preserving both resource bounds.

theorem Complexity.NTM.toWitnessTM_decidesInSpace_iff {k : ℕ} (N : NTM k) (L : Language) (S : ℕ → ℕ) : N.toWitnessTM.DecidesInSpace L S ↔ N.DecidesInSpace L S

Every NTM has an online witness presentation with the exact same space bound.