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)\to x$, $F(x,y,S(n))\to G(y,F(x,y,n))$, where the step argument $y$ 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 $Π^0_2$-combinatorial, formalizable in $\mathrm{I}Σ_1$, with an artifact-facing $ω^3$ termination measure inside $\mathrm{RCA}_0$, far below the $\varepsilon_0$-scale of classical Gödelian 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ödel 1931 as a specialization. A witness-language hierarchy with minimal order $κ^{}$ identifies the boundary as $κ^{}(x)>0$.

翻译：我们识别项重写证明系统的一个结构性质，称为操作不可表达性：没有任何推导同时依赖于指定输入维度并约束目标问题。典型实例是原始递归复制器 $F(x,y,Z)\to x$、$F(x,y,S(n))\to G(y,F(x,y,n))$ 上的直接聚合，其中步骤参数 $y$ 在右侧被复制。在任何直接整项测度下，递归器的质量剖面与真正循环引用的质量剖面一致；边界算子的通道保持公理和依赖对健全性可区分它们。正确响应分为构造方法（多项式解释、路径序）扩展证明语言，以及坦白方法（依赖对、反投影、大小变化终止、参数过滤）在外部许可下投影掉不可纳入的维度；所有四种方法共享一个投影秩和认证遗忘接口。Arts-Giesl 健全性是 $Π^0_2$-组合的，可在 $\mathrm{I}Σ_1$ 中形式化，在 $\mathrm{RCA}_0$ 内具有一个面向工件的 $ω^3$ 终止测度，远低于经典哥德尔反射的 $\varepsilon_0$ 尺度。坦白负担在规范迹上呈二次增长，而剩余证明工作呈线性增长。一个架构必要性定理表明，任何在保持生成器的同时发射每步记录帧的一阶步骤规则必须进行复制。一个外部许可下层间穿越（LCEL）模式将坦白置于费弗曼-别克列米舍夫反射族中，而非劳维尔-亚诺夫斯基对角线族，恢复了与哥德尔1931年作为特例的六步结构恒等式。一个具有最小序 $κ^{}$ 的见证语言层级将边界识别为 $κ^{}(x)>0$。