Polynomial-time verifiers give NP membership

This is the language-independent entry point for linear and polynomially bounded witnesses. Linear witnesses use the proved finite-certificate compiler; arbitrary polynomial bounds reduce to the linear case by polynomial-time padding. Neither route imports a SAT-specific machine.

Clients needing only linear witnesses can import Complexitylib.Classes.NP.Verifier.Linear to avoid the padding infrastructure. Exact theorems about the older concrete machine remain available separately in Complexitylib.SAT.GuessVerify.

theorem Complexity.mem_NP_of_poly_witness {L L₀ : Language} (p : Polynomial ℕ) (hL₀ : L₀ ∈ P) (hbal : ∀ (x y : List Bool), pair x y ∈ L₀ → y.length ≤ Polynomial.eval x.length p) (hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), pair x y ∈ L₀) : L ∈ NP

Guess and verify with polynomial witnesses. A polynomial-time verifier whose accepted certificates have polynomially bounded length places its existential language in NP.