GeezerVison

Refs #375.

Follow-up to #476 and #485, approved by the PM. The simplified Found
(the last step the VS Code panel shows) no longer lists path conditions
that Expected does not depend on.

## Problem

#485 trims the message to the facts linked to Expected. The panel's last
step still listed every `if`/loop guard, so the message and the panel
disagreed. In the study exercises:

- A1_56: the message is `expected redoable(undoManager) but could not
prove it`, but the panel still shows two `switch` guards.
- A1_01: the panel shows `baseline || extended`, which says nothing
about `wParam`.

## Rule

A binder of a generated boolean (a path condition such as
`#if_condition`) is dropped when both hold:
- **Not linked to Expected:** neither its variable nor any term of its
refinement shares a term with Expected, directly or through other facts
of Found.
- **Not mentioned by another row**, so no remaining row refers to a
variable whose binder was dropped.

Rows that are not generated booleans are never dropped by this rule; the
message still trims those (#485), so the message is always a subset of
the panel's last step. Without expected terms (`NeededVariables.NONE`),
nothing is dropped.

Each removal is a step of the existing `Binder` pass. **Stepping back in
the panel still shows the original facts:** the root of the
`VCSimplificationResult` origin chain keeps every dropped guard. I
checked this for the A1_56 shape (each guard is its own `Binder` step
and the root has both), and `TestGeneratedNames` now reads the original
Found, so it checks it on every run.

**One source for the linking.** `factsOf`, `linkedTerms`, `termsOf`,
`termName` and `linkedToExpected` moved from `RefinementError` to
`VCSimplificationUtils`, so simplification no longer needs anything from
diagnostics. `RefinementError` (message and counterexample),
`StateRefinementError` (message) and `NeededVariables` (panel) now all
use them. `VCSimplificationUtils` had its own `termsOf` that named
applications by `toString()`. Now applications over variables are named
as in the SMT model (`size(x)`), which the counterexample needs, and the
other applications are named as written (`f(1)`). All tests pass with
that change.

The "could not prove it" frame, the shortcut that keeps Found as written
when every fact is linked, and the counterexample are unchanged.

## Before / after (the panel's last step)

The rows below are the simplified chain exactly as
`VCImplication.toString()` prints it, from `origin/main` and this
branch.

A1_56 (JabRef `EditAction`, line 69). The message is unchanged on both:
`expected redoable(undoManager¹⁴¹) but could not prove it`.
```
before: ∀##if_condition_122:boolean, !##operation_result_121  =>
        ∀##if_condition_136:boolean, !##operation_result_134 || ##operation_result_135  =>
        ∀#undoManager_141:CountingUndoManager, #undoManager_141 == ##getUndoManager_result_139
after:  ∀#undoManager_141:CountingUndoManager, #undoManager_141 == ##getUndoManager_result_139
```

A1_01 (dcm4che `SlideRecoder`, line 131). The message is unchanged:
`found startTiling(wParam²⁹⁷) && startCompression(wParam²⁹⁷) but
expected compressionExplicit(wParam²⁹⁷)`.
```
before: ∀##if_condition_302:boolean, #baseline_298 || #extended_299  =>
        ∀#wParam_297:ImageWriteParam, startTiling(#wParam_297) && startCompression(#wParam_297)
after:  ∀#wParam_297:ImageWriteParam, startTiling(#wParam_297) && startCompression(#wParam_297)
```

A guard Expected depends on stays
(`ErrorCounterexampleLinkedPathCondition`). The message is unchanged:
`!(port < 0) && timeout¹⁰ == port - 1 is not a subtype of timeout¹⁰ >=
0`.
```
before: ∀##if_condition_0:boolean, !retries > 3  =>
        ∀##if_condition_4:boolean, !port < 0  =>
        ∀#timeout_10:int,    #timeout_10 == port - 1
after:  ∀##if_condition_4:boolean, !port < 0  =>
        ∀#timeout_10:int,    #timeout_10 == port - 1
```
`retries > 3` is dropped. `port < 0` is linked through `timeout == port
- 1` and stays.

In all three cases the original step still shows every guard.

No screenshots: the `liquidjava-dev` harness has no panel-capture script
yet, and the extension server would need this verifier built into it, so
I skipped them.

## Tests

`VCBinderSimplificationTest` has 4 new tests. Each fails without the
change.
- `removesPathConditionsExpectedDoesNotDependOn`: the A1_56 shape,
including a negated disjunction.
- `keepsPathConditionExpectedDependsOnThroughAnotherRow`: a guard linked
through `y == x - 10` stays while an unlinked one goes.
- `keepsPathConditionAnotherRowMentions`: a guard whose variable a
ternary row uses stays.
- `keepsPathConditionsExpectedNames`: a guard whose own variable
Expected names stays, and so does a guard on a call Expected names
(`f(1)`, Codex round 1).

**Changed:** `TestGeneratedNames` now reads the original Found instead
of the simplified one, because the simplified one no longer has the
guards whose names it checks. Only line 54 changes: it is now `isNull ==
#operation_result && #if_condition == isNull && #if_condition && x ==
0`, the alias as written before simplification.

`mvn test`: **702 tests, 0 failures**.

**Size:** +192 / −108 over 7 files. About 90 of the removed lines are
the helpers that moved out of `RefinementError`.

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

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