Correctness of the ordinary finite-verifier compiler

The initialized prefix and deterministic suffix form one concrete witness machine. Every stream halts, every accepted run has a permitted certificate, and every permitted accepting certificate is generated by some stream.

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

A time-bounded deterministic decider obeys the same bound in decision space.

theorem Complexity.WitnessTM.Verifier.compile_contract_internal {r : ℕ} {bound : ℕ → ℕ} {k : ℕ} (setup : WitnessBoundSetup r bound) (M : TM k) {L : Language} {T S : ℕ → ℕ} (hM : M.DecidesInTimeSpace L T S) (x : List Bool) : (compile setup M).machine.HoareTime (prefixEntry r k x) (fun (x_1 : Tape) (x_2 : Fin (tapes r k + 1) → Tape) (out : Tape) => ∃ (y : List Bool), y.length ≤ bound x.length ∧ (pair x y ∈ L → out.cells 1 = Γ.one) ∧ (pair x y ∉ L → out.cells 1 = Γ.zero)) (time setup T x.length) ∧ (compile setup M).machine.HoareSafety (prefixEntry r k x) fun (inp : Tape) (work : Fin (tapes r k + 1) → Tape) (out : Tape) => { state := (), input := inp, work := fun (i : Fin (tapes r k)) => work i.castSucc, output := out }.WithinDecisionSpace x.length (space setup S x.length)

Concrete full-pipeline time and all-reachable projected space contracts.

theorem Complexity.WitnessTM.Verifier.compile_run_verdict_internal {r : ℕ} {bound : ℕ → ℕ} {k : ℕ} (setup : WitnessBoundSetup r bound) (M : TM k) {L : Language} {T S : ℕ → ℕ} (hM : M.DecidesInTimeSpace L T S) (x : List Bool) (g : ℕ → Bool) : have c := (compile setup M).run x g (time setup T x.length); (compile setup M).machine.halted c ∧ ∃ (y : List Bool), y.length ≤ bound x.length ∧ (pair x y ∈ L → c.output.cells 1 = Γ.one) ∧ (pair x y ∉ L → c.output.cells 1 = Γ.zero)

Every completed stream run has the verifier's verdict for a bounded certificate.

theorem Complexity.WitnessTM.Verifier.compile_accepts_of_certificate_internal {r : ℕ} {bound : ℕ → ℕ} {k : ℕ} (setup : WitnessBoundSetup r bound) (M : TM k) {L : Language} {T S : ℕ → ℕ} (hM : M.DecidesInTimeSpace L T S) (x y : List Bool) (hy : y.length ≤ bound x.length) (hyes : pair x y ∈ L) : (compile setup M).AcceptsInTime x (time setup T x.length)

A chosen accepting finite certificate yields an accepting initialized run.

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

The certificate-storing compiler realizes bounded existential verification with the explicit independent time and charged-space formulas.