diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs
index 4a4f8b5..591bb54 100644
--- a/crates/ailang-core/src/desugar.rs
+++ b/crates/ailang-core/src/desugar.rs
@@ -521,11 +521,19 @@ impl Desugarer {
 
     /// A binder name unique within the current fn: `<base>$<n>` with
     /// the lowest `n ≥ 1` free in both `scope` (in-scope effective
-    /// names) and `used` (the `$mp_` / `$lr_` synthetic space).
-    /// Records the minted name in `used` so a later mint is distinct.
-    /// Authored names cannot contain `$` (the lexer reserves it for
-    /// synthetic names), so `<base>$<n>` never collides with an
-    /// authored binder.
+    /// names) and `used` (the `$mp_` / `$lr_` synthetic space plus
+    /// prior mints). Records the minted name in `used` so a later mint
+    /// is distinct.
+    ///
+    /// `$` is the project's convention for synthetic names, but it is
+    /// NOT lexer-enforced — an authored binder may legally contain `$`.
+    /// The probe rejects a `<base>$<n>` that is already in `used` or
+    /// currently in `scope`, but it does NOT see an authored
+    /// `<base>$<n>` that is out of scope at mint time yet later binds
+    /// under the same `(def, name)` key. No fixture exercises an
+    /// authored `$` binder; closing that latent gap (enforce the
+    /// reservation, or seed `used` with every authored binder name in
+    /// the def) is tracked as a follow-up.
     fn fresh_binder(&mut self, base: &str, scope: &Scope) -> String {
         let mut n = 1u64;
         loop {
diff --git a/design/contracts/0008-memory-model.md b/design/contracts/0008-memory-model.md
index 00ded55..d969c16 100644
--- a/design/contracts/0008-memory-model.md
+++ b/design/contracts/0008-memory-model.md
@@ -268,6 +268,23 @@ metadata's role is explicit:
   the requirement that every ptr-typed slot in the active
   ctor's pattern is in `moved_slots[scrutinee]`.
 
+**Per-fn binder-name injectivity (a precondition of every gate
+above).** All three drop gates read `consume_count` from the
+uniqueness side-table keyed by `(def_name, binder_name)`. Codegen
+looks up by the binder's source name and must resolve the binding it
+means — so within one `def_name`, every `binder_name` must denote
+exactly one binding. The desugar pass guarantees this: it
+alpha-renames any binder whose name shadows an enclosing binding to a
+fresh `<name>$<n>` (`ailang-core::desugar`), so a shadow-rebind idiom
+like `(let buf (new…) (let buf (set buf…) … (get buf)))` becomes
+`buf, buf$1, buf$2, buf$3`. Without this, shadowed binders collapse
+onto one key and a gate reads a sibling binding's `consume_count`,
+suppressing or doubling a drop. Ratified by
+`raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats` and
+`flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed` in
+`crates/ail/tests/e2e.rs`, and the desugar unit test
+`shadowing_let_is_alpha_renamed`.
+
 **`ret_mode` — let-binder trackability.**
 
 - **`Term::App` drop at let-scope close.** A
diff --git a/design/models/0003-pipeline.md b/design/models/0003-pipeline.md
index d4c3b3b..5e0c029 100644
--- a/design/models/0003-pipeline.md
+++ b/design/models/0003-pipeline.md
@@ -30,10 +30,12 @@ structurally cheapest allocator — it is not a production target.
 The **desugar** pass
 ([`ailang-core::desugar::desugar_module`](../../crates/ailang-core/src/desugar.rs))
 runs before typecheck and codegen in every entry point of
-`ailang-check` and `ailang-codegen`. It is a pure AST → AST rewriter — currently
-only flattens nested constructor patterns, but is the chosen
-home for any future surface-smoothing rewrites that should not bloat
-the core AST or the backends. **Critical invariant:** `CheckedModule.symbols`
+`ailang-check` and `ailang-codegen`. It is a pure AST → AST rewriter —
+it flattens nested constructor patterns and alpha-renames any binder
+whose name shadows an enclosing binding to a fresh `<name>$<n>` (so the
+uniqueness side-table's `(def_name, binder_name)` key is injective per
+fn), and is the chosen home for any future surface-smoothing rewrites
+that should not bloat the core AST or the backends. **Critical invariant:** `CheckedModule.symbols`
 in the `check` entry point continues to hash from the *original*
 on-disk module, not the desugared one, so `ail diff` and `ail manifest`
 report identities that match the canonical JSON the user is editing.