ch:universes: ch:universes

Problem and invariant. Evaluate the finite max/successor algebra required by the seminar. Maintain the invariant that a reported assignment satisfies every displayed lower bound.

Two representations. One can use weighted difference edges or expression trees. The companion uses expression trees because successor and maximum remain visible in each oracle.

First complete version. Implement evaluation, then comparison, then the two lower bounds for const. Add the strict cycle and three-variable maximum only after the least concrete solution passes.

Observable result. The accepted corpus prints five named PASS lines and then All 5 Chapter 74 corpus cases passed.

A failing version. Make successor evaluate as its argument. The mutant still typechecks but changes the normalized-expression and lower-bound oracles.

Acceptance test. Run the four commands in appendix E. Require a silent check, one passing inline test, the exact six-line run transcript, and an empty audit. Restore the accepted source after replaying the mutation and repeat all four commands.

Mathematical boundary. The program decides the finite representation and cases just described. It does not prove the chapter’s general theorem; that proof remains the local argument or exact import in the main text.