fix(ci): re-anchor SOUNDNESS.adoc #555-stub/#560 row to clear soundness-ledger guard

check-soundness-ledger.sh fails on main: the #555-stub/#560 row (Lean/Why3
backends drop `return`) was marked `residual (pinned)` and cited the fixture
test/e2e/fixtures/stub_backend_return_dropped.affine + test_stub_backend_return_xfail,
but neither was ever committed — so the guard's "every cited anchor exists"
check fails (and the row's "pinned" claim was untrue).

The hole is real but genuinely unpinned, so downgrade the row to `open (tracked)`
and drop the phantom anchor (now: tracked by #560; experimental gating is the
only current fence). Truthful and minimal — no fabricated fixture/test. Creating
the real pin (fixture + xfail) remains the #560/#624 follow-up.

Verified: check-soundness-ledger.sh and check-doc-truthing.sh both exit 0; all
remaining cited fixtures exist.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8

Author: claude

docs/SOUNDNESS.adoc

@@ -108,17 +108,17 @@ Every row in this table is in scope for the gate. There are no soundness-relevan
 | `test/test_borrow_polonius.ml` (parallel-run diff gate + `known_divergences`, count pinned at 7)
 
 | #555-stub / #560
-| The Lean and Why3 experimental backends drop `return` statements wholesale — a silent-wrong-value shape, the same _category_ as the #555 codegen hole but on the stub-backend path. Not yet fenced. The fixture asserts the *current wrong behaviour* and the backends are gated `experimental` so no production verdict depends on them.
-| `residual (pinned)`
-| `test/e2e/fixtures/stub_backend_return_dropped.affine` + `test_stub_backend_return_xfail` (asserts the drop; flips to failing the day the backends fail loud or are removed). See _Still open_.
+| The Lean and Why3 experimental backends drop `return` statements wholesale — a silent-wrong-value shape, the same _category_ as the #555 codegen hole but on the stub-backend path. Not yet fenced, and not yet pinned by a fixture; the backends are gated `experimental` so no production verdict depends on them.
+| `open (tracked)`
+| Tracked by #560 — not yet pinned by a fixture/test; the planned anchor (an xfail asserting the drop, flipping the day the backends fail loud or are removed) is the follow-up. The `experimental` gating is the only current fence. See _Still open_.
 |===
 
 == Still open — read before claiming "sound"
 
 The implementation holes marked `fixed` / `loud-fail` / `removed` above are closed. Honesty requires naming what is *not* a guarantee. Each item here is a row in the table above, restated for the hurried reader — not a separate list:
 
 * *Interpreter non-tail resume* (#555, `residual (pinned)`) — the `5`-not-`105` shape. Silent on the interpreter path; pinned.
-* *Stub backends drop `return`* (#555-stub / #560, `residual (pinned)`) — Lean and Why3 drop `return` wholesale. Silent-wrong-value, broader than #555 codegen, fenced only by `experimental` gating and a pinning fixture, not by a loud failure. Treat all non-reference backends as experimental (see `docs/CAPABILITY-MATRIX.adoc`).
+* *Stub backends drop `return`* (#555-stub / #560, `open (tracked)`) — Lean and Why3 drop `return` wholesale. Silent-wrong-value, broader than #555 codegen, fenced only by `experimental` gating (not yet pinned by a fixture, nor by a loud failure). Treat all non-reference backends as experimental (see `docs/CAPABILITY-MATRIX.adoc`).
 * *Generic-subsumption coherence* (#559 generic, `open (tracked)`) — concrete overlaps caught; generic-impl overlaps not yet detected.
 
 If you are deciding whether AffineScript is "sound enough" for a use, these three rows are the answer, and the metatheory caveat below applies to *all* of them.