FNP and TFNP #
This file defines the function/search complexity classes FNP and TFNP
(see FNP/Defs.lean) and proves the fundamental connection between TFNP and
NP ∩ coNP: if a language has both NP and coNP witness relations, the combined
certificate-finding problem is in TFNP (Megiddo–Papadimitriou 1991).
theorem
Complexity.orRelation_mem_TFNP_of_NP_coNP_witnesses
{R₁ R₂ : List Bool → List Bool → Prop}
{L : Language}
(hR₁ : R₁ ∈ FNP)
(hR₂ : R₂ ∈ FNP)
(h_mem : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), R₁ x y)
(h_nmem : ∀ (x : List Bool), x ∉ L ↔ ∃ (y : List Bool), R₂ x y)
:
NP ∩ coNP yields TFNP (Megiddo–Papadimitriou 1991): given FNP relations
R₁ (witnesses for x ∈ L) and R₂ (witnesses for x ∉ L), the combined
relation is in TFNP. Any witness valid for either component serves as a
solution to the combined search problem.
Combined with the NP witness theorem
(NP = {L | ∃ R ∈ FNP, ∀ x, x ∈ L ↔ ∃ y, R x y}),
this establishes that every language in NP ∩ coNP gives rise to a TFNP
search problem.