Problem and invariant. Run the Kappa companion, then extend its interval operations. Maintain this decidable invariant: every named concrete operand pair produces a result contained in the returned interval. For the countdown fixture, every state must also satisfy 0 ≤𝑥 ≤𝑦.
First complete version. Keep lower and upper extended endpoints as separate datatypes, implement containment, and replay input three as (3,3),(2,3),(1,3),(0,3). Require the five named passes in appendix E and an empty audit before adding new cases.
Multiplication and its failing version. First return [𝑙1𝑙2,𝑢1𝑢2]. The inputs [ −2,3], [4,5] expose the bug because ( −2)5 = −10 ∉[ −8,15]. Replace the rule by the minimum and maximum of all four endpoint products. The accepted result is [ −10,15], and the same four-product membership check is the oracle.
Threshold widening. Add threshold 10. On the increasing counter chain require exactly [0,0],[0,1],[0,10],[0, +∞]. At every step check that the new interval contains both the old interval and the proposal. Termination follows from a strictly increasing index in the finite threshold list, followed by infinity.
Relational mutation. Append 𝖲𝗍𝖺𝗍𝖾(4,3). The unchanged 𝑥 ≤𝑦 oracle must fail. The correct precondition is that all input states satisfy 0 ≤𝑥 ≤𝑦; the countdown step preserves it because only a positive 𝑥 is decremented. Remove the bad state or reject the fixture before replay.
Acceptance and boundary. Run the four commands in appendix E. Require the original five passes, the naive multiplication counterexample, accepted [ −10,15], the four-stage threshold trace with coverage checks, relational-mutant rejection, and audit []. This finite suite does not establish structural analyzer soundness, general widening convergence, DBM closure, or Verasco correctness.