The rewrite rule \[ \mathrm{recur}(b,s,\mathrm{succ}(n))\to \mathrm{wrap}(s,\mathrm{recur}(b,s,n)) \] copies its step argument, the payload, and consumes one recursion counter. It terminates; we ask which direct measures prove it. For measures built from counter and payload by constants, sums, products, maxima, and natural scalar multiples, those that orient every root successor step of the free recursor are those that ignore the payload and increase strictly with the counter. This set is the Orientation Boundary. The mechanism compares the cost of the copied payload with the gain per counter step: every natural-valued measure of any shape (linear, polynomial, matrix, or other) that keeps both wrapper arguments with bounded counter gain fails, and twelve direct measure families fail by this comparison under their hypotheses. Termination is proved by violating a barrier hypothesis or using information outside the direct classes: dependency-pair projection, nonlinear counter-payload coupling, or a path order. Seventy-six termination methods from the literature receive a machine-checked termination verdict on the free recursor. For constructor-local natural polynomial interpretations of any degree, orientation of the two free-recursor rules is decidable at unit successor slope, and at higher slopes its undecided remainder contains the open zero problem for two-variable integer polynomials over $\mathbb N^2$. The free recursor is strongly normalizing and confluent under all contexts, so orientation separates from termination. Every numbered result is machine-checked in Lean~4; TTT2 and CeTA certify the free recursor and a fixed system containing it, and the barrier theorems predict the MAYBE answers of TTT2's Knuth-Bendix strategy there, and of its matrix strategies when both wrapper matrices have a positive diagonal entry at a tracked coordinate.

翻译：暂无翻译