English

Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary

Logic in Computer Science 2026-05-22 v3

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 F(x,y,Z)xF(x,y,Z)\to x, F(x,y,S(n))G(y,F(x,y,n))F(x,y,S(n))\to G(y,F(x,y,n)), where the step argument yy 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 Π20\Pi^0_2-combinatorial, formalizable in IΣ1\mathrm{I}\Sigma_1, with an artifact-facing ω3\omega^3 termination measure inside RCA0\mathrm{RCA}_0, far below the ε0\varepsilon_0-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 κ\kappa^{} identifies the boundary as κ(x)>0\kappa^{}(x)>0.

Keywords

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

R2 v1 2026-07-01T12:34:16.705Z