Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary
Abstract
We identify a structural property of term-rewriting proof systems called operational inexpressibility: no derivation depends on a specified input dimension and also constrains the target question. The canonical instance is direct aggregation on the primitive recursion duplicator , , where the step argument is duplicated on the right. Under any direct whole-term measure the recursor's mass profile coincides with that of a true circular reference; the boundary operator's channel-preservation axiom and the dependency-pair soundness license separate them. Sound responses split into construction methods (polynomial interpretations, path orderings) extending the proof language, and confession methods (dependency pairs, counter-projection, size-change termination, argument filtering) projecting away the unincorporable dimension under external license; all four share a projection rank and certified-forgetting interface. Arts-Giesl soundness is -combinatorial, formalizable in , with an artifact-facing termination measure inside , far below the -scale of classical G\"odelian reflection. The confessed burden grows quadratically across the canonical trace while residual proof work grows linearly. An architectural necessity theorem shows that any first-order step rule emitting a per-step record frame while preserving its generator must duplicate. A Layer-Crossing-Under-External-License (LCEL) schema places the confession in the Feferman-Beklemishev reflection family rather than the Lawvere-Yanofsky diagonal family, recovering the six-step structural identity with G\"odel 1931 as a specialization. A witness-language hierarchy with minimal order identifies the boundary as .
Cite
@article{arxiv.2604.22844,
title = {Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary},
author = {Moses Rahnama},
journal= {arXiv preprint arXiv:2604.22844},
year = {2026}
}
Comments
60 pages. All the Lean codes are available on https://github.com/MosesRahnama/The-Orientation-Boundary