ch:dependent-copattern-elaboration: ch:dependent-copattern-elaboration

Problem, result, and invariant. Compile a dependent three-field orbit record without checking a field before the projections appearing in its type are available. Maintain the invariant that the frontier stored at field $j$ contains a term for every field strictly before $j$.

Representation tradeoff. An intrinsically typed case tree could index each node by its exact field telescope. Kappa’s companion instead stores field names and an explicit finite set of prior names, then validates membership before constructing the node. Intrinsic indices rule out malformed trees by construction; explicit frontiers make missing-dependency diagnostics and semantic mutations direct.

First complete version. Compile the ordered clause list into a spine of field nodes, and store in each node the frontier that was accumulated before it. Begin next with the empty frontier; require next when reaching step, then extend with step before tail. Now print nothing by hand: render the tree from the spine, render the frontiers from the stored sets, and drive the observation trace from the spine as well, taking each value from the next node and each following state from the tail node. Anything printed as a literal here is a claim the program has not checked.

Remaining cases. Add an ordered input-pattern fixture with zero and successor constructors, and make coverage reject a definition that splits only at successor, naming the missing constructor. Add the declaration-order fixture that requests step with an empty frontier. Then add three orthogonal failures: a wholly missing field, coverage missing only in one field, and a right side of the wrong finite field type. Each diagnostic names its field and local obligation.

Observable result. The accepted program prints the tree, all three frontiers, observations 1,2,3, five named rejections, and All 8 Chapter 125 corpus cases passed.

Five failing versions. Remove next from the declared predecessors of step; the mutant accepts the bad order, which is the clause order that checks reflexivity against an unknown endpoint. Separately, let one constructor pattern count as covering, stop advancing the stored frontier, check all coverage through the next rows, and invoke the term checker on no fields. The four resulting outputs expose missing constructor, frontier, per-field, and finite typing checks.

Acceptance test. Run the four commands in subappendix E.5. Require a passing check, one passing inline test, the exact nine-line run transcript, and an empty audit. Replay each mutation, require its oracle to fail, restore the accepted source, and repeat all four commands.

Mathematical boundary. The implementation calculates the typed-frontier invariant of definition 125.4 for one finite record and one finite input split. It illustrates, but does not prove, theorem 125.19 or the imported Cockx–Abel theorem.