Polynomial witness bounds by padding

The linear-witness theorem is provided by the generic finite-verifier compiler through Complexitylib.Classes.NP.Verifier.Linear. Polynomial witness bounds reduce to that case by padding until the witness bound is linear in input size. This implementation has no SAT dependency. The public membership theorem is in Complexitylib.Classes.NP.Verifier, and Classes.NP.WitnessConstruction uses it to prove the FNP-to-NP corollaries.

Any polynomial witness bound

noncomputable def Complexity.padWith (p : Polynomial ℕ) (x : List Bool) : List Bool

The input padded with a ruler long enough to make the witness bound linear.

Equations

• Complexity.padWith p x = Complexity.pair x (Complexity.polyRuler p x)

theorem Complexity.padWith_mem_FP (p : Polynomial ℕ) : padWith p ∈ FP

noncomputable def Complexity.padVerifier (p : Polynomial ℕ) (L₀ : Language) : Language

The verifier for the padded language: run the original verifier on the unpadded input, and check that the padding really is long enough.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.padVerifier_mem_P {p : Polynomial ℕ} {L₀ : Language} (hL₀ : L₀ ∈ P) : padVerifier p L₀ ∈ P

noncomputable def Complexity.padLang (p : Polynomial ℕ) (L₀ : Language) : Language

The padded language, whose witnesses are short enough for the linear guess-and-verify machine.

Equations

• Complexity.padLang p L₀ = {z : List Bool | ∃ (y : List Bool), y.length ≤ z.length + 1 ∧ Complexity.pair z y ∈ Complexity.padVerifier p L₀}

theorem Complexity.padLang_mem_NP {p : Polynomial ℕ} {L₀ : Language} (hL₀ : L₀ ∈ P) : padLang p L₀ ∈ NP

theorem Complexity.mem_NP_of_poly_witness_internal {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 any polynomial witness bound. A language whose members are exactly the inputs carrying a certificate a polynomial-time verifier accepts is in NP, provided the verifier only accepts certificates of polynomial length.