2026/04/30 by Moses Rahnama
#cs.LO
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)→ x, F(x,y,S(n))→ 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 Π02 principle; its subterm-criterion route is a size-change instance formalizable in RCA0 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.