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.
Brummel
b151990028