A partial function is lambda-definable if and only if it is partial recursive

Assume $f$ is partial recursive. By [L2], it is built from the initial arithmetic functions by composition, primitive recursion, and minimization. The initial functions are represented by the standard lambda terms for zero, successor, and projections; composition is represented by term substitution; primitive recursion is represented by the usual iterator on Church numerals; and minimization is represented by a fixpoint term that performs the unbounded search $y=0,1,2,\dots$ until a zero-test succeeds. Hence some lambda term represents $f$ in the sense of [L1].

Conversely, assume $f$ is lambda-definable. By [L1], there is a lambda term $F$ such that $F\overline{n_1}\cdots \overline{n_k}$ reaches a Church numeral exactly on the tuples where $f$ is defined, and the numeral reached is its value. Given the sequence code of $(n_1,\dots ,n_k)$, a Turing machine uses [L4] to recover the coordinates, forms that application, and performs a breadth-first search through all finite beta-reduction sequences, halting when a branch reaches a Church numeral. This computes the unary coded version of $f$, so [L3] makes that coded function partial recursive. Composing with the primitive-recursive tuple coder from [L5] and coordinate readers from [L4] makes the original $k$-ary $f$ partial recursive.

Steps 1.1 and 1.2 prove both directions, so lambda-definability and partial recursiveness are equivalent for $f$.