ch:linear-dependent-types: shape and usage checking

Problem and invariant. A state variable has total usage at most one, while every classifier contains only parameter syntax or computed state shape.

Two representations. Indexed syntax can enforce sort and usage intrinsically. The companion uses finite cases and explicit verdicts so nearby rejections remain observable.

First complete version. Define parameter and state types, unit-valued state shape, result types, a three-binding context, and recursive term/type traversals. Compute the threaded-read result and check duplicated state, state-in-index, shaped-state-index, and duplicated-parameter cases.

Observable result. The run prints seven named passes, including Pair(Bit,VecCell(2)). Its final line is

All 7 Chapter 98 corpus cases passed.

A failing version. Make the shape of CellState(width) expose width. The mutant checks, but the state-shape oracle changes and the inline test exits nonzero.

Acceptance test. Run all four commands in subappendix E.8; require exact stdout and []. Restore the accepted branch afterward.

Mathematical boundary. The corpus has no simultaneous substitution induction, evaluation relation, fibration, or dependent counit. It proves neither preservation nor semantic soundness.