audit: raw-buf close-fixes — honesty + ledger for the binder-rename (refs #43)

Architect drift review at raw-buf milestone close (after 55d76ae closed
#43) surfaced three items; this commit clears them. All three lockstep-
invariant pairs were confirmed intact and the effective-name keying was
confirmed consistent across the desugar→lift boundary (lift_letrecs reads
the desugared tree's effective names too).

1. [high] Honesty fix. `fresh_binder`'s doc-comment (and 55d76ae's body)
   claimed "authored names cannot contain `$` — the lexer reserves it".
   False: the lexer (ailang-surface) reserves only `.`, not `$`. The
   `$`-for-synthetic convention is not enforced. So collision-freedom
   rests solely on the `used` + in-scope-`scope` probe, which does not
   see an authored `<base>$<n>` that is out of scope at mint time but
   later binds under the same `(def, name)` key — the very collision
   class this fix closes. Latent (no fixture uses a `$` binder), but the
   stated rationale was wrong. Doc-comment now describes the probe
   honestly and names the gap + its two possible closures (enforce the
   reservation, or seed `used` with every authored binder name in the
   def). The enforce-or-retract decision is the next-direction follow-up.

2. [medium] design/models/0003-pipeline.md — "desugar currently only
   flattens nested constructor patterns" no longer matches the code
   (it now also alpha-renames shadowing binders). Corrected to current
   state (honesty-rule).

3. [low] design/contracts/0008-memory-model.md — the three drop gates
   all key on `(def_name, binder_name)` consume_count, silently relying
   on per-fn binder-name injectivity, which the ledger never stated.
   Added that invariant as an explicit precondition of the gates, with
   the desugar guarantee and its ratifying tests.

No code-logic change; doc-comment + ledger only.

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 {