docs(ledger): record ground-truthed soundness-survey correction (#554/#553/#555/#556/#558/#559)

The canonical .claude/CLAUDE.md soundness survey is stale. Captured the
corrected, test-verified status (528 tests green) in the committed tidy-up
ledger instead of editing CLAUDE.md, which lacks an SPDX/owner header and is
thus owner-only to commit. Owner to fold into CLAUDE.md manually.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/reports/TIDY-UP-LEDGER-2026-06-16.adoc

@@ -111,3 +111,47 @@ move the dangle. Left as-is so the gap stays visible:
 * `docs/academic/README.adoc` → `white-papers/type-system.md`,
   `white-papers/effect-system.md`
 * `docs/alib/README.adoc` → `../specs/affinescript-spec.md`
+
+== Soundness survey correction (2026-06-16) — canonical CLAUDE.md is STALE
+
+The `.claude/CLAUDE.md` "Known soundness items (2026-06-11 survey)" section
+(and the disambiguation-table Proofs cell) are STALE. Ground-truthed below by
+running the build + full test suite (528 tests green). The canonical survey
+was NOT edited in place: `.claude/CLAUDE.md` carries no SPDX/owner header, so
+committing an edit trips the strict pre-commit hook, and adding a licence
+header to it is an owner-only decision. Owner to fold these corrections into
+CLAUDE.md manually (with the header) when convenient.
+
+[cols="1,3",options="header"]
+|===
+| Item | Corrected status (2026-06-16)
+
+| **#554** | FIXED. Use-after-move through a callee-returned borrow is now
+  REJECTED (`MoveWhileBorrowed`); aggregate / ref-reassign / match-tail
+  hardening + anti-over-rejection cases asserted
+  (`test_borrow_callee_returned_borrow_*`). #177 closed. issue-draft 08
+  (conditional-origin escape) also FIXED. (Survey still says "this hole
+  remains" — wrong.)
+| **#553 / Polonius** | M1–M3 implemented, NOT "0% implemented". Loan-vs-loan
+  exclusivity now modeled (allowlist 7 divergences: return-escape ×4,
+  captured-linear ×2, call-aliasing ×1). Still TEST-ONLY / unwired — gates no
+  production verdict.
+| **#555** | Codegen FENCED on every reachable backend (WASM, WasmGC,
+  Deno-ESM, JS-text, C) — no more silent arm-drop. Interp: tail-resume
+  correct, multi-shot loud-fails, non-tail single-shot still silently returns
+  the resumed value (residual; needs delimited continuations — blocked on
+  OCaml 4.14 / js_of_ocaml). Runtime handler tests now exist. (Survey says
+  "zero runtime handler tests exist" — wrong.)
+| **#556** | FIXED. Async CPS table-miss fails loud, not silent sync fallback.
+| **#558** | N/A (closed). Refinement & dependent types removed in v1
+  (2026-04-10); `assume(...)` rejected, `T where (P)` parse-errors — no
+  silent-unenforcement path. (Survey says "parsed but silently not enforced"
+  — no longer applicable.)
+| **#559** | FIXED (concrete overlaps). Trait coherence implemented + wired in
+  `check_program`; overlapping impls whose self types unify are rejected.
+  Follow-up: generic-subsumption overlap.
+|===
+
+Session commits (signed, branch `feat/solo-core-metatheory-proofs`,
+unpushed): `bc061ad` (#555 C fence), `2b3f63c` (#559 coherence),
+`3a531e1` (M3 loan-vs-loan).