Two different failures, two different lessons

The earlier affine example had a false advertised equation despite attributed PASS. The v4 phase suite instead rejected a false equation and reported aggregate failure. The first is an acceptance-semantics defect; the second is evidence that the relevant fail-closed check worked.

Neither statement establishes every predicate of the earlier software or the correctness of the loop data.