GeezerVison

…th (#534)

Stacked on #531 (base `feat/found-fold-decided-ternary`). Part of #523:
the last step of folding A1_09's Found.

## What

After #531 folds A1_09's ternary under `newMode == BORDERLESS`, the
ternary no longer mentions `newMode`, yet Found still shows `newMode ==
BORDERLESS`. The cause is in **Relevant to Expected**
(`VCRelevantFacts.addSymbols`, `VCRelevantFacts.java:125` on #531):
every `Var` is a symbol, and an enum constant read in code is a `Var`
named `DisplayMode.BORDERLESS`. So `newMode == BORDERLESS` and the
folded ternary stay linked through the constant. (An enum constant
written in a refinement is an `Enum` node, which already linked
nothing.)

A constant is a fixed value: two facts that only compare values with the
same constant share no unknown. The relevance pass now ignores enum
constants as symbols, **except** when a function or alias takes the
constant, or a value one takes is compared with it. There, equality
through the constant does relate facts (`x == A && state(A) == shown`
gives `state(x) == shown`). This exception comes from Codex's round-1
counterexample.

- `VCRelevantFacts` takes the enum constants of the chain.
`VCKnownEnumValues.enumConstants` exposes the set #531 already builds.
- There is still one relevance run and no new pass. The step order is
unchanged: Substitution, Function Substitution, Binder, **Known Enum
Values**, Folding, Arithmetic, Logical, Constraint to a fixed point,
then **Relevant to Expected** once, then `ErrorMessage`'s fact
selection.

## Soundness

Display only; the verdict is unchanged. The relevance pass drops only
facts D whose unknowns are disjoint from Expected's and from the kept
facts S. Enum constants are distinct `EnumSort` values. When no function
takes a value equal to a shared constant, a model of S and a model of D
combine. So the premises imply S, and S fails Expected exactly when the
premises do. `static final` constants are not in the set.

## A1_09 (the only study task that changes)

```
#531:  found newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) but expected display(host) == notDisplayable
this:  found previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable but expected display(host) == notDisplayable
```
The other seven study tasks have the same output as on #531, byte for
byte, with one error each on `reportedLine`. All 287 `testSuite`
fixtures have the same headlines as on #531.

The formatter writes a Found that is a single ternary without
parentheses, as in #531's FULLSCREEN case. That is outside this PR.

## Tests

- `VCSimplificationTest#relevantStepDoesNotLinkFactsThroughAConstant`
(fails without the change).
-
`VCSimplificationTest#relevantStepLinksFactsThroughAConstantAnObjectEquals`
(Codex's counterexample; fails with the naive "drop every constant"
version).
- `mvn test`: 735 tests, 0 failures.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>