← All papers
First page of The Orientation Boundary for Step-Duplicating Recursors: A Machine-Checked Structural Theory of Termination Proofs

The Orientation Boundary for Step-Duplicating Recursors: A Machine-Checked Structural Theory of Termination Proofs

Moses Rahnama

cs.LO Nov 26, 2025 · v12 math.LO
All numbered results on orientation barriers, termination, normalization and confluence of a step-duplicating recursor rewrite system are machine-checked in Lean 4.
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.

The rewrite rule recur(b,s,succ(n)) → wrap(s,recur(b,s,n)) duplicates its step argument. The paper asks which direct termination measures can orient it and why simple additive or polynomial measures fail.

Defines a minimal operator-only rewrite calculus (KO7) and proves strong normalization of a guarded safe fragment using a triple-lexicographic measure with a Dershowitz–Manna multiset component and an MPO-style head precedence. Builds a certified normalizer by well-founded recursion and proves confluence via Newman's Lemma using per-shape local-join lemmas. Proves impossibility (barrier) theorems for broad classes of measures under duplication. Mechanizes everything in Lean 4 and cross-checks the free recursor with TTT2 and CeTA.

For measures built from sums, products, maxima and scalars, exactly those that ignore the payload and increase strictly with the counter orient the rule. Seventy-six literature termination methods receive a machine-checked verdict. Orientation by natural polynomial interpretations is decidable at unit successor slope, while at higher slopes the undecided remainder contains an open problem. The barrier theorems predict TTT2's MAYBE answers for its Knuth-Bendix strategy and, under a stated diagonal condition, for its matrix strategies.