Fixed-arity inputs for Cobham's characterization

FP is defined for unary string functions, while Cobham's algebra is inherently multi-arity. This module gives the public, auditable bridge: encodeVec packs a fixed-arity argument vector into one string, vectorLength measures its unencoded size, and FPn asks a unary FP function to agree on the encoded vectors.

The nested pairing has an arity-dependent constant overhead. It is injective, and for every fixed arity its encoded length is linear in vectorLength.

Main definitions and results

• Cobham.encodeVec — nested-pairing tuple encoding, head component last
• Cobham.vectorLength — sum of the component lengths
• Cobham.encodeVec_injective — tuple encoding loses no information
• Cobham.encodeVec_length_le — fixed-arity linear length bound
• Cobham.FPn — polynomial time on encoded argument vectors

def Complexity.Cobham.encodeVec {n : ℕ} : (Fin n → List Bool) → List Bool

Encode an argument vector as a single bitstring by nested pairing, with the head component placed in the verbatim suffix: encodeVec ![] = [] and encodeVec (x ::ᵥ v) = pair (encodeVec v) x.

Equations

• Complexity.Cobham.encodeVec x_2 = []
• Complexity.Cobham.encodeVec v = Complexity.pair (Complexity.Cobham.encodeVec (Fin.tail v)) (v 0)

@[simp]

theorem Complexity.Cobham.encodeVec_zero (v : Fin 0 → List Bool) : encodeVec v = []

@[simp]

theorem Complexity.Cobham.encodeVec_succ {n : ℕ} (v : Fin (n + 1) → List Bool) : encodeVec v = pair (encodeVec (Fin.tail v)) (v 0)

theorem Complexity.Cobham.encodeVec_one (v : Fin 1 → List Bool) : encodeVec v = pair [] (v 0)

The arity-one encoding is the single component placed in the verbatim suffix of an empty block: encodeVec ![x] = pair [] x.

def Complexity.Cobham.vectorLength {n : ℕ} (v : Fin n → List Bool) : ℕ

The sum of the component lengths of a fixed-arity input vector.

Equations

• Complexity.Cobham.vectorLength v = ∑ i : Fin n, (v i).length

@[simp]

theorem Complexity.Cobham.vectorLength_zero (v : Fin 0 → List Bool) : vectorLength v = 0

@[simp]

theorem Complexity.Cobham.vectorLength_succ {n : ℕ} (v : Fin (n + 1) → List Bool) : vectorLength v = (v 0).length + vectorLength (Fin.tail v)

theorem Complexity.Cobham.encodeVec_length_succ {n : ℕ} (v : Fin (n + 1) → List Bool) : (encodeVec v).length = 2 * (encodeVec (Fin.tail v)).length + 2 + (v 0).length

Exact recursive length law for the nested tuple encoding.

theorem Complexity.Cobham.encodeVec_injective {n : ℕ} : Function.Injective encodeVec

encodeVec is injective at every arity.

theorem Complexity.Cobham.encodeVec_length_le {n : ℕ} (v : Fin n → List Bool) : (encodeVec v).length ≤ 2 ^ n * (vectorLength v + 2 * n)

For fixed arity n, the nested encoding has length linear in the sum of the component lengths. The explicit coefficient also records that this is not a uniform-in-arity linear bound.

def Complexity.Cobham.FPn {n : ℕ} (f : (Fin n → List Bool) → List Bool) : Prop

Multi-arity polynomial time. A function of an argument vector is FPn when some genuine unary FP function computes it on encoded vectors.

Equations

• Complexity.Cobham.FPn f = ∃ g ∈ Complexity.FP, ∀ (v : Fin n → List Bool), g (Complexity.Cobham.encodeVec v) = f v