ch:formalized-graded-erasure: guarded finite extraction

Problem and result. Implement the chapter’s finite extraction decision for variables, naturals, graded lambdas and applications, and weak-pair matches. The invariant is that deletion occurs only at inferred grade zero, and an erased match is rejected in an open context. Acceptance means that all named expected-output comparisons succeed and the mutation that deletes a grade-one argument fails.

Representation. The companion uses an extrinsic term tree with an explicit grade on each binder and application. An intrinsic syntax indexed by demand would make illegal deletion unrepresentable, but it would hide the rejection path that the exercise asks the program to display. The result type therefore distinguishes extracted syntax, retained arguments, and a diagnostic.

First complete version. Begin with variables, zero, successor, and a recursive occurrence check. Add lambda extraction: a zero-grade binder replaces its target occurrence by the closed loop marker, while a nonzero binder remains. At this stage the erased-index input already produces suc zero end to end.

Remaining cases. Add application next, following U-App: grade zero returns the extracted function and a nonzero grade records that the argument was retained. Add the weak-match case last because it carries the contextual side condition absent from ordinary syntax traversal. The open-context flag is checked before the branch is accepted. These stages follow the variable, binder, application, and exceptional match order of the printed extraction proof.

A failing version. Return the extracted function in every application branch. The program then deletes the grade-one argument in retained-argument; its named oracle fails. A second faulty version returns zero for every erased weak match; open-erased-match exposes the missing theorem side condition.

Add an inferred-use pass that rejects a dishonest zero grade, and stop occurrence search at a shadowing binder with the same spelling. These two cases keep inferred demand and binder identity separate from source annotations.

Acceptance test.

Require the six accepted lines recorded in subappendix E.9, an empty audit, and nonzero test status for each restored mutation. The run must retain the grade-one argument and reject both the open erased match and the dishonest grade. It must also accept the closed erased match and leave the shadowed outer binder unused. The executable record in subappendix E.9 alone stores the source identity and mutation replay.

Mathematical boundary. The traversal illustrates extraction and its operational boundary. Running it does not prove the logical relation, source normalization, usage preservation, or exact heap access counts.