pith. sign in

arxiv: 2512.00081 · v10 · pith:V2F6FVEAnew · submitted 2025-11-26 · 💻 cs.LO · math.LO

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

Moses Rahnama This is my paper

Pith reviewed 2026-05-22 12:17 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords term rewritingterminationdirect measuresmechanized proofsrecursorsorientation boundarystep duplicationLean formalization
0
0 comments X

The pith

A specific step-duplicating recursor evades orientation by every payload-erasing direct measure.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper centers on the Right-Duplicating Recursor Schema and proves that no payload-erasing semantic direct measure can orient it. It does so by exhaustively ruling out twelve base classes of measures along with their matrix and polynomial extensions inside a Lean 4 formalization. A sympathetic reader cares because the result supplies the first mechanized object-level barrier theorem for a fixed terminating system that avoids any reduction to undecidability. The development also supplies escape routes via witnesses and extractors on the positive side.

Core claim

The Right-Duplicating Recursor Schema cannot be oriented by any of the twelve base direct-measure classes, their arctic and tropical matrix continuations, or the WPO-facing polynomial-branch corollary. This yields 72 schema-level impossibilities and 80 concrete-system global-step theorems, organized by four meta-theorems and capped by a semantic proof that every payload-erasing direct measure is counter-dominated by the schema.

What carries the argument

The Right-Duplicating Recursor Schema (RDRS), written recur(b,s,succ(n)) → wrap(s, recur(b,s,n)), which functions as the fixed object whose termination orientation is bounded from above and below.

If this is right

  • The RDRS schema lies outside the reach of all examined unconditional, scalar-growth, and tracked-vector direct measures.
  • A transparency-essentiality witness together with a dependency-pair projection supplies an explicit escape from the barrier.
  • Computable witness extractors and a coefficient-table decision procedure certify successful orientations when they exist.
  • Mutual-recursion and synchronized-SCC barriers extend the same impossibility results to larger systems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same exhaustive style of mechanized boundary analysis could be applied to other fixed recursive patterns that appear in practical term-rewriting problems.
  • The KO7 witness calculus with its ordinal calibration might transfer to termination proofs for related guarded recursion schemes outside the original schema.
  • Connecting the Lean development to external tools such as TTT2 and CeTA suggests a practical route for exporting certified termination results for duplicating systems.

Load-bearing premise

The twelve base direct-measure classes together with arctic and tropical matrix continuations and the WPO polynomial-branch corollary already cover every relevant direct measure that could possibly orient the schema.

What would settle it

Discovery of any direct measure outside the twelve classes and listed continuations that successfully orients even one concrete instance of the RDRS schema would falsify the no-go claim.

Figures

Figures reproduced from arXiv: 2512.00081 by Moses Rahnama.

