ch:dependent-refinement: three isolated ledgers

Problem and result. Implement three finite decisions without permitting evidence from one decision procedure to cross into another: dependent-function variance, certificate replay for a difference bound, and vector-index casts. Acceptance requires the positive/nonzero comparison, the two boundary-index decisions, both vector outcomes, and rejection of an incorrectly tagged request.

Representation. The companion uses a sum of request constructors rather than one record with optional fields. The request tag determines the handler before any evidence is inspected. An intrinsically indexed request family could make cross-ledger routing unrepresentable; the extrinsic sum keeps the required negative test executable and makes the rejected route visible.

First complete version. Begin with the dependent-function case. Store the provider and client domain classes and return Accepted only in the printed contravariant comparison. Add the certificate request next: its constructor carries the candidate index and bound, and replay accepts at $i=0$ while rejecting the same upper-bound claim at $i=3$.

Remaining cases.

Before casts, replay both bounded paths and negative-cycle certificates: every edge must occur in the graph, endpoints must be contiguous, and the recomputed sum must satisfy the requested bound or be negative for a closed cycle.

Represent vectors by their outer constructor and index. The unknown-index upcast retains that representation. The downcast to zero returns NilResult for nil and CastError for cons. Add reversed-domain rejection before the dynamic casts. For difference constraints, replay a supplied edge path, recompute its weight from the edge list, and reject both a forged weight and a disconnected path. Add WrongLedger last and reject it before any handler-specific payload is considered. This order makes the tag-dispatch invariant independent of the three calculations.

Observable result. The accepted run prints the eleven named PASS lines recorded in subappendix E.10 and ends All 11 Chapter 106 corpus cases passed. The index-three rejection and cons cast are distinct results: one is a static certificate failure and the other is a run-time cast error.

A failing version. Trust the certificate’s claimed path weight instead of summing the named edges. The mutant still typechecks, but the forged-weight oracle prints FAIL. Rejection of the disconnected path distinguishes a bad certificate shape from a merely bad claimed total.

Acceptance test. Require the exact eleven accepted lines recorded in subappendix E.10, successful checking and testing, and the literal audit result []. The named mutation must make its test fail; the restored edge-sum replay must pass. The executable record in subappendix E.10 alone stores commands, source identities, and the mutation transcript.

Mathematical boundary. The program checks finite representatives of three rules. It does not prove $\lambda P_{\le }$ decidability, refinement preservation, GCIC graduality, or the list/vector connection laws.