SearcharxivSearch

arXiv subjects

Moses Rahnama

Publications and source records attributed to Moses Rahnama.

2 recordsLinked to original sources

Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary

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 $\Pi^0_2$ principle; its subterm-criterion route is a size-change instance formalizable in $\mathrm{RCA}_0$ with an order-$\omega$ 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\"odel's 1931 move. A witness-language hierarchy with minimal witness order $\kappa^*$ puts the orientation boundary at $\kappa^*(x)>0$.

cs.LO

The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification

We mechanize an orientation boundary for first-order rewrite systems with step-duplicating recursors, using the Right-Duplicating Recursor Schema $\mathrm{recur}(b,s,\mathrm{succ}(n)) \to \mathrm{wrap}(s,\mathrm{recur}(b,s,n))$. For a reflected scalar grammar over counter and payload coordinates with constants, sums, products, pointwise maxima, and natural scalar multiples, Lean proves $\mathrm{Orients}(e) \iff \mathrm{PayloadBlind}(e) \land \mathrm{CounterStrict}(e)$. On the counter-admissible subclass, orientation is equivalent to payload blindness. The counter projection inhabits the class; the payload-blind constant-zero expression fails counter strictness and orientation, showing the restriction is necessary. A vector extension makes payload blindness necessary whenever strict comparison forces nonincrease of a grammar-expressible scalarization. Twelve scalar and tracked-vector families form the witness-bearing barrier basis, and 80 root-level exclusions lift to context-closed rewriting under their original hypotheses. An escape trichotomy shows that every successful orienter in the stated universe must abandon wrapper-subterm sensitivity, successor transparency, or the formalized families; dependency-pair, nonlinear-polynomial, and multiset-path-order witnesses realize the escape side. For a concrete calculus, Lean certifies strong normalization and confluence of the guarded relation, termination results for the unguarded system, executable normalization and reachability procedures, derivation-length bounds, and ordinal calibrations. Three TTT2 termination proofs receive CeTA 2.36 certification. Machine-checked ledgers close the stated 76-family syntactic universe and a separate 16-row semantic universe. This is an object-level classification for a fixed terminating system and explicit measure classes, not a class-wide undecidability theorem.

cs.LO