ch:dependent-control: finite NEF classification

Problem and result. Recognize the displayed NEF proof fragment and keep non-NEF control syntax legal outside formula dependencies. Acceptance requires variables, lambdas, pairs, reflexivity, and the restricted $\mu \star$ form inside dependencies; rejection of ordinary $\mu \alpha$-proofs and application spines there; and a visible result-family argument for a dependent product.

Representation. Use separate recursive datatypes for proofs and formula skeletons. The proof syntax distinguishes fragment-local MuStar from ordinary MuAlpha. A MuStar contains a NEF command whose context is only NStar or a NEF binder; it is not the source’s distinguished continuation constructor. A Boolean nef traversal governs only the operation that inserts a proof into a formula; a separate syntax predicate retains all constructors for ordinary program positions. This separation prevents NEF from being mistaken for a global ban on control.

First complete version. Implement nef structurally for variables, lambdas, positive pairs, reflexivity, and the fragment-local MuStar form. Return false for undelimited MuAlpha and application spines. Add one fixture for each constructor before formula translation; these named lines fix the exact ordinary-versus-delimited control boundary. Also record that a proof pair is NEF without claiming that it is a normal form.

Remaining cases. Walk equality and existential-natural formulas without erasing their first-order terms. For a proof-dependent product, print the translated positive domain and the computation-valued codomain family with its proof argument still visible. Keep a separate outside-dependency check that accepts control. Add the $p_0$ witness/proof mismatch as the negative observable for the deliberate NEF mutation.

Observable result. The run prints the twelve lines in subappendix E.10. It ends with All 12 Chapter 109 corpus cases passed. The result-family line must retain its proof argument; a translation that prints a constant codomain does not satisfy the exercise. The nondependent-equality line must contain no proof occurrence.

A failing version. Change only the MuAlpha branch of nef to True. The source remains well typed, but the undelimited-$\mu$ rejection and $p_0$-mismatch oracles print FAIL. The outside-dependency control oracle should remain accepted, showing that the mutation concerns the dependency gate.

Acceptance test. Require the exact twelve accepted lines and audit result [] recorded in subappendix E.10. The named mutation must make its test fail; restoring the MuAlpha rejection must restore every accepted outcome. The executable record in subappendix E.10 alone stores commands, source identities, and the mutation transcript.

Mathematical boundary. The checker implements the displayed finite grammar and target type skeleton. It does not implement stores, the distinguished continuation, source reduction, CPS terms, subject reduction, normalization, or consistency for $d{L}_{\widehat{\mathsf{tp}}}$.