docs(tech-debt): mark CORE-01 (S1) borrow-checker Phase-3 DONE — closes #177

The ledger entry was stale: it listed C' (loop soundness), D (linear-capture
by closure), and ref-to-ref binding as residual, but those three slices
landed via PRs #395, #396, #397 (with #399/#400 as related follow-ups).

Refresh the CORE-01 row to:
* document the three landed slices alongside Slices A/B/C-light,
* flip the Stage D ASCII status from ACTIVE to CLOSED,
* mark the row CLOSED 2026-05-30 with the residual scoped exclusively to
  ADR-022 (true Polonius origin/region variables), filed as a separate
  workstream in docs/decisions/0022-polonius-origin-variables.adoc (PR #407).

Closes #177.

Evidence:
* lib/borrow.ml:1635-1715 documents pt1+pt2+pt3 (A/B/C-light/C'/D+ref-to-ref).
* test/test_e2e.ml "E2E Borrow Graph" suite: 28 hermetic regression tests.
* git log --oneline -- lib/borrow.ml: PR #395 ref-to-ref, #396 C' loop
  soundness, #397 Slice D, #399 whole-place assignment, #400 self-assign
  guard, #407 ADR-022 (Polonius gating).
* CI green on main at 4f0f3ca (2026-05-30 15:19Z).

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

Author: hyperpolymath

docs/TECH-DEBT.adoc

@@ -29,7 +29,7 @@ Stage A  CLOSED ─────────────────────
 Stage B  CLOSED (#215; residual conflicts = ADR-012 won't-fix)  │
 Stage C  CLOSED 2026-05-18 (#128/#135 stdlib AOT)               │
                                                                  ▼
-Stage D  ACTIVE ── CORE-01 (#177)  ─┐                            (base lang
+Stage D  CLOSED ── CORE-01 (#177)  ─┐                            (base lang
          ├─ INT-01 (#178) ──────────┼─ substrate, S1            complete)
          ├─ INT-02 (#179) ──┐       │
          ├─ INT-03 (#180)   │       │
@@ -174,19 +174,38 @@ propagation). Moves/borrows from arm i no longer pollute arm i+1;
 2 hermetic tests in "E2E Borrow Graph" (positive: two catch arms can
 independently move the same value; anti-regression: body-side moves
 still propagate past the try, preserving conservative correctness).
-*Residual (Slices C-full / C' / D):* true Polonius origin/region
-variables on `TyRef`/`TyMut` with subset constraints and a datalog-
-style loan-live-at-point solver (architectural change to the type
-system; ADR-gated); loop soundness via a 2-iteration check on
-`StmtWhile`/`StmtFor` (coupled to a `StmtAssign` clear-on-rewrite
-fix — assignment is currently treated as a read of LHS, so the
-naive 2-iter spuriously fails on legitimate re-assignment loops);
-reborrow through indirection (`r = some_other_ref_var` RHS, parks
-with the let-graph's same restriction); tighter quantity-checker
-integration for captured linears. |S1 |pt1 #240 + pt2 return-escape
-+ `&mut` surface + pt3 Slices A+B+C-light DONE (Refs #177); residual
-= Slices C-full (origin variables, ADR-gated), C' (loop soundness),
-D (quantity integration), plus ref-to-ref binding — issue #177
+*Part 3 ref-to-ref binding LANDED* (PR #395, Refs #177): `let r2 = r`
+and `r2 = r` (where `r` is a ref-binder) extend the borrow-graph by
+aliasing `r2` to the same borrow `r` holds; `ref_source_borrow` unifies
+`&p` / `&mut p` / ref-var cases so `record_ref_binding` and the
+`StmtAssign` reborrow block both reach through one extra level of
+indirection. Closes the reborrow-through-indirection gap.
+*Part 3 Slice C' LANDED* (PR #396, Refs #177): loop soundness via a
+2-iteration check on `StmtWhile`/`StmtFor`. Body runs once; state-fields
+snapshot; cond+body run again from the post-iter-1 state. Body-moves
+that aren't restored surface as `UseAfterMove` on the 2nd pass. Pairs
+with `StmtAssign` clear-on-rewrite (PR #399 `is_whole_place_write`) so
+legitimate re-init loops accept while loops with unrestored body-move
+reject. *Part 3 Slice D LANDED* (PR #397, Refs #177): borrow-side
+rejection of `@linear`-binding capture by a closure. Closures may be
+called 0..N times, so capturing a `@linear`/`QOne` binding lifts its
+consumption count out of the borrow checker's finite-once proof.
+`state.linear_bindings` populated from `[@linear]` / `Cmd _` annotations
+on params, `let`-statements, and `let`-expressions; `ExprLambda`
+rejects free-vars whose sym-id is in that set with
+`LinearCapturedByClosure` (errors at the lambda span, before the
+downstream quantity-checker `QOmega`-scaled "used multiple times"
+diagnostic). *Residual:* true Polonius origin/region variables on
+`TyRef`/`TyMut` with subset constraints and a datalog-style loan-
+live-at-point solver — architectural change to the type system,
+covered by ADR-022 (`docs/decisions/0022-polonius-origin-variables.adoc`,
+PR #407) as a separate workstream; lexical checker is the merge oracle
+through M3 per the ADR migration plan. Tighter quantity-checker
+integration for captured linears is a small remaining nicety, not a
+soundness gap. |S1 |*CLOSED 2026-05-30* (#177) — pt1 #240 + pt2
+return-escape + `&mut` surface + pt3 Slices A+B+C-light+C'+D + ref-to-
+ref binding DONE; residual Polonius work is ADR-022 (#407), a separate
+workstream
 |CORE-02 |Effect-handler dispatch on WasmGC (was `UnsupportedFeature`;
 the chosen path is CPS over the EH proposal). The #225 CPS line closed
 the async slice; #234 generalised the boundary recogniser from a