The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification
arXiv:2512.00081
Abstract
We mechanize an orientation boundary for first-order rewrite systems with step-duplicating recursors, using the Right-Duplicating Recursor Schema . For a reflected scalar grammar over counter and payload coordinates with constants, sums, products, pointwise maxima, and natural scalar multiples, Lean proves . On the counter-admissible subclass, orientation is equivalent to payload blindness. The counter projection inhabits the class; the payload-blind constant-zero expression fails counter strictness and orientation, showing the restriction is necessary. A vector extension makes payload blindness necessary whenever strict comparison forces nonincrease of a grammar-expressible scalarization. Twelve scalar and tracked-vector families form the witness-bearing barrier basis, and 80 root-level exclusions lift to context-closed rewriting under their original hypotheses. An escape trichotomy shows that every successful orienter in the stated universe must abandon wrapper-subterm sensitivity, successor transparency, or the formalized families; dependency-pair, nonlinear-polynomial, and multiset-path-order witnesses realize the escape side. For a concrete calculus, Lean certifies strong normalization and confluence of the guarded relation, termination results for the unguarded system, executable normalization and reachability procedures, derivation-length bounds, and ordinal calibrations. Three TTT2 termination proofs receive CeTA 2.36 certification. Machine-checked ledgers close the stated 76-family syntactic universe and a separate 16-row semantic universe. This is an object-level classification for a fixed terminating system and explicit measure classes, not a class-wide undecidability theorem.
78 pages. The Lean 4 formalization and certified TTT2/CeTA artifacts are available at https://github.com/MosesRahnama/The-Orientation-Boundary