ch:type-theory-modulo: finite typed-rewrite certificates

Problem and invariant. Check a bounded rewrite card while keeping typedness, peak joinability, termination, and decidable conversion separate. Accepted rules have equal endpoint types; a decidable-conversion claim also requires termination.

Two representations. Dependent telescopes would model the framework directly. The companion uses a finite certificate plus a typed addition language, which keeps every negative oracle executable.

First complete version. Implement structural equality and endpoint inference, one-step addition, fuel-bounded normalization, and recursive overlap traversal. Store the overlap terms rather than a claimed Boolean verdict. Check an orthogonal card, mismatched endpoint types, joining and nonjoining peaks, a later bad entry in MoreOverlaps, and absent supplied termination evidence at explicit fuel 12.

Observable result. The run prints eight named PASS lines and ends All 8 Chapter 97 corpus cases passed.

A failing version. Change inference for $\mathsf{Truth}$ from $\mathsf{Bool}$ to $\mathsf{Nat}$. The mutant checks, but a certificate with unlike endpoint terms is accepted and the endpoint-inference test exits nonzero. In a separate replay, replace the recursive MoreOverlaps branch by True; the later dishonest pair is then accepted and its named oracle fails.

Acceptance test. Run all four commands in subappendix E.8; require exact stdout and []. Restore the source after replaying the mutation.

Mathematical boundary. Finite peaks and bounded reduction prove neither global confluence nor termination. The corpus has no dependent conversion or higher-order matching, so it does not prove either chapter metatheorem.