ch:dependent-effects: dependent sequencing

Problem and result. Build a finite value/computation checker in which dependent sequencing stores an effectful producer only as a thunk. The invariant is that classifiers contain value variables or admitted thunks, never raw computations. The resulting evaluator accepts a returned length-two vector, rejects a raw effect in a type, and leaves forcing an unknown thunk neutral.

Representation. The companion uses separate enums for value types, computation forms, and classifier expressions. A single untyped AST with a phase tag would require dynamic checks at every recursive node; the split enums centralize the value/computation boundary. A richer intrinsically sorted encoding would prevent construction of the negative fixture, so the classifier checker is kept extrinsic.

First complete version. Implement natural values, Return, and the vector classifier. The smallest complete computation returns two and substitutes it into the vector family, producing accepted: Vec 2. This stage makes the Bind${}^{+}$ substitution visible before adding other computations.

Remaining cases. Add thunk and force next, including the beta case for a known thunk and the neutral case for an unknown one. Define the global readto classifier as a thunked computation retaining both state endpoints. Admit it only by the one-sided inclusion rule; a separate equality check must report that a global read is not thunkable. Reject an unknown thunk as a dependency. Add the classifier-formation pass last. This order follows formation, introduction, elimination, computation, and the neutral boundary.

A failing version. Make the fallback of inferClassifierIndex accept a raw computation. The source still checks as a Kappa program, but the raw-effect oracle fails. A separate mutation replaces the high endpoint of a thunked read with its low endpoint. That mutation loses the sensitive-family distinction. Declaring the global read thunkable separately would instead confuse equality with inclusion.

Acceptance test. Require the eight exact pass lines recorded in subappendix E.9, an empty audit, and a nonzero test result for the recorded mutations. The global readto line must say thunked; the neutral-force line remains distinct from evaluated force and rejected dependency. The executable record in subappendix E.9 alone stores the accepted source identity and mutation replay.

Mathematical boundary. The checker illustrates the sorting premise of Bind${}^{+}$ and one beta instance. Running it proves neither theorem 103.3 nor theorem 103.10, thunkability, or semantic soundness.