Linear witnesses give NP membership #
The generic finite-certificate compiler computes the |x| + 1 bound, stores a
certificate on charged work tape, builds the paired virtual input, and runs the
verifier. Online-witness equivalence supplies an NTM with the compiler's explicit
resource bounds. This module does not import SAT or polynomial-padding machinery.
theorem
Complexity.mem_NP_of_linear_witness_internal
{L L₀ : Language}
(hL₀ : L₀ ∈ P)
(hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), y.length ≤ x.length + 1 ∧ pair x y ∈ L₀)
:
Guess and verify. A language whose members are exactly the inputs
carrying a certificate of length at most |x| + 1 that a polynomial-time
verifier accepts is in NP.