The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification
This addresses termination analysis in automated theorem proving and term rewriting systems, providing foundational insights with mechanized proofs, though it is incremental in formalizing known boundaries.
The paper formalizes the orientation boundary for first-order step-duplicating recursors, showing that no measure in twelve formalized direct classes uniformly orients the duplicating step, yielding the first mechanized direct impossibility result for named termination-measure classes on a fixed terminating system. For the concrete witness calculus KO7, they certify properties like strong normalization, confluence, and decidable reachability, with specific ordinal calibrations at ω^ω and below ω^ω·2.
We formalize the orientation boundary for first-order step-duplicating recursors. At the schema, no measure in twelve formalized direct classes strictly orients the duplicating step uniformly. These classes include additive and transparent-compositional measures, affine and nonlinear scalar extensions, and tracked vector/pair families, together with a scalar-projection meta-theorem for the matrix side and a symbolic variable-condition barrier yielding a KBO-style impossibility corollary. To our knowledge, this is the first mechanized direct impossibility result for named termination-measure classes on a fixed terminating system. All internal proofs are formalized in Lean~4. The boundary is explanatory, not only negative: we prove an escape trichotomy for the explicit direct universe, a transparency-essentiality theorem with a concrete witness, a dependency-pair escape characterization, a generalized polynomial boundary theorem isolating failure of frozen base dominance, computable barrier-witness extractors, ablations, and SCC synchronization theorems, showing that successful methods cross the boundary only by importing structure outside the formalized direct classes. For the concrete witness calculus KO7, the guarded fragment is certified for strong normalization, confluence, a certified normalizer, decidable reachability to safe normal-form targets, an exact DM-component ordinal calibration at $Ï^Ï$, and a triple-lex certificate image below $Ï^Ï\cdot 2$. For full unguarded KO7, we prove root termination by a nonlinear polynomial witness and a KO7-specialized MPO, lift the nonlinear witness to context-closed strong normalization with an explicit derivation-length bound, expose executable classifier/witness/oracle tooling for direct-orientation attempts, and connect the Lean development to TTT2/CeTA through a checked TPDB export and verifier bridge.