Polynomial time for linear finite-certificate verification

The concrete compiler overhead and its finite verifier-time maximum have a uniform explicit polynomial bound, without assuming verifier-time monotonicity.

theorem Complexity.WitnessTM.Verifier.time_linear_eq (T : ℕ → ℕ) (n : ℕ) : time WitnessBoundSetup.linear T n = 13 * n + 32 + window (fun (n : ℕ) => n + 1) T n

Exact linear setup overhead, including phase handoffs.

theorem Complexity.WitnessTM.Verifier.time_linear_polynomial_bound {T : ℕ → ℕ} {c : ℕ} (hT : BigO T fun (x : ℕ) => x ^ c) : ∃ (q : Polynomial ℕ), ∀ (n : ℕ), time WitnessBoundSetup.linear T n ≤ Polynomial.eval n q

A natural polynomial bound for the verifier induces an explicit polynomial bound for the whole linear-witness compiler, without monotonicity of T.

theorem Complexity.WitnessTM.Verifier.time_linear_bigO_of_bigO {T : ℕ → ℕ} {c : ℕ} (hT : BigO T fun (x : ℕ) => x ^ c) : ∃ (d : ℕ), BigO (time WitnessBoundSetup.linear T) fun (x : ℕ) => x ^ d

The linear-witness compiler preserves polynomial running time.