Paired relation predicates

This file adds the complexity-class predicates built on the neutral binary pairing codec from Complexitylib.Encoding.Pairing.

def Complexity.PolyBalanced (R : List Bool → List Bool → Prop) : Prop

A binary relation is polynomially balanced if witness length is bounded by a polynomial in the input length. This is the standard short-witness condition used in the definitions of NP, FNP, FNL, and related classes.

Equations

• Complexity.PolyBalanced R = ∃ (p : Polynomial ℕ), ∀ (x y : List Bool), R x y → y.length ≤ Polynomial.eval x.length p

def Complexity.pairLang (R : List Bool → List Bool → Prop) : Language

The pair language of R contains exactly the encodings pair x y for which R x y holds.

Equations

• Complexity.pairLang R = {z : List Bool | ∃ (x : List Bool) (y : List Bool), z = Complexity.pair x y ∧ R x y}

@[simp]

theorem Complexity.mem_pairLang_pair (R : List Bool → List Bool → Prop) (x y : List Bool) : pair x y ∈ pairLang R ↔ R x y

Membership of a canonically encoded pair reduces to the underlying binary relation.