A new method of "minimal" realizability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)--functions $f$ such that HA $\vdash \forall x\exists!yA(x, y)\Rightarrow$ for all $m, A(m, f(m))$ is true, where $A(x, y)$ may be an arbitrary formula of $\mathscr{L}$(HA) with only $x, y$ free--are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the $< \varepsilon_0$-recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be $< \varepsilon_0$-recursive. The method is extended to intuitionistic finite-type arithmetic, $HA^\omega_0$, and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived.