The guess-and-verify NTM construction

This file discharges NP.WitnessNTMConstruction, the machine-construction interface stated in Complexitylib.Classes.NP.Witness. The machine is the generic guess-and-verify NTM behind mem_NP_of_poly_witness: guess a certificate, pair it with the input, and run the deterministic verifier. This file only repackages that theorem. A polynomial-time decider for pairLang R is a verifier in P, the witness-length bound transfers through mem_pairLang_pair, and NP membership unfolds to the required NTM.

With the construction proved, the FNP ⇒ NP direction of the witness characterization holds unconditionally (NP.mem_NP_of_FNP). The converse, that every NP language has an FNP witness relation, is not yet formalized.

Main results

• NP.witnessNTMConstruction — the construction interface holds
• NP.mem_NP_of_FNP — a language characterized by an FNP relation is in NP
• NP.witnessLang_mem_NP — the witness language of an FNP relation is in NP

theorem Complexity.NP.witnessNTMConstruction : WitnessNTMConstruction

The guess-and-verify NTM construction. A polynomial-time DTM deciding pairLang R, together with a polynomial bound on witness length, yields a polynomial-time NTM deciding witnessLang R.

theorem Complexity.NP.mem_NP_of_FNP {R : List Bool → List Bool → Prop} {L : Language} (hR : R ∈ FNP) (hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), R x y) : L ∈ NP

FNP ⇒ NP. If R ∈ FNP and x ∈ L ↔ ∃ y, R x y, then L ∈ NP.

theorem Complexity.NP.witnessLang_mem_NP {R : List Bool → List Bool → Prop} (hR : R ∈ FNP) : witnessLang R ∈ NP

The witness language of an FNP relation is in NP.