diff --git a/docs/specs/0064-harden-ownership-analysis-part-2.md b/docs/specs/0064-harden-ownership-analysis-part-2.md
new file mode 100644
index 0000000..27060e5
--- /dev/null
+++ b/docs/specs/0064-harden-ownership-analysis-part-2.md
@@ -0,0 +1,508 @@
+# Harden the ownership analysis for universal activation, part 2 — Design Spec
+
+**Date:** 2026-06-01
+**Status:** Draft — awaiting user spec review
+**Authors:** orchestrator + Claude
+
+## Goal
+
+Close the remaining precision gaps in the strict linearity analysis
+(`use-after-consume` / `consume-while-borrowed`,
+`crates/ailang-check/src/linearity.rs`) so that deleting
+`ParamMode::Implicit` (#55, spec 0062) does not turn part of the
+migrated corpus red. This is the **second hardening pass** —
+`#56` (spec 0063, plan 0120) closed two false-positive classes
+(value-type *params*; application-is-a-borrow). Executing the #55
+cutover (plan 0121, Task 4) surfaced **three more** false-positive
+classes plus **one genuine corpus over-consume** that no mode
+annotation can fix:
+
+1. **Local function-typed binder modes (false positive).**
+   `callee_arg_modes` (`linearity.rs:750`) resolves the param-modes of a
+   call's callee only for **global** fns; a local function-typed binder
+   (a HOF predicate param such as `std_list.filter`'s `p`) returns an
+   empty mode vector, so every arg of `(app p h)` defaults to `Consume`.
+   `filter` then reuses `h` in the kept `Cons` after `(app p h)`
+   "consumed" it → false `use-after-consume`. Blocks `std_list.filter`
+   and its importers.
+2. **`let`-alias of a borrowed value (false positive).** `Term::Let`
+   walks its value in `Position::Consume` (`linearity.rs:506`).
+   `(let a t (match a …))` over a `borrow`-mode `t` therefore *consumes*
+   `t` at the binding, tripping `consume-while-borrowed`.
+   `design/contracts/0008-memory-model.md:340` documents this
+   propagation as explicitly **not shipped**.
+3. **Inferred value-typed `let`-binders (false positive).** A
+   `let`-binder of an unboxed value type (`Float` etc.) is installed as
+   a default `BinderState` with `is_value = false` (`linearity.rs:507`),
+   so a value-typed `let`-binder used more than once trips
+   `use-after-consume`. Spec 0063 deferred exactly this class
+   ("value-typed `let`-binders … deferred until a corpus shape demands
+   it"); `eqord_3_newton_sqrt.iterate`'s `(let xnew (app / …) …)` is
+   that shape. No mode annotation applies — the binder's type is
+   inferred, not annotated.
+4. **Genuine double-consume (real corpus bug, NOT a false positive).**
+   `std_either_list.partition_eithers` projects both `(app Pair.fst
+   rest)` and `(app Pair.snd rest)` from one owned `rest`. `Pair.fst` /
+   `Pair.snd` are `own`-param projections that move a field out, so each
+   consumes `rest` → `rest` is genuinely consumed twice without a
+   `clone`. The fix is a body rewrite (destructure `rest` once), out of
+   the migration's mechanical scope; the check correctly stays RED on
+   the unrewritten shape.
+
+Classes 1–3 are precision gaps the gated-off `Implicit` activation was
+hiding; class 4 is a real fixture over-consume. This is the
+**precondition for #55**: spec 0062 §8 asserts the migrated corpus
+"contains none" of the rejected shapes, which only holds once classes
+1–3 are closed and class 4 is rewritten.
+
+The rationale anchors are `design/models/0008-ownership-totality.md` §4
+(HOF mode slots — a function param is applied, which is a read) and
+§3.2 (value types are trivial-`own`), plus the RC/uniqueness contract
+`design/contracts/0008-memory-model.md` (whose `:340` let-alias
+carve-out this cycle closes). The model is `status: Design
+exploration`; its claims are validated against the live tool below
+(Testing strategy), not assumed.
+
+### Scope decisions ratified here
+
+1. **The let-binder type is teed out of the type-checker, not
+   re-inferred.** The inferred type of every `Term::Let` binder is
+   *already computed* at `synth`'s `Let` arm (`lib.rs:3808`, `let v =
+   synth(value, …)`) and then **discarded**. The fix records it into a
+   `(def, binder) → Type` table returned alongside the typecheck
+   diagnostics; linearity reads the table. This is the "stop discarding
+   known information" fix, not the "re-run inference in the linearity
+   walk" anti-pattern that aaa70d4 / spec 0063 ruled out. The table is
+   the chosen mechanism for classes 1 (function-typed `let`/`lam`
+   binders) and 3 (value-typed `let` binders) uniformly. *(User
+   decision, 2026-06-01.)*
+
+2. **Parameter and `lam`-param modes/types stay signature-local.** A
+   parameter's fn-type (with `param_modes`) and a `lam`-param's type are
+   already on the signature where the linearity walk installs the binder
+   (`check_fn` has `param_tys`; `Term::Lam` carries `param_tys`). These
+   continue to be read from the signature — the type table is only
+   needed for `let`-binders, whose type is not locally annotated. The
+   corpus driver for class 1 (`filter`'s `p`) is a **param**, so its
+   mode resolution is signature-local; the table generalises class 1 to
+   `let`/`lam`-bound function values for free.
+
+3. **The `let`-alias fix is an alias *redirect*, not a state clone.**
+   `(let a t body)` where `t` is a bare `Term::Var` resolving to a
+   tracked binder records `a → root(t)` in an alias map for the body
+   scope and does **not** walk `t` in `Consume`; `use_var`, the `App`
+   borrow-count bump, and `callee_arg_modes` resolve a name through the
+   map first. A clone of `t`'s state would be **unsound** — `(let a t
+   (seq (consume a) (consume t)))` would mark two independent binders
+   and miss the double-consume. The redirect keeps consume/borrow
+   bookkeeping on the single root, so a real double-consume through an
+   alias is still caught.
+
+### Out of scope
+
+- **#55 itself** — deleting `ParamMode::Implicit`, the schema/hash
+  reset, the parser/return changes (spec 0062). This spec only hardens
+  the analysis; it changes no schema, resets no hash, and is testable
+  **today** against explicit-mode fns (Testing strategy).
+- **Re-running inference in the linearity walk.** Ruled out by aaa70d4
+  and reaffirmed here; the type is teed, never recomputed.
+- **`Str` consume semantics.** Unchanged — `Str` stays heap
+  (`is_value_type` excludes it, spec 0063 scope decision 1).
+- **The `over-strict-mode` lint.** Untouched. (It emits a benign
+  Warning on the `fst`/`snd` projection helpers; that is pre-existing
+  and orthogonal.)
+
+## Architecture
+
+Four additive changes, no schema change, no new `Type` variant, no hash
+shift, no codegen change. The analysis stays a pure diagnostic pass.
+
+**New type-checker output (`crates/ailang-check/src/lib.rs`):**
+
+A `LetBinderTypes` table, `HashMap<(String, String), Type>` keyed
+`(def_name, binder_name)`, populated at the `synth` `Term::Let` arm
+(`lib.rs:3808`) with the binder's resolved inferred type, and threaded
+out of `check_in_workspace` / `check_workspace` to the linearity
+dispatch. One insert, the value already in hand; the cost is plumbing
+the table through the two pass functions and into the `Checker`.
+
+**Fix 1 — local function-typed binder modes (`linearity.rs`):**
+
+`BinderState` gains `fn_param_modes: Option<Vec<ParamMode>>`. It is
+seeded at every binder-introduction site whose binder is function-typed:
+params and `lam`-params from the locally-available signature type;
+`let`-binders from the `LetBinderTypes` table. `callee_arg_modes`, for a
+local `Var` callee, reads the callee binder's `fn_param_modes` before
+falling back to the global symbol table. A local HOF predicate's
+declared arg modes then resolve, so its borrow-arg slot is walked
+`Borrow`, not `Consume`.
+
+**Fix 2 — value-typed `let`-binder exemption (`linearity.rs`):**
+
+`Term::Let` looks the binder's type up in the `LetBinderTypes` table and
+sets `is_value` from `type_is_value` — the same per-binder flag spec
+0063 already seeds at param / pattern / `lam` sites, now extended to the
+`let` site. The walk reads the table where the source's type is
+otherwise unavailable; it never re-infers.
+
+**Fix 3 — `let`-alias borrow propagation (`linearity.rs`):**
+
+The `Checker` gains `aliases: HashMap<String, String>`. `Term::Let`
+with a bare `Term::Var` value resolving (through the alias map) to a
+tracked binder records the alias and skips the `Consume` walk of the
+value; `use_var` / the `App` borrow bump / `callee_arg_modes` resolve a
+name to its root before touching `binders`. Scoped by the existing
+save/restore discipline.
+
+**Fix 4 — class-4 corpus body rewrite (`examples/std_either_list.ail`):**
+
+`partition_eithers` is rewritten to destructure `rest` once via `(match
+rest (case (pat-ctor MkPair ls rs) …))` and reuse `ls` / `rs`, instead
+of the double `Pair.fst` / `Pair.snd` projection. No check change; the
+check correctly rejects the old shape (a genuine double-consume) and
+accepts the new one. Any other corpus fn the universal activation
+reveals to have the same genuine-consume shape is rewritten the same
+way (enumerated during the migration, not here).
+
+**Contract update (`design/contracts/0008-memory-model.md`):**
+
+The `:340` "Does not cover let-aliases of borrowed values" carve-out is
+rewritten to record that the propagation now ships (Fix 3). A contract
+change rides with the feature that forces it.
+
+## Concrete code shapes
+
+Every `ail` block below was run through `ail check`
+(`target/debug/ail`, 2026-06-01); the exit-code traces are in the
+Testing section. All are **explicit-mode** fns, so the linearity check
+is active **today** without #55 — each is RED now and GREEN after the
+named fix.
+
+### RED→GREEN class 1: local function-typed predicate param
+
+An LLM author writes the canonical `filter` HOF; the borrow-mode
+predicate `p` is applied to the heap element `h`, which is then reused
+in the kept `Cons`. False `use-after-consume` today:
+
+```ail
+(module c1_local_hof
+  (data Box
+    (doc "heap cell")
+    (ctor Box (con Int)))
+  (data List
+    (doc "boxed list of boxes")
+    (ctor Nil)
+    (ctor Cons (con Box) (con List)))
+  (fn filter_box
+    (doc "borrow-mode predicate p applied to h; h reused in the kept Cons")
+    (type
+      (fn-type
+        (params (borrow (fn-type (params (borrow (con Box))) (ret (own (con Bool)))))
+                (own (con List)))
+        (ret (own (con List)))))
+    (params p xs)
+    (body
+      (match xs
+        (case (pat-ctor Nil) (term-ctor List Nil))
+        (case (pat-ctor Cons h t)
+          (if (app p h)
+            (term-ctor List Cons h (app filter_box p t))
+            (app filter_box p t)))))))
+```
+
+### RED→GREEN class 2: `let`-alias of a borrowed param
+
+`(let a t …)` over a `borrow`-mode `t`; false `consume-while-borrowed`
+today:
+
+```ail
+(module c2_let_alias
+  (data Tree
+    (doc "boxed tree")
+    (ctor TLeaf)
+    (ctor TNode (con Int) (con Tree) (con Tree)))
+  (fn count
+    (doc "alias a := borrowed t, then match a")
+    (type (fn-type (params (borrow (con Tree))) (ret (own (con Int)))))
+    (params t)
+    (body
+      (let a t
+        (match a
+          (case (pat-ctor TLeaf) 0)
+          (case (pat-ctor TNode v l r) 1))))))
+```
+
+### RED→GREEN class 3: value-typed `let`-binder used multiple times
+
+`xnew` is a `Float` `let`-binder used in the cond and both branches;
+false `use-after-consume` (×2) today:
+
+```ail
+(module c3_value_let
+  (fn iterate
+    (doc "xnew is a Float let-binder used in cond and both branches")
+    (type (fn-type (params (own (con Float)) (own (con Float))) (ret (own (con Float)))))
+    (params x tol)
+    (body
+      (let xnew (app / x 2.0)
+        (if (app float_lt (app - xnew x) tol)
+          xnew
+          xnew)))))
+```
+
+### Must-stay-RED class 4: genuine double-consume
+
+`rest` is projected by both `fst` and `snd` (`own`-param projections) →
+genuinely consumed twice. This is a **real** `use-after-consume` and
+**stays an error** after every fix (the exemptions are type-/alias-gated,
+not blanket). The migration rewrites the body; the check is unchanged:
+
+```ail
+(module c4_double_consume
+  (data Pair
+    (doc "boxed pair of ints")
+    (ctor MkPair (con Int) (con Int)))
+  (fn fst (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p)
+    (body (match p (case (pat-ctor MkPair a b) a))))
+  (fn snd (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p)
+    (body (match p (case (pat-ctor MkPair a b) b))))
+  (fn both
+    (doc "MUST STAY RED: rest projected by fst AND snd = consumed twice")
+    (type (fn-type (params (own (con Pair))) (ret (own (con Pair)))))
+    (params rest)
+    (body (term-ctor Pair MkPair (app fst rest) (app snd rest)))))
+```
+
+### Class-4 fix: destructure once (clean today)
+
+The body rewrite — the same shape applied to the real
+`partition_eithers`. Clean today, clean after:
+
+```ail
+(module c4_rewrite
+  (data Pair
+    (doc "boxed pair of ints")
+    (ctor MkPair (con Int) (con Int)))
+  (fn both
+    (doc "rewrite: destructure rest once via match")
+    (type (fn-type (params (own (con Pair))) (ret (own (con Pair)))))
+    (params rest)
+    (body (match rest (case (pat-ctor MkPair a b) (term-ctor Pair MkPair a b))))))
+```
+
+### Secondary: implementation shapes (before → after)
+
+*Supporting detail, not the headline.*
+
+**`crates/ailang-check/src/lib.rs` — tee the let-binder type at `synth`'s `Let` arm (`:3808`):**
+
+```text
+before:
+  Term::Let { name, value, body } => {
+      let v = synth(value, env, locals, …, subst, …)?;
+      let prev = locals.insert(name.clone(), v);
+      let r = synth(body, …)?;
+      …restore prev…
+      Ok(r)
+  }
+after:
+  Term::Let { name, value, body } => {
+      let v = synth(value, env, locals, …, subst, …)?;
+      let_binder_types.insert((in_def.clone(), name.clone()), subst.apply(&v)); // tee the known type
+      let prev = locals.insert(name.clone(), v);
+      …unchanged…
+  }
+  // let_binder_types is a new &mut out-param on synth, threaded out of
+  // check_fn → check_in_workspace → check_workspace to the linearity dispatch.
+```
+
+**`crates/ailang-check/src/linearity.rs` — `BinderState`:**
+
+```text
+before: struct BinderState { consumed: bool, borrow_count: u32, is_value: bool }
+after:  struct BinderState { consumed: bool, borrow_count: u32, is_value: bool,
+                             fn_param_modes: Option<Vec<ParamMode>> }
+        // Some(modes) for a function-typed binder; None otherwise.
+```
+
+**`linearity.rs` — `callee_arg_modes` consults local binders first (`:750`):**
+
+```text
+before: only Term::Var resolving to self.globals; locals → vec![]
+after:  for a Term::Var callee, resolve through self.aliases, then:
+          1. if the binder carries fn_param_modes, return them;
+          2. else fall back to self.globals (today's path).
+```
+
+**`linearity.rs` — `Term::Let` (`:505`):**
+
+```text
+before:
+  Term::Let { name, value, body } => {
+      self.walk(value, Position::Consume);
+      self.with_binder(name, BinderState::default(), |this| { this.walk(body, pos); });
+  }
+after:
+  Term::Let { name, value, body } => {
+      // (a) bare-Var alias of a tracked binder → record alias, skip the consume walk;
+      // (b) otherwise walk value in Consume as today;
+      // seed the let-binder's is_value / fn_param_modes from LetBinderTypes
+      // (keyed (def, name)) for the body scope.
+  }
+```
+
+**`examples/std_either_list.ail` — `partition_eithers` Cons arm (`:61`):**
+
+```text
+before:
+  (case (pat-ctor Cons h t)
+    (let rest (app partition_eithers t)
+      (match h
+        (case (pat-ctor Left l)
+          (term-ctor Pair MkPair (term-ctor List Cons l (app Pair.fst rest)) (app Pair.snd rest)))
+        (case (pat-ctor Right r)
+          (term-ctor Pair MkPair (app Pair.fst rest) (term-ctor List Cons r (app Pair.snd rest)))))))
+after:
+  (case (pat-ctor Cons h t)
+    (let rest (app partition_eithers t)
+      (match rest
+        (case (pat-ctor MkPair ls rs)
+          (match h
+            (case (pat-ctor Left l)
+              (term-ctor Pair MkPair (term-ctor List Cons l ls) rs))
+            (case (pat-ctor Right r)
+              (term-ctor Pair MkPair ls (term-ctor List Cons r rs))))))))
+  // rest destructured once; ls/rs each consumed once per independent match-arm.
+```
+
+## Components
+
+- **`ailang-check::lib` (typecheck pass)** — `synth` gains the
+  `let_binder_types` out-param and one insert at the `Let` arm;
+  `check_fn` / `check_in_workspace` / `check_workspace` thread the table
+  out to the linearity dispatch (`lib.rs:1276`).
+- **`ailang-check::linearity`** — `BinderState.fn_param_modes`; the
+  `Checker` gains an immutable `let_binder_types` reference and a scoped
+  `aliases` map; `callee_arg_modes` resolves locals + aliases;
+  `Term::Let` seeds `is_value` / `fn_param_modes` from the table and
+  records bare-Var aliases.
+- **`.ail` fixtures** — the three RED→GREEN fixtures (classes 1–3), the
+  must-stay-RED double-consume, and the rewrite, under `examples/`.
+- **`examples/std_either_list.ail`** — the `partition_eithers` rewrite
+  (plus any sibling corpus fn the migration reveals with the same
+  genuine-consume shape).
+- **`design/contracts/0008-memory-model.md`** — the `:340` let-alias
+  carve-out updated to "ships".
+
+No change to: the schema (`ParamMode`, `Type::Fn`), the parser, the
+printer, codegen, the runtime, `is_heap_type`, or the
+`over-strict-mode` lint.
+
+## Data flow
+
+**The type table.** The typecheck pass already synthesises every
+`let`-binder's type (`lib.rs:3808`); today it is dropped when `check_fn`
+returns `Result<()>`. The fix records `subst.apply(&v)` — the resolved
+type — into `(def, binder) → Type` and threads it to linearity, which
+runs strictly **after** a clean typecheck (`lib.rs:1254` gate), so the
+table is fully populated before the walk starts. Linearity reads the
+table only at the `Term::Let` introduction site; params and `lam`-params
+keep reading their signature types. A binder whose teed type is not a
+value `Type::Con` and not a `Type::Fn` defaults exactly as today
+(`is_value = false`, `fn_param_modes = None`).
+
+**Mode resolution.** For `(app callee args)`, `callee_arg_modes`
+resolves the callee `Var` through the alias map, then prefers a tracked
+binder's `fn_param_modes` over the global table. A global fn-ref callee
+is untracked, so it still falls through to `self.globals` — no behaviour
+change for the common case. A local function-typed binder now resolves
+its declared arg modes, so a borrow-arg slot is walked `Borrow`.
+
+**Alias soundness.** `(let a t body)` with `t` a tracked binder makes
+`a` a redirect to `root(t)`. Every binder op on `a` (consume, borrow,
+mode lookup) acts on the single root state, so: a borrow-position use of
+`a` does not consume `t` (fixes the false positive), and a consume of
+`a` marks `t` consumed (so a later consume of either is a real
+`use-after-consume` — no false negative). Aliases are installed for the
+body scope and removed on exit, like any binder.
+
+## Error handling
+
+No new diagnostic codes. The two existing codes (`use-after-consume`,
+`consume-while-borrowed`) fire on a strictly smaller, more correct set:
+they no longer fire on local HOF-param applications (class 1),
+borrowed-value `let`-aliases (class 2), or value-typed `let`-binders
+(class 3). They continue to fire on the genuine double-consume (class
+4, must-stay-RED) and on any real use-after-consume reached through an
+alias. The change is a precision improvement to existing diagnostics,
+not a new check surface.
+
+## Testing strategy
+
+Live `ail check` traces (run 2026-06-01, `target/debug/ail`) — the
+state **today**, before the fixes:
+
+```text
+c1_local_hof.ail      : exit 1  error: [use-after-consume] filter_box: `h` ...
+c2_let_alias.ail      : exit 1  error: [consume-while-borrowed] count: `t` ...
+c3_value_let.ail      : exit 1  error: [use-after-consume] iterate: `xnew` ...  (x2)
+c4_double_consume.ail : exit 1  error: [use-after-consume] both: `rest` ...
+                                 (+ benign over-strict-mode warnings on fst/snd)
+c4_rewrite.ail        : exit 0  ok
+```
+
+- **RED→GREEN fixtures.** `c1_local_hof`, `c2_let_alias`, `c3_value_let`
+  land under `examples/`; each asserts its named diagnostic fires
+  **today** and is **clean** (exit 0) after the matching fix. These are
+  the RED side of fixes 1–3.
+- **Must-stay-RED fixture.** `c4_double_consume` asserts the genuine
+  double-consume still fires after all fixes — the exemptions are
+  type-/alias-gated, not blanket. It is the analogue of spec 0063's
+  `real_consume`.
+- **Class-4 corpus rewrite.** `examples/std_either_list.ail` checks and
+  runs clean after the `partition_eithers` rewrite; its existing
+  E2E/demo (`std_either_list_demo.ail`) output is unchanged.
+- **Alias soundness unit test.** An in-source `#[cfg(test)]` case in
+  `linearity.rs`: a `(let a t (seq …consume a… …consume t…))` over an
+  `own` `t` still produces `use-after-consume` (the redirect does not
+  mask a real double-consume).
+- **`std_list.filter` + importers.** `std_list.ail` and the seven
+  modules that import it (`kem_1_list_running_sum`, `nested_pat`,
+  `std_either_list`, `std_either_list_demo`, `std_list_demo`,
+  `std_list_more_demo`, `std_list_stress`) check clean once `filter`'s
+  signature is migrated to explicit modes (validated against the
+  migrated corpus; the analysis only activates with explicit modes).
+- **Full corpus regression.** `cargo test --workspace` stays green, and
+  the `examples/` typecheck/codegen suite is the net for "no exemption
+  silenced a real consume". Per the typed-MIR re-synth strictness
+  memory, run the whole workspace suite, not just e2e.
+- **Regression scripts.** `bench/check.py` and `bench/compile_check.py`
+  stay green (diagnostic-only change; no compile-baseline shift
+  expected).
+
+## Acceptance criteria
+
+1. A `(def, binder) → Type` table is teed from the typecheck pass and
+   threaded to linearity; `synth`'s `Let` arm records the resolved
+   binder type, and linearity reads it (no inference re-run in the
+   walk).
+2. `c1_local_hof`, `c2_let_alias`, `c3_value_let` check **clean** (exit
+   0) after their fixes; each shipped as an `examples/` fixture
+   asserting its today→post transition.
+3. `c4_double_consume` still fails with `use-after-consume` after all
+   fixes (exemptions are type-/alias-gated).
+4. `callee_arg_modes` resolves a local function-typed binder's
+   `param_modes`; a borrow-mode HOF predicate param applied to a heap
+   element does not consume it.
+5. A `let`-alias of a `borrow`-mode binder does not trip
+   `consume-while-borrowed`, and a `let`-alias of an `own` binder still
+   catches a real double-consume (alias soundness unit test).
+6. `examples/std_either_list.ail` checks and runs clean after the
+   `partition_eithers` rewrite; output unchanged.
+7. `cargo test --workspace` green; `bench/check.py` and
+   `bench/compile_check.py` green.
+8. `design/contracts/0008-memory-model.md:340` is updated to record the
+   let-alias propagation as shipped.
+9. No change to `ParamMode`, `Type::Fn`, the parser/printer, codegen,
+   the runtime, `is_heap_type`, or the `over-strict-mode` lint (grep /
+   diff clean).