ch:capture-types: ch:capture-types
Problem and invariant. Decide five finite subcapturing and escape cases. Maintain that every queued name is an original source name or belongs to the declared bound of a visited name. The result is acceptance or rejection of one finite upper-bound query.
Representation. Represent names by natural numbers, a capture set by either Universal or a duplicate-free finite list, and the environment by an association list from names to declared bounds. A graph adjacency map would make reachability conventional, but would hide the SC-Var direction and pure empty bounds. The association list keeps both visible. A fuel counter makes cyclic malformed inputs terminate; the named tests fit far below its bound.
First complete version. Test whether the target is universal, then test each source name for direct membership in a finite target. Otherwise look up its declared bound and prepend finite dependencies to the work list. An empty declared bound adds no work and therefore eliminates a pure binding; a universal declared bound cannot fit below a finite target.
Remaining cases in metatheory order. Add universal-target acceptance, direct membership, finite-left decomposition, environment expansion, visited-name rejection, and an unbound-name rejection. These cases mirror SC-Star, SC-Set-R, SC-Set-L, SC-Var, the acyclic work invariant, and the escape boundary.
A failing version. Add the exact reverse-dependency search recorded in the companion’s MUTATIONS.md. This makes the chain FAIL.
Acceptance test. Run the four Appendix E commands. Require a silent check, a passing inline harness, the exact seven-line transcript, and an empty audit. Restore the accepted source after mutation and repeat all commands.
Mathematical boundary. The program omits types, variance, beta reduction, and polymorphism. It illustrates lemma 51.3, theorem 51.8 but proves neither result.