Point 5 of the Main3.ck header: `with mut` over a record-typed local did not
lower, so a plex's changing state had to be carried as loose scalars beside it.
The refusal was never about the target — a `let mut` record local is registered
in `mut_records` and both its projections already lowered (`w.f with mut e`,
`w with mut { f: … }`). It was about the VALUE: the whole-value arm demanded a
headless brace, and anything else — a record-returning call, another record
local, a `with`-update — fell through to `WithMutTarget`.

A record local's value IS a frame base, so there were two ways to close it and
only one is CkLang. Re-pointing the local at the replacement's base is one line
and aliases two live records onto one frame; copying the replacement's words
over the target's own frame keeps one record per frame and needs no threading
for a value that does not ride a register. `algorithms_DFS_trapped/trap.md` had
already priced it and chose the copy; this is that arm, written where the trap
said it belonged.

`copy_record_into` is `record_lower::lower_with_update`'s copy aimed at an
EXISTING frame instead of a fresh one — the source is materialized whole first
(so `w with mut f(w)` reads the target before the first store lands on it),
then one `Load`/`Store` per slot, matched by NAME and refused as
`LowerError::RecordLayout` if the field count or a slot's word shape disagrees.
No new allocation: `lower_record_like` returns the source's base, it does not
build a second one.

  - `store_whole_record` is the one dispatcher for `record with mut <value>`:
    brace → the per-field overrides that already worked, record-like → the
    copy, anything else → the honest `WithMutTarget` at the same span as
    before. `store_record_overrides` now takes the collected overrides, so its
    unreachable `ok_or` is gone rather than left as dead honesty.
  - `LowerError::WithMutTarget`'s rendering listed two mutable families and had
    been stale for three slices (the record field store, the brace, the list
    element all lower). It now names what lowers and what does not — Law 3: a
    diagnostic that describes the compiler of a year ago is prose stating
    behavior, and prose is deleted, not trusted.
  - `tests/corpus/ml_othello` is the corpus carrier: `Othello::apply_move` and
    `flip_ray` fold a `Board` with `acc with mut next`. Both are now FULLY
    BOUNDED — `flip_ray` 7024 B + unbounded → 7560 B, `apply_move` 8800 B +
    unbounded → 10424 B. The numbers grew because a body that did not lower had
    no measurable allocations at all; what is counted now is one Board-sized
    return area per record-returning call, which was always there and merely
    unpriceable. `tests/sizes_pin/unbounded_inventory.txt` drops 262 → 239
    components: 23 rows, every one `corpus/ml_othello … WithMutTarget`, nothing
    added. The `ml_othello` door carrier stays listed — its remaining 133
    WithMutTarget rows are the LIST local's whole-value rebind
    (`acc: List<Int, 64> with mut next`), a different mechanism and its own
    open cell.
  - Cells: `with_mut_record_valued_expr` flips `lower: WithMutTarget` → `runs: 4`
    and gains the `// STATUS:` marker it never had (UNMARKED_CELL_COUNT
    148 → 147). One cell added — `record_let_mut_whole_value_replace_in_a_loop`,
    `runs: 31` — because a record local does NOT thread through loop head
    params, so a replace that re-pointed instead of writing through would read a
    stale frame on the second trip, and that is the claim worth a cell of its
    own (CELL_COUNT 428 → 429). BROKEN_CELL_COUNT does not move: the flipped
    cell was unmarked, not marked BROKEN.
  - The `a_test_body_that_does_not_lower_*` PAIR is re-aimed, not retired. Its
    law is the EMISSION boundary — a test body is lowered by `ckc test` and not
    by `ckc run` — and it needs a construct that does not lower to say so. The
    old construct was this slice's gap; the new one is the nested field path
    (`q.Home.Street with mut …`), still `lower: WithMutTarget`, still
    byte-identical across the two halves, which is the whole discriminator.
  - Nested field paths and the list local's whole value are untouched. They
    refuse through different mechanisms — a second projection to walk, and a
    two-word descriptor with nothing to thread — and their cells stay BROKEN.

Gate: NOT RUN (owner instruction, thermal). Verified narrowly and without a
container: fmt clean, clippy 0 warnings on ck_lower + ck_driver, ck_lower --lib
23 passed, architecture 38 passed (mut_lower.rs 525 ≤ 540, worst fn 57 ≤ 71),
frame_reconcile 2 passed — NO frame pin moves, ml_othello still does not reach
the run path — corpus + sizes_query 21 passed, unbounded_inventory re-pinned and
green. `tests/sizes_pin/ml_othello.pin` DOES move (the `ckc sizes` section, 73
lines) and is deliberately left unblessed for review.

@@ -78,3 +78,3 @@
 /// - **deleting cells** fails too. A cell is only legitimately removed when the
 ///   law it pins stops existing; that is a deliberate act, not a side effect.
-const CELL_COUNT: usize = 428;
+const CELL_COUNT: usize = 429;

@@ -417,0 +418,4 @@
+         slot's own frame bytes), and a `let mut` list local's element — a \
+         nested field PATH, a list local's whole value, and a target that is \
+         not a mutable binding at all land with their own slices (the M4 \
+         ownership checker + the wide-local half of the register law)"

@@ -344,0 +398,4 @@
+                ExprKind::Load {
+                    addr,
+                    offset,
+                    repr: slot.repr.clone(),