Finite verification with explicit time and space

A concrete bound-setup machine and an ordinary paired-input verifier compile to a witness machine that stores its certificate on charged work tape. Both resource bounds include initialization and the paired virtual input. Reusing that certificate is permitted because its stored copy is ordinary workspace.

Verifier.compile_decidesInTimeSpace is uniform over arbitrary realized bound functions; finite maxima avoid monotonicity assumptions on the verifier's resource bounds. Exact online-witness equivalence then gives the corresponding NTM with the same compiler bounds. Polynomial witness theorems are downstream.

theorem Complexity.TM.decidesInTimeSpace_of_decidesInTime {k : ℕ} {M : TM k} {L : Language} {T : ℕ → ℕ} (hM : M.DecidesInTime L T) : M.DecidesInTimeSpace L T T

A deterministic time bound also bounds every charged decision-space prefix.

theorem Complexity.WitnessTM.Verifier.compile_decidesInTimeSpace {r : ℕ} {bound : ℕ → ℕ} {k : ℕ} (setup : WitnessBoundSetup r bound) (M : TM k) {L : Language} {T S : ℕ → ℕ} (hM : M.DecidesInTimeSpace L T S) : (compile setup M).DecidesInTimeSpace (language bound L) (time setup T) (space setup S)

An ordinary finite verifier and realized bound yield a concrete stored- certificate witness machine, with explicit independent resource bounds.

theorem Complexity.WitnessTM.Verifier.compile_decidesInTime {r : ℕ} {bound : ℕ → ℕ} {k : ℕ} (setup : WitnessBoundSetup r bound) (M : TM k) {L : Language} {T : ℕ → ℕ} (hM : M.DecidesInTime L T) : (compile setup M).DecidesInTime (language bound L) (time setup T)

The finite verifier compiler also applies when only time is being tracked.