diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 03b742c..9539aac 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -712,14 +712,6 @@ Trade-offs accepted:
   build host. Users without it get a link-time error from
   clang, not a silent failure.
 
-A future iter may layer a per-fn-arena optimisation on top: when
-a fn's return type contains no boxed ADT, ADT boxes allocated
-inside that fn cannot escape, so an arena freed at fn return is
-sound by construction. That requires
-escape analysis, the corresponding AST/IR plumbing, and is its
-own design pass. Boehm-everything is the floor; arena is an
-optimisation above it.
-
 ### Per-fn arena via stack `alloca`
 
 This optimisation is layered on top of Boehm in its simplest form.
@@ -1013,10 +1005,10 @@ makes them load-bearing rather than incidental:
    guarantee that any value graph reachable from a binding is a
    DAG. The reference graph has no cycles. (Follows from 1–3.)
 
-A future iter that proposes any of laziness, recursive value
-bindings, shared mutable state, or any feature that creates
-cycles must either prove the cycle is collectible by an
-extension (e.g. linear ownership) or be rejected at design time.
+Laziness, recursive value bindings, shared mutable state, or any
+feature that creates cycles is rejected at design time unless the
+proposal proves the cycle is collectible by an extension (e.g.
+linear ownership).
 
 ### Schema additions
 
@@ -1083,9 +1075,7 @@ identical: `param_modes` is skipped when every entry is
 `Implicit`, `ret_mode` is skipped when `Implicit`. Existing
 modules emit the same bytes as before.
 
-The legacy `(con T)` form is treated as `(own T)` semantically;
-a future iteration (deferred) makes the explicit annotation mandatory
-and rejects `Implicit` for boxed parameter types.
+The legacy `(con T)` form is treated as `(own T)` semantically.
 
 (An incidental observation, not a design reason: keeping `Type`
 itself unchanged also avoids touching ~250 sites across the
@@ -1341,8 +1331,7 @@ backstop. The answer is a separate ownership/linear extension
 that gates mutability behind static single-owner discipline. RC
 + uniqueness is the universal floor; ownership extends it for
 specific high-performance primitives without rebreaking the
-acyclicity invariant. Concrete design deferred until the need
-materialises with a real workload.
+acyclicity invariant.
 
 ### What this Decision deliberately does not do
 
@@ -1663,11 +1652,8 @@ end-to-end path is the milestone's typeclass acceptance gate
 `instance Foo IntBox`); see `docs/specs/2026-05-09-22-typeclasses.md`
 "Amendments" for the substantive rationale.
 
-A future milestone may add a Prelude when concrete LLM-author code
-surfaces a case that benefits from `Show a` / `Eq a` / `Ord a`
-over per-type primitive functions. Until then, primitive output
-goes through `io/print_int` / `io/print_bool` / `io/print_str`
-directly.
+Primitive output goes through `io/print_int` / `io/print_bool` /
+`io/print_str` directly.
 
 `==`, `<`, `<=`, `>`, `>=` REMAIN primitive operators (unchanged
 from the original draft). Class methods are accessed by name (`eq x y`,