The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification

We formalize the orientation boundary for first-order step-duplicating recursors, centered on the Right-Duplicating Recursor Schema (RDRS), $\mathrm{r}\mathrm{e}\mathrm{c}\mathrm{u}\mathrm{r}(b,s,\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(n))\to \mathrm{w}\mathrm{r}\mathrm{a}\mathrm{p}(s,\mathrm{r}\mathrm{e}\mathrm{c}\mathrm{u}\mathrm{r}(b,s,n))$. In Lean 4, the no-go side excludes twelve base direct-measure classes (two unconditional, six scalar growth, four tracked vector / pair), with arctic / tropical matrix continuations, a WPO-facing polynomial-branch corollary, and a KBO obstruction. Four meta-theorems organize the stack: projected-primary dominance, scalar-projection lift, mixed-matrix scalarization, and the symbolic comparator barrier. The surface spans 72 schema-level dup-step impossibilities and 80 concrete-system global-step theorems, with a 76-row RDRS method-universe closeout and a semantic capstone proving every payload-erasing semantic direct measure is counter-dominated. The successful side carries a transparency-essentiality witness, a dependency-pair projection escape, a generalized polynomial barrier under frozen-base failure, computable witness extractors, a coefficient-table decision procedure, and mutual-recursion / synchronized-SCC barriers. The witness calculus KO7 has a two-layer chain. Its guarded fragment is strongly normalizing, root-confluent, and normalizable, with single-exponential contextual derivation bounds and an exact ${\omega }^{\omega }$ ordinal calibration below ${\omega }^{\omega }\cdot 2$. The full unguarded system is root-terminating via a nonlinear polynomial witness and a specialized MPO, with context-closed strong normalization lifted through every constructor position. A checked TPDB export and a Lean-side replay of the FAST certificate connect the development to TTT2 / CeTA. To our knowledge, this is the first mechanized object-level barrier theorem on a fixed terminating system, proved without reductions or undecidability arguments.