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

TL;DR

This paper formalizes the orientation boundary for first-order step-duplicating recursors, establishing impossibility results, escape mechanisms, and certification methods within Lean 4, advancing the understanding of termination and measure-based proofs.

Contribution

It introduces a comprehensive formal framework for the orientation boundary of step-duplicating recursors, including new meta-theorems, impossibility results, and certified proof techniques in Lean 4.

Findings

Excluded twelve base direct-measure classes in Lean 4

Proved all payload-erasing semantic direct measures are counter-dominated

Developed a guarded fragment with strong normalization and exact ordinal calibration

Abstract

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 $\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.