diff --git a/BUILT.md b/BUILT.md
index 7723cd4..bf285ba 100644
--- a/BUILT.md
+++ b/BUILT.md
@@ -1637,14 +1637,192 @@ nothing marked it — which is precisely what a static rule cannot see.
 exists for is not implemented: a slice is ptr+len and has nowhere to carry the Vec's identity or its generation. Said
 plainly here rather than implied by the word's presence in the header.
 
-### What this leaves for steps 4 to 7
+### What this leaves for steps 5 to 7
 
-`(Map K V)`; `drop` and with it the transitive move-only rule, recursive teardown, and the refusal to construct a
-drop-carrying container against an allocator without `can-free`; `(Result T E)` and `try`; generics; the macro expander.
+`(Map K V)` is built — see below. What is left: `drop` and with it the transitive move-only rule, recursive teardown,
+and the refusal to construct a drop-carrying container against an allocator without `can-free`; `(Result T E)` and
+`try`; generics; the macro expander.
 And the **accumulation pattern** — `(fn [c] (push errors c) ...)` over an enclosing Vec — which `Vec` does not buy:
 capture does not exist at all, and the spec's captured-`Vec`-by-pointer rule has never had to exist because every
 capturable type today is a value type. It is its own item and should be planned as one.
 
+## `(Map K V)`, which is Odin's map
+
+Step 4 of the container build order, over the runtime `Vec` already established. `spec-memory.md` is followed as
+written; the two places this departs from *Odin* are named below, and there is one amendment to the spec and one
+restriction under it.
+
+### The three properties that were the point
+
+Odin's header states them and they are why it was the thing to follow (`base/runtime/dynamic_map_internal.odin`).
+
+- **Open-addressed Robin Hood hashing at a 75% load factor.** No buckets and no per-entry allocation: one block holds
+  every key, every value and every hash. Robin Hood is the part that earns its keep — on insert, an element that is
+  further from the slot its hash wanted than the occupant it is looking at takes the slot and sends the occupant on.
+  Probe distances even out, and a lookup may stop the moment it is further from home than the occupant it is looking
+  at, because no element is ever further from home than one it passed. That early exit is why a miss costs about what
+  a hit does.
+- **Cache-line cell packing.** A flat `[capacity]K` array lets one key straddle two cache lines, so a probe walking
+  four slots can touch five lines. A cell packs as many `K` as fit in 64 bytes and pads the rest, so no key ever
+  straddles a line. Keys, values and hashes are three separate runs, so a probe — which reads hashes, and only then
+  one key — touches hash lines and nothing else until it has a candidate.
+- **Pointer-width integers throughout**, so no sign extension or masking gets into the probe loop.
+
+### Two departures from Odin, both deliberate
+
+**There are no tombstones**, because `spec-memory.md` defers removal ("Move-aware lookup, removal, and owned entries
+are deferred"). A slot is empty or occupied and nothing else, which deletes Odin's backward-shift loop entirely — it
+is the single largest reason this file is shorter than the original. When removal arrives, that loop is what it costs.
+
+**The header does not tag the capacity into the data pointer.** Odin stuffs `log2cap` into the low six bits because
+its `Raw_Map` must be three words. This header already carries an allocator, a generation and an epoch, so the tagging
+would buy nothing, cost a mask on every access, and — the part that actually matters — make correctness depend on the
+block being 64-byte aligned. Alignment is *requested*; an arena whose base is not cache-aligned now gives a slower map
+rather than a wrong one.
+
+The header is six words, 48 bytes, the same as a `Vec`'s and for the same reason: a layout that changes with a build
+flag can disagree across the reload boundary.
+
+    data  len  log2cap  allocator  gen  epoch
+
+### The hash and equality pair, and why most key types do not get one
+
+`spec-memory.md` restricts keys to built-in structural types and makes hashing and equality compiler-provided
+structural operations. So there is no dispatch to design: a key type resolves to a pair of symbols, passed to the
+type-erased runtime the way Odin hangs two contextless `proc`s off a `Map_Info`.
+
+Most key types need nothing emitted. A key whose equality is bytewise and whose bytes are all present — every integer,
+enum, bool, and fixed array of those — is served by one runtime pair over `(pointer, size)`. Two kinds are not, and
+the reasons are worth keeping because they are what a bytewise shortcut would have got wrong:
+
+- a **string** is ptr+len and its bytes are elsewhere, so two equal strings at different addresses must hash alike;
+- a **struct** may have padding, whose bytes are indeterminate — two structs equal field by field can differ bytewise
+  — and it may hold a string, which brings the first problem inside it.
+
+A struct therefore gets a pair emitted for it, walking its fields in declaration order and addressing nothing but
+fields. Two maps with the same key type share one pair, and a struct reached twice through two fields emits one.
+
+`Tast.FnAddr` is what carries the symbol, and it is **not** a function value: nothing in the surface language can
+produce one, name its type, or call through it. It is the same escape the allocator used — the one NEXT.md predicted
+would work — and `reach.ml` learned the edge, because a function reached only by address is invisible to the
+reachability walk otherwise. That was already true of handler clauses.
+
+A pair emitted for a struct is an ordinary Flan function, so its signature ends with the transfer channel like every
+other. The runtime's typedef spells that pointer out rather than hoping nothing writes through it, and each built-in
+hasher exists in two spellings — the pointer form that matches the typedef, and the direct form an emitted hasher
+calls per field, which has no channel to hand on.
+
+### The surface
+
+| Name | What |
+|---|---|
+| `(map-new)` `(map-new K V)` `(map-new a)` `(map-new K V a)` | a new map; the pair may be omitted where the context says |
+| `(put m k v)` | upsert, `Unit` |
+| `(get m k)` | `(Option V)` — absence is `None` |
+| `(has-key? m k)` | `bool`, copying no value |
+| `(len m)` `(reserve m n)` `(clone m)` `(clone m a)` `(free m)` | extended, not duplicated |
+
+`len`, `reserve`, `clone` and `free` were **extended rather than given map-shaped names of their own**, which is what
+`at` and `len` already did for `Vec`: one question, one word. `reserve`'s `n` is entries, not slots — the runtime sizes
+the block so `n` still sits under the load factor, which is the only reading of "room for n" that does not reallocate
+on the nth put.
+
+`get` builds the `Option` in the checker, not the runtime, which has no idea what an `Option`'s layout is; keeping it
+that way is what lets one entry point serve every value type. `put` and `get` bind their arguments to slots before the
+allocation guard, so a `retry` re-attempts the allocation and not the expressions that produced the key and value.
+
+**`{K V}` is the type spelling and there is no map literal.** A bare map form in expression position is a struct
+literal's field list, and giving the same braces two meanings is what the colon-to-dot change was for. A map is built
+with `map-new` and filled with `put`.
+
+### The refusals, each by name
+
+- A **float key** — not a milestone question, which is why it is said separately. NaN is not equal to itself, and
+  `0.0` and `-0.0` are equal while differing bytewise. There is no equality there for a map to hash.
+- A **`Ptr`, slice, `Vec` or `Map` key** — would hash an address rather than what it points at, which is a different
+  operation.
+- A **fixed array whose elements are not compared bytewise** — an array of structs or of strings needs the
+  per-element walk a struct key gets, driven by a loop rather than a field list. Nothing has wanted one, so it is
+  refused rather than written untested, and the shape that does work (a struct holding the array) is named beside it.
+  **This is narrower than the spec**, which lists fixed arrays without qualification.
+- A **move-only value** — the refusal `(Vec (Vec T))` already carries, for the identical reason: the runtime copies
+  entries bytewise, so `clone` would duplicate headers and `free` would leak what they own. Owned entries arrive with
+  `drop`.
+- **`Unit` as a value** — there is nothing to store, and the cell geometry divides a cache line by the element size.
+  Named rather than left to divide by zero, because it is the natural spelling of a set.
+
+`StorageExhausted` under `retry` holds over `map-new`, `put`, `reserve` and `clone`, reusing the machinery that landed
+with `Vec`; no operation returns an error. A map is the harder of the two containers for that rule, and
+`map-exhausted.flan` is why it gets its own program: a `Vec`'s failing allocation leaves the `Vec` untouched, whereas a
+map's growth allocates a new block, rehashes into it, and only then releases the old one — so a failure partway must
+leave the map exactly as it was, or the retry re-attempts against a half-moved map.
+
+The epoch trap covers the map too, and `map-stale-region.flan` is separate from `stale-region.flan` because the two
+reach the check by different routes: a `Vec`'s operations check on the way in and stop there, while a map's `get` goes
+on to call a hash and an equality function through pointers into the block. A missing check there is not a wrong
+number, it is a probe loop walking released memory.
+
+### Is this another Python dict? — measured
+
+The question was asked directly and the answer is that **Python's algorithm is fine**. What makes CPython's dict slow
+is that every key and every value is a separately allocated, reference-counted object and hashing goes through
+`__hash__` and `__eq__` calls that cannot be inlined. This map stores raw bytes in the block and compiles hashing and
+comparison concretely per key type. That is most of the gap before any cleverness.
+
+Measured on this machine, `i64` to `i64`, against CPython 3.13's dict on the same workload:
+
+| Working set | Flan | CPython dict |
+|---|---|---|
+| 10k entries, 10M lookups (cache-resident) | 21 ns/lookup | 132 ns/lookup |
+| 1M entries, 10M puts + 10M lookups | 1.41 s | 1.16 s |
+
+**Six times quicker cache-resident, and slower at a million entries** — and the second row is written down rather than
+left out. Both are waiting on memory there, and this layout waits longer: keys, values and hashes are three separate
+runs, so a lookup that misses everything takes three cache misses where a compact dict takes two, and the hash run is a
+full eight bytes a slot. Cell packing buys probe locality, which is a win while the hash run is resident and a loss
+once nothing is. One byte of metadata a slot — the Swiss-table arrangement — is the known answer and is not built.
+
+The path from 35 ns to 18 ns (the cache-resident floor, at 500 entries) was **profiled, and the first two guesses were
+both wrong**: the per-slot cell division and the block-size divisions were each replaced first and neither moved the
+number. What did: FNV one byte at a time became eight, and a key that is one machine word became one load and one mix
+with no loop; equality on eight bytes stopped being a call into libc's vectorised `memcmp`, and copying a value out
+stopped being a call into `memmove`; the block geometry stopped being recomputed five times over in a function that ran
+twice per lookup; and the seed stopped being a five-multiply avalanche on the critical path for mixing the hasher does
+again immediately after. `64/size` is a table, which is Odin's `Map_Cell_Info` by another route — Odin precomputes it
+per type because the probe loop must not divide, and here the sizes arrive as ordinary arguments.
+
+What remains at 18 ns is the type erasure itself: a non-inlinable call into the runtime and two non-inlinable indirect
+calls to the pair. That is the trade `spec-memory.md` chose deliberately — "It is type-erased on purpose… No generics
+are involved, and none are needed" — and monomorphisation is what would buy it back, at the cost the spec declined.
+
+## `defer` may be written in a `let`
+
+The whole of this project's resource-cleanup answer, and NEXT.md records `drop` and a `with-cleanup` form as both
+considered and rejected before it.
+
+`defer` is a **compile-time** construct: the cleanup is copied into every exit path of the function. That is why a loop
+body and a branch stay refused — a loop body's would fire once at function exit rather than once per iteration, and a
+branch would have to express "maybe registered", which a form copied into every exit path or into none cannot say.
+
+A `let` is neither. It is not a frame here: its bindings are function slots like any other and **nothing is released at
+scope exit**, so a `let` at the top level of a function body has exactly the function's extent and a `defer` written in
+it always registers. It was refused for a reason that does not apply to it.
+
+The rule, stated precisely, because "top level of a function body" is easy to get wrong: a form at the top level of the
+body may carry one, and so may a form in the body of a `let` that itself may — to any depth. A `let` inside a `while`
+or an `if` has the loop's extent or the arm's, and inherits the refusal rather than the permission.
+
+The implementation detail worth keeping: **the permission is granted again before every form of a body, never once
+around the body.** `check` withdraws it as it starts, so granting it once would let the first `defer` through and refuse
+the second — and two resources acquired in one `let` is the case this exists for. `defer-let.flan` covers exactly that,
+along with nesting, interleaved registration order across the `let` boundary, and an early return.
+
+This **amends `spec-memory.md`**, which states under "When storage is released" that `(defer (free v))` for a
+`let`-bound `v` is "not expressible today" and that no idiom in the spec may depend on it. It is expressible now.
+
+`do` at the top level of a body has the same extent argument and is deliberately **not** included: nothing asked for it,
+and the rule is easier to state and to trust with one construct in it.
+
 ## Assets are baked in, and the reason it is a compiler feature
 
 NEXT.md decision 1. `(embed "brush.png")` is a `[u8]`, `(embed "brush.png" string)` is a `string`, and
diff --git a/NEXT.md b/NEXT.md
index f0d0c03..fa712b6 100644
--- a/NEXT.md
+++ b/NEXT.md
@@ -73,6 +73,29 @@ the commit that made it.
    `-2851001042534928384` — the same 64 bits, printed unsigned now that `hash-grid`'s `u64` no longer goes through an
    `(i64 …)` cast — and a trap column shifted because the call it names got shorter.
 
+### Landed — `(Map K V)`, and `defer` in a `let`
+
+Step 4 of the container build order, following Odin: open-addressed Robin Hood hashing at a 75% load factor,
+cache-line cell packing, pointer-width integers through the probe loop. Two deliberate departures from Odin — no
+tombstones, because `spec-memory.md` defers removal, which deletes the backward-shift loop entirely; and no capacity
+tagged into the data pointer, because this header has room for it and tagging would make correctness depend on an
+alignment that is only ever requested.
+
+**One amendment to a frozen `spec-memory.md`, and it is the `defer` half**: the spec says under "When storage is
+released" that `(defer (free v))` for a `let`-bound `v` is "not expressible today" and that no idiom may depend on it.
+It is expressible now. A `let` at the top level of a function body has exactly the function's extent — a `let` is not a
+frame here, and nothing is released at scope exit — so a `defer` in one always registers. A loop body and a branch stay
+refused, by name, for the reason that does apply to them.
+
+**One restriction the spec does not have**: a fixed array is a map key only when its elements compare bytewise, so an
+array of structs or of strings is refused by name. A struct key holding the array works, because a struct key is walked
+field by field.
+
+The measured answer to the author's "is this another Python dict": **six times quicker cache-resident and slower at a
+million entries**. Python's algorithm is fine — what makes it slow is a separately allocated refcounted object per key
+and value, and hashing through calls that cannot be inlined. The second half of that result is the interesting one and
+is written down rather than left out; see the unsettled list under the build order.
+
 ### Landed — the allocator, the arena, `(Vec T)`, `StorageExhausted`
 
 The critical path, and the thing NEXT.md said was the only one standing between this and writing a game. Steps 1, 2 and
@@ -418,9 +441,12 @@ run one lane at a time; item 4 is disjoint and runs alongside any of them.
    old spelling and their files want the same pass at merge — `python3 tools/colon-to-dot.py .` over the tree, and
    `--in-strings` for a `test/*.ml` that embeds Flan.
 
-3. **`Map`, and the `defer` relaxation.** `Map` is step 4 of the container build order and finishes what `Vec` started.
-   The `defer` change — permitting it in a `let` whose extent is the function body — is small, independent, and is the
-   whole of the resource-cleanup answer.
+3. ~~**`Map`, and the `defer` relaxation.**~~ **Both done.** See *`(Map K V)`, which is Odin's map* and *`defer` may be
+   written in a `let`* in [`BUILT.md`](BUILT.md). The `defer` relaxation **amends `spec-memory.md`**, which said
+   `(defer (free v))` for a `let`-bound `v` was not expressible; it is now. `Map` restricts one thing the spec does not:
+   a fixed array is a key only when its elements compare bytewise, so an array of structs or of strings is refused by
+   name. The measured answer to "is this another Python dict" is six times quicker cache-resident and *slower* at a
+   million entries, and the second half is the interesting one — see below.
 
 4. **The Emacs batch. Disjoint from the compiler, so it runs in parallel with anything above.** Globals in the break
    buffer; the buffer opening itself when the program stops; the indentation rewrite with `clojure-mode` as the
@@ -792,9 +818,13 @@ expander last, on 6's unions.
    backend learned nothing about allocation. `test/programs/exhausted.flan` exhausts an allocator for real and takes the
    restart; `exhausted-unhandled.flan` is the same failure with nothing handling it.
 
-4. **`(Map K V)`** — flat open-addressed key and value arrays, with a compiler-emitted hash and equality pair per key
-   type passed as arguments. `spec-memory.md`'s structural-key restriction holds this to the built-in key set, so there
-   is no dispatch to design.
+~~4. **`(Map K V)`**~~ **Done**, following Odin: open-addressed Robin Hood hashing at a 75% load factor, cache-line
+   cell packing, and pointer-width integers through the probe loop. `map-new`, `put`, `get`, `has-key?`, and `len`,
+   `reserve`, `clone` and `free` extended rather than duplicated. Two departures from Odin, both deliberate: no
+   tombstones, because the spec defers removal, which deletes the backward-shift loop entirely; and no capacity tagged
+   into the data pointer, because this header has room and tagging would make correctness depend on an alignment that
+   is only requested. `Tast.FnAddr` carries the emitted hash and equality pair and is not a function value — the same
+   escape the allocator used.
 5. **`drop`.** The hook, the transitive move-only and non-`clone`able rules, and the refusal to construct a
    `drop`-carrying value against an allocator without `can-free`. It is additive — no type in the repo has a hook today
    — but the `can-free` refusal has to land with the construction path it guards, before any arena-allocated container
@@ -807,6 +837,22 @@ expander last, on 6's unions.
 
 **What is genuinely unsettled.**
 
+- **The Map is slower than CPython's dict at a million entries** (1.41s against 1.16s on the same workload), while
+  being six times quicker cache-resident (21ns against 132ns per lookup at 10k entries). Both are memory-bound at the
+  larger size and this layout waits longer: keys, values and hashes are three separate runs, so a lookup that misses
+  everything costs three cache misses where a compact dict costs two, and the hash run is a full eight bytes a slot.
+  Cell packing buys probe locality, which is a win while the hash run is resident and a loss once nothing is. One byte
+  of metadata a slot — the Swiss-table arrangement — is the known answer and is not built. Worth measuring before
+  building: the crossover is somewhere between 10k and 1M and nobody has found it.
+- **What is left at 18ns cache-resident is the type erasure itself** — one non-inlinable call into the runtime and two
+  non-inlinable indirect calls to the hash and equality pair. That is the trade `spec-memory.md` chose on purpose, and
+  monomorphisation is what would buy it back. It is a reason to want generics, not a reason to regret the choice.
+- **A fixed array of structs or of strings is not a map key**, which is narrower than `spec-memory.md`'s key set. It
+  needs the per-element walk a struct key gets, driven by a loop rather than a field list. Refused by name rather than
+  written untested; a struct holding the array works today.
+- **Map removal is not built**, which is what keeps the implementation free of tombstones and of Odin's backward-shift
+  loop. The spec defers it deliberately. When it arrives, that loop is the cost.
+
 - `spec-memory.md`'s "Open: catching a use-after-release statically" is still open, and it is now open with evidence
   available for the first time: the epoch trap is built and `test/programs/stale-region.flan` is the case it catches.
   What the spec says would settle it — real Flan programs using arenas, to show whether the escapes that actually occur