Linearly bounded polynomial-time verifiers give NP membership

This language-independent entry point uses the proved finite-certificate compiler WitnessTM.Verifier.compile. It imports neither SAT nor the polynomial-padding machinery. mem_NP_of_linear_witness retains its established name and statement; NP.mem_NP_of_linear_witness adapts it to a relation with a verifier in P.

For arbitrary polynomial witness bounds, import Complexitylib.Classes.NP.Verifier. Exact theorems about the older SAT.satGuessVerifyNTM remain available separately from Complexitylib.SAT.GuessVerify; the two machines are not identified.

theorem Complexity.mem_NP_of_linear_witness {L L₀ : Language} (hL₀ : L₀ ∈ P) (hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), y.length ≤ x.length + 1 ∧ pair x y ∈ L₀) : L ∈ NP

Guess and verify. A language characterized by certificates of length at most |x| + 1 accepted by a polynomial-time verifier is in NP.

theorem Complexity.NP.mem_NP_of_linear_witness {R : List Bool → List Bool → Prop} {L : Language} (hbound : ∀ (x y : List Bool), R x y → y.length ≤ x.length + 1) (hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), R x y) (hverify : pairLang R ∈ P) : L ∈ NP

A linearly bounded witness relation with a polynomial-time paired verifier places the language it characterizes in NP.