audit: spec 0064 cycle close — drift-clean after two ledger fixes (#57)

Cycle-close audit for spec 0064 (the #57 hardening of the linearity
analysis, the #55-cutover precondition; four iterations 47964ab,
cc5991e, be259f9, 2769e50).

Architect drift review (39b674c..HEAD): both CLAUDE.md lockstep pairs
confirmed untouched (INTERCEPTS↔intrinsic markers; Pattern::Lit
typecheck↔pre_desugar_validation) — the cycle is genuinely
diagnostic-only. It found two drift items, both in the iter-3 contract
edit, both fixed here (fix path, folded into the audit close since they
are doc-only):

1. [medium] design/contracts/0008-memory-model.md — the iter-3 rewrite
   placed a "Covers let-aliases…" statement under the "What this
   widening does NOT do" heading (incoherent) and named only the
   linearity-check mechanism, silently dropping the codegen dimension
   the original carve-out actually referred to ("Iter A / pre-tail-call
   shallow-dec arm" = the drop gates). Verified the real current state:
   let-aliases are propagated on BOTH axes — the linearity diagnostic
   (Checker.aliases + resolve_alias, this cycle) AND the codegen drop
   gates (MTerm::Let's current_param_modes mode inheritance,
   ailang-codegen/src/lib.rs:1811, pre-existing). The bullet is moved
   out of the "does NOT do" list into a positive paragraph naming both
   mechanisms.
2. [low] design/INDEX.md memory-model row — the ratifying-test cell
   listed only uniqueness.rs while the contract trailer now also names
   linearity.rs. Cell updated to "uniqueness.rs + linearity.rs".

Regression gate (both green, exit 0):
- bench/check.py: 34 metrics; 0 regressed, 1 improved beyond tolerance
  (latency.implicit_at_rc.median_us -5.27%), 33 stable. The "improved"
  is measurement noise, NOT a real metric move — this cycle is
  diagnostic-only and touches no codegen/runtime, so it cannot have
  improved runtime latency. Baseline deliberately NOT updated (no
  ratify: nothing in the code moved the metric).
- bench/compile_check.py: 24 metrics; 0 regressed, 24 stable.

Outcome: cycle 0064 tidy (drift-clean). All four #57 hardening classes
(value-typed let-binders, local fn-param modes, let-alias propagation,
partition_eithers double-consume) shipped and ratified. The #55-cutover
precondition is met. Drift-clean is not a milestone close: #55 (the
irreversible ParamMode::Implicit deletion) is the next, separate step.

refs #57

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 //! |

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-aliases of borrowed values are propagated** (no longer a
-  let-binder whose value is a bare `Term::Var` resolving to a
+carve-out). A let-binder whose value is a bare `Term::Var`
-  tracked binder is recorded as an alias to that root in the
+resolving to a tracked binder is treated as an alias of that
-  linearity walk (`crates/ailang-check/src/linearity.rs`,
+source on both axes of the ownership analysis:
-  `Checker.aliases` + `resolve_alias`); the binding does not
+
-  consume the source, and every binder-state lookup resolves
+- the linearity diagnostic (spec 0064, class 2) records `a →
-  the alias to its root, so a borrow-position use of the alias
+  root` in the walk (`crates/ailang-check/src/linearity.rs`,
-  does not consume the root while a real double-consume through
+  `Checker.aliases` + `resolve_alias`) and resolves every
-  the alias is still caught.
+  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`.