ch:dependent-nominal-type-theory: context restriction

Problem and invariant. Implement DNTT restriction on newest-first contexts. Discard variables above the target, rebuild fresh names above it, remove the target, and retain the older prefix.

Build and mutation. On x3,b,x2,a,x1, restriction at a returns b,x1. A dependency check rejects use of x2. The two-form body model identifies alpha-renamed bound bodies but distinguishes a bound body from a free name. A mutation that preserves later variables breaks the dependency-rejection oracle.

Acceptance and boundary. Run the four appendix E commands and require six passes and an empty audit. The run decides the finite representation, not DNTT completeness or adequacy.