ch:well-founded-recursion: ch:well-founded-recursion

Problem and result. Implement a Kappa checker whose accepted recursive calls carry a strictly smaller natural measure. The finished corpus accepts the Euclidean trace $18,12,6,0$, computes the two named gcd examples, and rejects the mutation $\mathsf{gcd}(a,b)\mapsto \mathsf{gcd}(b,a)$ at its first call from $(48,18)$.

Representation. Represent every successful edge by MkDecrease oldMeasure newMeasure. An accepted gcd result carries a list of these certificates; a failed edge carries Nondecreasing oldMeasure newMeasure. A bare Boolean comparison would discard the two measures needed to replay either verdict.

First complete version. Use Kappa’s natural remainder and implement one transition that records the old and new second components only when the latter is smaller. Drive it with structurally decreasing fuel so the Kappa program is independently total, and print the $18,12,6,0$ trace.

Remaining cases. Add complete gcd evaluation for $(48,18)$ and $(1071,462)$. Preserve the checked measure at every recursive step rather than recomputing a successful Boolean after the call. Finally expose the named nondecreasing result for the proposed measure $48$ after $18$.

A failing version. Replace the Euclidean recursive call $(b,a\mathsf{rem}b)$ by $(b,a)$. On input $(48,18)$ its first new measure is $48$, which is not less than $18$. A checker that reverses the comparison accepts that call where the oracle requires rejection, so the inline test fails.

Acceptance test. Run the four commands in appendix E. Require the four exact PASS lines, the final summary, and the empty audit recorded there.

Mathematical boundary. The program replays the measures in example 82.21. It does not prove accessibility induction, certificate independence, or completeness of any termination checker.