Figure 1
Figure 1. Figure 1: Auxiliary triple-lex components. Duplicators decrease via [PITH_FULL_IMAGE:figures/full_fig_p022_1.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper formalizes in Lean 4 the orientation boundary for first-order step-duplicating recursors, centered on the Right-Duplicating Recursor Schema (RDRS) recur(b,s,succ(n)) → wrap(s,recur(b,s,n)). On the no-go side it excludes twelve base direct-measure classes (two unconditional, six scalar growth, four tracked vector/pair) together with arctic/tropical matrix continuations, a WPO-facing polynomial-branch corollary and a KBO obstruction, organized by four meta-theorems (projected-primary dominance, scalar-projection lift, mixed-matrix scalarization, symbolic comparator barrier). This yields 72 schema-level dup-step impossibilities, 80 global-step theorems and a 76-row method-universe closeout whose semantic capstone asserts that every payload-erasing semantic direct measure is counter-dominated by RDRS. The positive side supplies a transparency-essentiality witness, dependency-pair projection escape, KO7 witness calculus (guarded fragment strongly normalizing with ω^ω ordinal bound; full system root-terminating via nonlinear polynomial witness and MPO), computable extractors, and certification via checked TPDB export plus Lean replay of a FAST certificate.

Significance. If the central claims hold, the work supplies the first mechanized object-level barrier theorem for a fixed terminating system proved without reductions or undecidability arguments. The scale of the Lean development (72+80 theorems, 76-row closeout) together with the external-tool connection (TPDB/FAST to TTT2/CeTA) and the constructive KO7 escape with explicit ordinal calibration constitute a substantial, reproducible contribution to termination theory for recursive schemas.

major comments (1)
  1. [No-go side organization and semantic capstone] No-go organization and semantic capstone: the universal quantifier that every payload-erasing semantic direct measure is counter-dominated rests on the claim that the twelve base classes plus arctic/tropical continuations, WPO polynomial corollary and KBO obstruction exhaust the relevant space. The modeling choice is stated, yet no independent meta-argument is supplied showing that all conceivable growth or tracking structures (including non-monotonic or context-sensitive projections not reducible to projected-primary dominance or mixed-matrix scalarization) fall inside this taxonomy; this is load-bearing for the capstone theorem.
minor comments (1)
  1. [Abstract] Abstract: the precise statement of the semantic capstone theorem and the exact handling of mixed-matrix scalarization are not spelled out, which would help readers assess the scope of the impossibility results.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed and constructive report, including the positive assessment of the mechanization's scale and the first object-level barrier result. We address the single major comment below on the no-go organization and semantic capstone.

read point-by-point responses

  1. Referee: No-go organization and semantic capstone: the universal quantifier that every payload-erasing semantic direct measure is counter-dominated rests on the claim that the twelve base classes plus arctic/tropical continuations, WPO polynomial corollary and KBO obstruction exhaust the relevant space. The modeling choice is stated, yet no independent meta-argument is supplied showing that all conceivable growth or tracking structures (including non-monotonic or context-sensitive projections not reducible to projected-primary dominance or mixed-matrix scalarization) fall inside this taxonomy; this is load-bearing for the capstone theorem.

    Authors: We agree that the manuscript states the modeling choice without supplying a separate, fully general meta-proof that the taxonomy is exhaustive over every conceivable structure. The four meta-theorems (projected-primary dominance, scalar-projection lift, mixed-matrix scalarization, symbolic comparator barrier) are intended to cover the forms of payload-erasing semantic direct measures standard in the termination literature, where measures are required to be monotonic with respect to the underlying order and to act via projections or scalar/matrix interpretations. Non-monotonic or context-sensitive projections fall outside this standard class and are typically addressed by other methods (e.g., dependency-pair frameworks) rather than direct measures. To make the scope and load-bearing assumptions explicit, we will add a short clarifying subsection that restates the definition of the considered measure class and shows how the meta-theorems together imply coverage within that class. This constitutes a partial revision that strengthens presentation without altering the technical claims. revision: partial

Circularity Check

0 steps flagged

Self-contained mechanized formalization with external tool validation

full rationale

The paper presents a Lean 4 formalization of the orientation boundary for the RDRS schema. The no-go side excludes twelve base direct-measure classes (two unconditional, six scalar growth, four tracked vector/pair) lifted via arctic/tropical matrix continuations, a WPO-facing polynomial-branch corollary, and a KBO obstruction, organized by four meta-theorems (projected-primary dominance, scalar-projection lift, mixed-matrix scalarization, symbolic comparator barrier). The successful side supplies transparency-essentiality witnesses, dependency-pair projections, generalized polynomial barriers, coefficient-table decision procedures, and mutual-recursion barriers. It includes a checked TPDB export and Lean-side replay of the FAST certificate connecting to TTT2/CeTA. As a self-contained mechanized development against external termination tools, with the modeling choice for payload-erasing semantic direct measures stated explicitly in the no-go organization and 76-row closeout, no central claim reduces by construction to a fitted parameter, self-citation loop, or input definition. The derivation chain is independent and externally anchored.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The development rests on standard Lean mathematics for ordinals, termination orders, and rewriting theory; no ad-hoc free parameters or invented entities are introduced beyond the RDRS schema itself.

axioms (2)
  • standard math Standard properties of ordinals and well-founded orders in Lean
    Invoked for the exact ω^ω ordinal calibration and strong normalization proofs.
  • domain assumption Soundness of the dependency-pair framework and matrix interpretations
    Used in the arctic/tropical continuations and MPO witness.

pith-pipeline@v0.9.0 · 5880 in / 1413 out tokens · 37897 ms · 2026-05-22T12:17:29.105445+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

20 extracted references · 20 canonical work pages

  1. [1]

    Termination of term rewriting using dependency pairs

    Thomas Arts and J¨ urgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1–2):133–178, 2000

    work page 2000

  2. [2]

    Small term reachability and related problems for termi- nating term rewriting systems.Logical Methods in Computer Science, 21(4), 2025

    Franz Baader and J¨ urgen Giesl. Small term reachability and related problems for termi- nating term rewriting systems.Logical Methods in Computer Science, 21(4), 2025

    work page 2025

  3. [3]

    Cambridge University Press, 1998

    Franz Baader and Tobias Nipkow.Term Rewriting and All That. Cambridge University Press, 1998

    work page 1998

  4. [4]

    Proof-theoretic analysis of termination proofs.Annals of Pure and Applied Logic, 75(1-2):57–65, 1995

    Wilfried Buchholz. Proof-theoretic analysis of termination proofs.Annals of Pure and Applied Logic, 75(1-2):57–65, 1995

    work page 1995

  5. [5]

    Decidability of reachability for term rewriting systems

    Anne-C´ ecile Caron and Jean-Luc Coquid´ e. Decidability of reachability for term rewriting systems. InRewriting Techniques and Applications (RTA), pages 16–30. Springer, 1994

    work page 1994

  6. [6]

    Termination of rewriting.Journal of Symbolic Computation, 3(1– 2):69–115, 1987

    Nachum Dershowitz. Termination of rewriting.Journal of Symbolic Computation, 3(1– 2):69–115, 1987

    work page 1987

  7. [7]

    Proving termination with multiset orderings.Com- munications of the ACM, 22(8):465–476, 1979

    Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings.Com- munications of the ACM, 22(8):465–476, 1979

    work page 1979

  8. [8]

    Proof-theoretic techniques for term rewriting theory

    Nachum Dershowitz and Mitsuhiro Okada. Proof-theoretic techniques for term rewriting theory. InProceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS), pages 104–111. IEEE, 1988

    work page 1988

  9. [9]

    Maria C. F. Ferreira and Hans Zantema. Well-foundedness of term orderings. InConditional and Typed Rewriting Systems (CTRS 1994), volume 968 ofLecture Notes in Computer Science, pages 106–123. Springer, 1995

    work page 1994

  10. [10]

    Robert W. Floyd. Assigning meanings to programs. InProceedings of Symposia in Applied Mathematics, volume 19, pages 19–32. American Mathematical Society, 1967

    work page 1967

  11. [11]

    Jean H. Gallier. What’s so special about kruskal’s theorem and the ordinalγ 0? a survey of some results in proof theory.Annals of Pure and Applied Logic, 53(3):199–260, 1991

    work page 1991

  12. [12]

    Dependency pairs revisited

    Nao Hirokawa and Aart Middeldorp. Dependency pairs revisited. InRewriting Techniques and Applications (RTA), volume 3091 ofLecture Notes in Computer Science, pages 249–

    work page

  13. [13]

    TTT2: Tyrolean termination tool 2

    Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. TTT2: Tyrolean termination tool 2. InRewriting Techniques and Applications (RTA), volume 5595 of Lecture Notes in Computer Science, pages 295–304. Springer, 2009

    work page 2009

  14. [14]

    Simple termination of rewrite systems.Theoretical Computer Science, 175(1):127–158, 1997

    Aart Middeldorp and Hans Zantema. Simple termination of rewrite systems.Theoretical Computer Science, 175(1):127–158, 1997

    work page 1997

  15. [15]

    On the undecidability of reachability for flat term rewriting systems.IEICE Transactions on Information and Sys- tems, E89-D(2):1000–1007, 2006

    Ichiro Mitsuhashi, Michio Oyamaguchi, and Yoshikatsu Ohta. On the undecidability of reachability for flat term rewriting systems.IEICE Transactions on Information and Sys- tems, E89-D(2):1000–1007, 2006. 20

    work page 2006

  16. [16]

    equivalence

    M. H. A. Newman. On theories with a combinatorial definition of “equivalence”.Annals of Mathematics, 43(2):223–243, 1942

    work page 1942

  17. [17]

    Proof-theoretic investigations on kruskal’s the- orem.Annals of Pure and Applied Logic, 60(1):49–88, 1993

    Michael Rathjen and Andreas Weiermann. Proof-theoretic investigations on kruskal’s the- orem.Annals of Pure and Applied Logic, 60(1):49–88, 1993

    work page 1993

  18. [18]

    PhD thesis, Uni- versity of Innsbruck, 2014

    Christian Sternagel and Ren´ e Thiemann.Certified Termination Analysis. PhD thesis, Uni- versity of Innsbruck, 2014. IsaFoR/CeTA:http://cl-informatik.uibk.ac.at/isafor/

    work page 2014

  19. [19]

    Cambridge University Press, 2003

    TeReSe.Term Rewriting Systems, volume 55 ofCambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003

    work page 2003

  20. [20]

    Improved modular termination proofs using dependency pairs

    Ren´ e Thiemann, J¨ urgen Giesl, and Peter Schneider-Kamp. Improved modular termination proofs using dependency pairs. InInternational Joint Conference on Automated Reasoning (IJCAR), volume 3097 ofLecture Notes in Computer Science, pages 75–90. Springer, 2004. A Addendum A.1 Lean kernel location The authoritative mechanized kernel is the Lean fileOperato...

    work page 2004