We identify operational inexpressibility, a structural property of term-rewriting proof systems: for a fixed input and dimension, every derivation ignores the dimension or leaves the target question unconstrained. 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))$, whose step argument $y$ is duplicated. A companion paper maps the non-representability frontier; we prove it is operational inexpressibility at the step-argument dimension. Sound responses split into construction methods extending the proof language and confession methods (dependency pairs, counter-projection, size-change termination, argument filtering) projecting away the unincorporable dimension under an external soundness license. Under any direct whole-term measure the recursor's mass profile coincides with that of a true circular reference: only the confession family's licensed projection separates them; non-derivability, TRS isomorphism and information equivalence are proved in Lean. Arts-Giesl soundness is a $Π^0_2$ principle; its subterm-criterion route is a size-change instance formalizable in $\mathrm{RCA}_0$ with an order-$ω$ termination measure. Within the analyzed family the duplicator is the unique structurally complete member requiring confession. The confessed burden grows quadratically against linear residual proof work; a Shannon-style validator recasts the obstruction as a divergent inefficiency coefficient. An architectural necessity theorem makes the duplicator the minimal faithful record-emitter. A layer-crossing schema places the dependency-pair confession in the Feferman-Beklemishev reflection family rather than the Lawvere-Yanofsky diagonal family, matching the six-step shape of Gödel's 1931 move. A witness-language hierarchy with minimal witness order $κ^*$ puts the orientation boundary at $κ^*(x)>0$.
翻译:暂无翻译