Polynomial-time computation on a regular input domain

A DFA guard extends a binary CSLib computation to all strings, returning empty output outside its regular domain. Only accepted inputs need source runtime bounds, since rejection never starts the source machine.

theorem Complexity.CslibGuard.computes_accepted {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) {w output : List Bool} {t s : ℕ} (hw : w ∈ D.accepts) (h : M.ComputesInTimeAndSpace w output t s) : (machine M D).ComputesInTimeAndSpace w output (2 * w.length + t + 2) (Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg w) (2 * w.length + t + 2))

Accepted inputs incur just linear validation and rewind overhead.

theorem Complexity.CslibGuard.computes_rejected {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) {w : List Bool} (hw : w ∉ D.accepts) : (machine M D).ComputesInTimeAndSpace w [] (w.length + 1) (Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg w) (w.length + 1))

Rejected inputs halt with empty output after a single scan.

theorem Complexity.CslibGuard.mem_FP_on_dfa {k : ℕ} {σ Q : Type} [Fintype σ] [Fintype Q] (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) [DecidablePred fun (x : List Bool) => x ∈ D.accepts] {f : List Bool → List Bool} {p : Polynomial ℕ} (h : ∀ w ∈ D.accepts, ∃ t ≤ Polynomial.eval w.length p, ∃ (s : ℕ), M.ComputesInTimeAndSpace w (f w) t s) : (fun (w : List Bool) => if w ∈ D.accepts then f w else []) ∈ FP

Polynomial source bounds on a regular domain give a total canonical FP function.