[testing] `Undetermined` (solve-result: 2) goldens are not soundness evidence; symbol-name determinism unverified

## Summary

Two testing-process points that let the soundness bug in #194 sit undetected in CI for a long time:

1. **`Undetermined` (`solve-result: 2`) is not soundness evidence.** A golden that pins a query to `solve-result: 2` passes whether the underlying theory is sound or not — `Undetermined` just means the solver did not decide. Goldens of this kind exercise nothing about the `Valid` path, so an inconsistent theory that reports `Valid` on false goals (#194) never trips them.
2. **Verdict determinism across symbol renaming is unverified and worth making robust.** SMT symbol suffixes (`_uniq.N`, `@lambdaN`, `@applyN`, `FunN`, `$N`) come from a global `mkFreshId` counter, so verdict-affecting artifacts (dump reproducibility, quantifier-instantiation order, goldens) depend on incidental naming. I could **not** reproduce a naming-driven `Valid ↔ Undetermined` flip under controlled conditions (see below), so this is a robustness/reproducibility recommendation, not a demonstrated bug.

## What I could and could not reproduce (controlled experiment, main @ `3a141c8`)

Because `_uniq` numbers derive from a global counter, renaming binders/definitions shifts them while preserving semantics. I ran each query in a fresh `lake env lean` process (`gen-cex: 0`):

- **Valid-family** (partition + `List.all` over an empty list, `Nat` codomain): 3 byte-identical copies + 4 renamed-binder variants → **all 7 `Valid`**. Stable.
- **Undetermined-family** (`foldr add = foldl add`): identical copies + renamed variants → **all `Undetermined`**. Stable.

So on these two lambda-family queries the verdict was **stable** across both identical reruns and symbol renaming. I did **not** observe a byte-identical-modulo-naming verdict flip. A pair of normalized SMT dumps from an earlier investigation (`na.txt`/`nb.txt`) are byte-identical modulo their (already-canonicalized) symbol labels, but they carry no attached verdicts, so they do not establish a flip either. The strong claim "byte-identical queries flip `Valid ↔ Undetermined`" is therefore **not substantiated** and should not be treated as a known bug; the deterministic-naming recommendation below stands on reproducibility/robustness grounds only.

## Directions

- **CI must not treat `solve-result: 2` as evidence of anything about the `Valid` path.** Add adversarial *soundness* goldens: negated known-false theorems (e.g. the `bogus`/`boom` family in #194) that must **not** come back `Valid`, and known-true theorems that must not be refuted. These would have caught #194 immediately.
- Prefer **canonical / deterministic symbol naming** in emitted SMT (stable, source-derived suffixes) so dumps are reproducible and goldens are not luck-shaped — regardless of whether naming actually affects verdicts.
- When triaging a `solve-result: 2` golden, remember it asserts "solver gave up here", not "this is correct".

## Relationship

This is the CI/testing gap that masked #194. #194 is the underlying soundness bug.

## Environment

- input-output-hk/Lean-blaster `main` @ `3a141c8`; Lean `v4.24.0`; Z3 4.15.2

## Severity

Testing / process.

Start by reviewing the existing goldens that use solve-result: 2 and the controlled experiments described in the issue, running each query in a fresh lake env lean process. Add adversarial soundness goldens for known-false and known-true theorems, then evaluate canonical symbol naming in emitted SMT. Done means Undetermined goldens are not treated as Valid-path evidence and false goals do not return Valid.

Written by the indexing model from the issue text.