ch:very-dependent-functions: finite predecessor checking
Problem and invariant. Validate a finite declaration in numeric label order. Every dependency must be strictly smaller than its field label.
Two representations. A graph plus topological sort supports arbitrary orders; numeric labels make the predecessor witness explicit and let structural list recursion decide the frozen corpus directly.
First complete version. Define fields as label/dependency pairs. Write allBefore, lift it over declarations, then add Point, numeric, self-edge, cycle, and predecessor-visibility fixtures.
Observable result. The run ends All 5 Chapter 95 corpus cases passed.
A failing version. Replace
Acceptance and boundary. Apply the four commands of subappendix E.7 and require audit []. Numeric order checking does not construct or validate a very-dependent PER family.