The multi-arity bridge — proof internals

The public tuple encoding and FPn predicate live in Complexitylib.Classes.P.Cobham.Vec. This internal module supplies the concrete FP building blocks used to connect their arity-one specialization to FP.

Main results

• Cobham.const_nil_mem_FP, Cobham.pairLeftNil_mem_FP — the two FP maps the arity-one glue needs

Foundational FP building blocks

theorem Complexity.Cobham.const_nil_mem_FP : (fun (x : List Bool) => []) ∈ FP

The constant empty-output function is in FP (the empty-support case of ite_mem_finset_mem_FP).

theorem Complexity.Cobham.pairLeftNil_mem_FP : (fun (x : List Bool) => pair [] x) ∈ FP

The framing map x ↦ pair [] x (i.e. false :: true :: x) is polynomial-time. This is the foundational map behind the arity-one encoding encodeVec ![x] = pair [] x, and it is exactly mem_FP_pairWithInput applied to the constant empty function.