diff --git a/design/INDEX.md b/design/INDEX.md
index 1ffbe9f..a27fd0e 100644
--- a/design/INDEX.md
+++ b/design/INDEX.md
@@ -83,7 +83,7 @@ is the default.
 | authoring-surface    | LLM author / stable           | crates/ailang-surface/tests/round_trip.rs       | design/contracts/0001-authoring-surface.md |
 | roundtrip-invariant  | every release / stable        | crates/ailang-surface/tests/round_trip.rs       | design/contracts/0009-roundtrip-invariant.md |
 | language-constraints | LLM author / stable           | crates/ailang-check/src/uniqueness.rs (in-source mod tests) | design/contracts/0015-language-constraints.md |
-| memory-model         | LLM author / stable           | crates/ailang-check/src/uniqueness.rs (in-source mod tests) | design/contracts/0008-memory-model.md |
+| memory-model         | LLM author / stable           | crates/ailang-check/src/uniqueness.rs + linearity.rs (in-source mod tests) | design/contracts/0008-memory-model.md |
 | data-model           | LLM author / stable           | crates/ailang-core/tests/design_schema_drift.rs | design/contracts/0002-data-model.md |
 | mangling             | codegen / stable              | crates/ail/tests/eq_ord_e2e.rs            | crates/ailang-codegen/src/lib.rs //! |
 | env-construction     | codegen / stable              | crates/ailang-check/tests/duplicate_ctor_pin.rs | crates/ailang-codegen/src/lib.rs //! |
diff --git a/design/contracts/0008-memory-model.md b/design/contracts/0008-memory-model.md
index d245699..1ea5129 100644
--- a/design/contracts/0008-memory-model.md
+++ b/design/contracts/0008-memory-model.md
@@ -337,15 +337,22 @@ twice (double-free under a hypothetical Consume + scope-close).
   subsequent work added codegen consumers, not new schema fields.
 - Does not introduce a new `Type` variant. Mode metadata stays
   flat on `Type::Fn` (see "Schema additions" above on why).
-- Covers let-aliases of borrowed values (spec 0064, class 2). A
-  let-binder whose value is a bare `Term::Var` resolving to a
-  tracked binder is recorded as an alias to that root in the
-  linearity walk (`crates/ailang-check/src/linearity.rs`,
-  `Checker.aliases` + `resolve_alias`); the binding does not
-  consume the source, and every binder-state lookup resolves
-  the alias to its root, so a borrow-position use of the alias
-  does not consume the root while a real double-consume through
-  the alias is still caught.
+**Let-aliases of borrowed values are propagated** (no longer a
+carve-out). A let-binder whose value is a bare `Term::Var`
+resolving to a tracked binder is treated as an alias of that
+source on both axes of the ownership analysis:
+
+- the linearity diagnostic (spec 0064, class 2) records `a →
+  root` in the walk (`crates/ailang-check/src/linearity.rs`,
+  `Checker.aliases` + `resolve_alias`) and resolves every
+  binder-state lookup to the root, so a borrow-position use of
+  the alias does not consume the source while a real
+  double-consume through the alias is still caught;
+- the codegen drop gates (`crates/ailang-codegen/src/lib.rs`,
+  the `MTerm::Let` lowering's `current_param_modes` mode
+  inheritance) give the let-binder its source's mode, so the
+  scope-close drop gate treats an alias of a borrow as borrowed
+  and emits no spurious `dec`.
 
 Ratified by: `crates/ailang-check/src/uniqueness.rs`,
 `crates/ailang-check/src/linearity.rs`.