Moses Rahnama

Moses Rahnama

We identify \emph{operational inexpressibility}: for a fixed input and dimension of term-rewriting proof systems, no derivation in the proof language both depends on that dimension and 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 step argument $y$ is duplicated. Sound responses split into \emph{construction methods} (polynomial interpretations, path orderings) extending the proof language, and \emph{confession methods} (dependency pairs, counter-projection, size-change, argument filtering) projecting the unincorporable dimension under external license; all four share one projection rank and certified-forgetting witness. The Arts-Giesl license is $Π^0_2$, formalizable in $\mathrm{I}Σ_1$, with termination measure at order type $ω^3$ in $\mathrm{RCA}_0$. Within the analyzed family the duplicator is the unique structurally complete member at which the confession becomes load-bearing. Confessed burden grows quadratically across the canonical trace while residual proof work grows linearly; a Shannon-style validator recasts the obstruction as a divergent inefficiency coefficient. An architectural-necessity theorem shows that any first-order step rule emitting a per-step record frame while preserving its generator must duplicate, so the duplicator is the minimal faithful record-emitter. A \emph{layer-crossing under external license} (LCEL) schema abstracts the ascent pattern and places the confession in the Feferman-Beklemishev reflection family (not Lawvere-Yanofsky diagonal), recovering the six-step structural identity with Gödel 1931. A witness-language stratification with minimal order $κ^*$ marks the orientation boundary as $κ^*(x)>0$. Mechanized in Lean 4 as a single typed LCEL carrier with canonical Gödel / DP realizations.

Moses Rahnama

We formalize the orientation boundary for first-order step-duplicating recursors. At the schema, no measure in twelve formalized direct classes strictly orients the duplicating step uniformly. These classes include additive and transparent-compositional measures, affine and nonlinear scalar extensions, and tracked vector/pair families, together with a scalar-projection meta-theorem for the matrix side and a symbolic variable-condition barrier yielding a KBO-style impossibility corollary. To our knowledge, this is the first mechanized direct impossibility result for named termination-measure classes on a fixed terminating system. All internal proofs are formalized in Lean~4. The boundary is explanatory, not only negative: we prove an escape trichotomy for the explicit direct universe, a transparency-essentiality theorem with a concrete witness, a dependency-pair escape characterization, a generalized polynomial boundary theorem isolating failure of frozen base dominance, computable barrier-witness extractors, ablations, and SCC synchronization theorems, showing that successful methods cross the boundary only by importing structure outside the formalized direct classes. For the concrete witness calculus KO7, the guarded fragment is certified for strong normalization, confluence, a certified normalizer, decidable reachability to safe normal-form targets, an exact DM-component ordinal calibration at $ω^ω$, and a triple-lex certificate image below $ω^ω\cdot 2$. For full unguarded KO7, we prove root termination by a nonlinear polynomial witness and a KO7-specialized MPO, lift the nonlinear witness to context-closed strong normalization with an explicit derivation-length bound, expose executable classifier/witness/oracle tooling for direct-orientation attempts, and connect the Lean development to TTT2/CeTA through a checked TPDB export and verifier bridge.