The Primitive Recursor Test: Construction-Recognition Gap and Representation-Shift Failure in Formal Reasoning

The primitive recursor, $F(x,y,Z)\to x$ and $F(x,y,S(n))\to G(y,F(x,y,n))$, is the counted loop inside fold combinators, proof-assistant recursors, and trip-counted compiler loops, and an automated termination tool certifies it in 0.025 seconds. Language models fail on it, in the forms that an observer-license theory of proof classes, stated in this paper, accounts for. The Primitive Recursor Test (PRT) asks 30 models, across 4,160 sessions, three questions: does the system terminate, does the proof have mathematical validity, and does the proof use the displayed rules alone. A Python rulebook decides every proof score from reader transcriptions against certified answers, Lean theorems, and ground-term counterexamples; no model and no person assigns one. The termination verdict is right in 791 of 960 sessions on the two-rule system, its copy-removed control, and an eight-rule system, and the proof behind it fails the test of mathematical validity in 516 of those 791. On the two-rule system, 64.6% of 240 sessions fail mathematical validity and 99.2% give no rule-derived proof under the paper's rulebook; the three models with mathematical validity in all 8 of their sessions give no rule-derived proof either. On the eight-rule system, which contains the recursor, 25.4% of 480 sessions give a wrong termination verdict and none gives a rule-derived proof. Offered the rule-derived method on a menu of five methods that all have mathematical validity, 94.2% of sessions judge that it has mathematical validity and is rule-derived; unaided, 2 of 240 and 0 of 480 sessions construct it, and 29 of 30 models change their method across identical prompts. The theory says why: a proof method uses only what its observer reads, and the step rule copies $y$ into the output and into the recursive call, as any first-order rule that records the step argument in its output while continuing the recursion must. No measure that adds symbol weights over the whole term then decreases at the step, so the standard methods need either a precedence or coefficients that the rules do not fix, or the dependency-pair projection, which compares the counter at the recursive call under an imported soundness theorem and is the one method the rules determine. Each failure form the theory derives occurs: termination denied, a decrease claimed that a ground term refutes, or imported parameters that differ from one session to the next. Sessions, reader records, scoring code, and reference proofs accompany the paper as supplementary material.