Pairing and relation predicates

This file defines a simple injective pairing pair : List Bool → List Bool → List Bool used to encode (x, y) as a single binary string for verification by a TM, along with the shared predicates PolyBalanced and pairLang used by FNP, FNL, and other search-problem classes.

def Complexity.pair (x y : List Bool) : List Bool

Encode a pair of binary strings as a single binary string. Each bit of x is doubled (false ↦ [false, false], true ↦ [true, true]), followed by the separator [false, true], followed by y verbatim. This encoding is injective and computable in linear time.

Equations

• Complexity.pair x y = List.flatMap (fun (b : Bool) => [b, b]) x ++ [false, true] ++ y

def Complexity.unpair? : List Bool → Option (List Bool × List Bool)

Partial inverse to pair. It scans doubled bits until the first separator [false, true], returning the decoded left component together with the remaining suffix. Invalid doubled prefixes return none.

Equations

• Complexity.unpair? [] = none
• Complexity.unpair? (false :: true :: y) = some ([], y)
• Complexity.unpair? (false :: false :: z) = Option.map (fun (xy : List Bool × List Bool) => (false :: xy.1, xy.2)) (Complexity.unpair? z)
• Complexity.unpair? (true :: true :: z) = Option.map (fun (xy : List Bool × List Bool) => (true :: xy.1, xy.2)) (Complexity.unpair? z)
• Complexity.unpair? x✝ = none

theorem Complexity.pair_cons_eq (b : Bool) (x y : List Bool) : pair (b :: x) y = b :: b :: pair x y

One step of the doubling encoder: pair on b :: x prepends the doubled bit b, b.

@[simp]

theorem Complexity.pair_length (x y : List Bool) : (pair x y).length = 2 * x.length + 2 + y.length

|pair x y| = 2·|x| + 2 + |y|. The 2·|x| comes from doubling every bit of x; the +2 is the separator [false, true].

theorem Complexity.pair_inj {x₁ x₂ y₁ y₂ : List Bool} (h : pair x₁ y₁ = pair x₂ y₂) : x₁ = x₂ ∧ y₁ = y₂

pair is injective: if pair x₁ y₁ = pair x₂ y₂ then x₁ = x₂ and y₁ = y₂.

@[simp]

theorem Complexity.unpair?_pair (x y : List Bool) : unpair? (pair x y) = some (x, y)

unpair? is a left inverse of pair: decoding an encoded pair recovers exactly its two components.

theorem Complexity.eq_pair_of_unpair?_eq_some {z x y : List Bool} (h : unpair? z = some (x, y)) : z = pair x y

Soundness of the decoder: if unpair? succeeds on z, producing (x, y), then z was exactly the encoding pair x y.

theorem Complexity.unpair?_eq_some_iff {z x y : List Bool} : unpair? z = some (x, y) ↔ z = pair x y

unpair? z returns some (x, y) if and only if z = pair x y, characterizing exactly which strings are valid pair encodings.

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, etc.

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 (verification language) of a binary relation R: the set of encoded pairs pair(x, y) such that 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}

theorem Complexity.pair_getElem_left_first (x y : List Bool) (i : ℕ) (hi : i < x.length) : (pair x y)[2 * i] = x[i]

In pair x y, the first duplicated copy of x[i] sits at position 2*i.

theorem Complexity.pair_getElem_left_second (x y : List Bool) (i : ℕ) (hi : i < x.length) : (pair x y)[2 * i + 1] = x[i]

In pair x y, the second duplicated copy of x[i] sits at position 2*i+1.

theorem Complexity.pair_getElem_sep_zero (x y : List Bool) : (pair x y)[2 * x.length] = false

The first separator bit in pair x y is false.

theorem Complexity.pair_getElem_sep_one (x y : List Bool) : (pair x y)[2 * x.length + 1] = true

The second separator bit in pair x y is true.

theorem Complexity.pair_getElem_right (x y : List Bool) (j : ℕ) (hj : j < y.length) : (pair x y)[2 * x.length + 2 + j] = y[j]

In pair x y, the suffix after the separator is exactly y.