We formalize the orientation boundary for first-order step-duplicating recursors, centered on the Right-Duplicating Recursor Schema (RDRS), $\mathrm{recur}(b,s,\mathrm{succ}(n))\to\mathrm{wrap}(s,\mathrm{recur}(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 $ω^ω$ ordinal calibration below $ω^ω\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.

翻译：我们形式化了一阶步复制递归子的方向边界，聚焦于右复制递归子模式（RDRS），$\mathrm{recur}(b,s,\mathrm{succ}(n))\to\mathrm{wrap}(s,\mathrm{recur}(b,s,n))$。在 Lean 4 中，否定侧排除了十二个基本的直接度量类（两个无条件类、六个标量增长类、四个追踪向量/对类），涉及北极/热带矩阵续延、一个面向 WPO 的多项式分支推论以及一个 KBO 障碍。四个元定理组织了该体系：投影主支配性、标量投影提升、混合矩阵标量化以及符号比较器障碍。表面层涵盖了 72 个模式级复制步骤不可行性和 80 个具体系统全局步骤定理，包含一个 76 行的 RDRS 方法宇宙收束以及一个语义基石，证明每个负载擦除的语义直接度量均被反支配。肯定侧携带了一个透明本质性见证、一个依赖对投影逃逸、一个冻结基失败下的广义多项式障碍、可计算见证提取器、一个系数表决策过程，以及互递归/同步 SCC 障碍。见证演算 KO7 具有两层链。其保护片段是强规范化的、根合流的且可规范化的，具有单指数上下文推导边界和严格低于 $ω^ω\cdot 2$ 的 $ω^ω$ 序数校准。完整无保护系统通过非线性多项式见证和专用 MPO 实现根终止，并通过每个构造子位置提升上下文闭合的强规范化。一个经过检查的 TPDB 导出和 Lean 端的 FAST 证书重放将该开发与 TTT2/CeTA 相连接。据我们所知，这是首个针对固定终止系统、无需归约或不可判定性论证的机械化对象级障碍定理。