diff --git a/docs/SPIKE-DYNAMIC.md b/docs/SPIKE-DYNAMIC.md
index 52d4eef..f00d960 100644
--- a/docs/SPIKE-DYNAMIC.md
+++ b/docs/SPIKE-DYNAMIC.md
@@ -353,13 +353,39 @@ That is the asymmetry worth defending, because the operators *do* promote (§5).
 questions. An operator has no stated expectation to violate — `(+ 1 2.5)` was written by somebody who
 wanted a number and there is one obvious number. An annotation *is* a stated expectation, written down by
 a person, and quietly turning their `i64` into an `f64` would make the boundary the one place in the
-language where a type changed without anybody writing it. Typed Flan has no implicit widening; the
-boundary into typed Flan should not invent some.
+language where a *value* changed type without anybody writing it. Typed Flan does not widen a value:
 
-The consequence for the compiler lane: a call from dyn code into `(defn f [x f64] ...)` with an integer
-argument traps at run time rather than converting. If that turns out to be too sharp in practice, the
-place to soften it is the *compiler*, by emitting a conversion where the checker can see both sides — not
-here, where the only thing visible is a tag.
+```lisp
+(defn g [x f64] f64 x)
+(defn h [y i64] f64 (g y))   ; scratch.flan:2:24: expected f64, found i64
+```
+
+### The one divergence the compiler lane has to know about
+
+Typed Flan does not widen a *value*, but a **literal adopts its expected type**. `(g 1)` compiles and
+prints `1`, because the checker gives the literal `1` the `f64` the parameter asks for; `(vec-new i64)`
+followed by `(push v 1)` works the same way.
+
+A dyn value has no such history. Once `1` has been through `flan_dyn_from_i64` it is tagged `int`, and
+nothing downstream can recover that it was written as a literal in a position that wanted a float. So:
+
+```lisp
+(g 1)          ; typed: compiles, prints 1
+(g some-dyn)   ; dyn, where some-dyn came from the literal 1: traps, "a float was wanted"
+```
+
+That is a real divergence between the same source read as typed and read as dyn, and it is stated here
+rather than discovered later. Two ways out, both the compiler's and neither this file's:
+
+1. **Tag the literal at the constructor.** Where the checker can see that an unannotated literal flows to
+   a float context, emit `flan_dyn_from_f64` instead of `flan_dyn_from_i64`. This is the same inference
+   the checker already performs for typed literals and it keeps the boundary sharp.
+2. **Emit a conversion at the call**, where both sides are visible, rather than softening
+   `flan_dyn_need_f64` — which sees only a tag and could not tell a literal-derived int from a computed
+   one.
+
+Softening the boundary itself is the option not to take: it would accept `(g (len xs))` as readily as
+`(g 1)`, and those are not the same mistake.
 
 ---
 
@@ -406,16 +432,21 @@ is a property of the build and not a wish:
   back-reference — `flan_rt_init` calling `flan_gc_init`, say, which was the obvious thing to write —
   would make the collector unconditional and the refusal a lie, so the heap initialises itself lazily on
   first allocation instead.
-- Consequently a program that calls no dyn operation pulls nothing out of that object, and the linker
-  leaves it behind.
+**The linker does not drop it today, and this document will not claim it does.** `flan_dyn.o` is a named
+object on the link line, not an archive member, and `ld` includes a named object in full — symbol-driven
+selection is a `.a` rule. Dead-code elimination *inside* an included object needs
+`-ffunction-sections -fdata-sections -Wl,--gc-sections`, which the link line does not pass. Measured
+rather than assumed: build any corpus program and `nm` it, and `flan_dyn_add` and `flan_gc_collect` are
+both there as defined symbols.
 
-The link line does **not** currently pass `-ffunction-sections`/`-Wl,--gc-sections`, and this document
-will not claim a drop the build cannot perform. What the above buys is the cheaper mechanism: the object
-is selected at the *file* level, so `--no-gc` is a one-line change at each of the three sites — the same
-per-target selection `select_csrcs` already performs for a package's C — rather than an argument with the
-linker about which sections are live. `flan_dev.c` is compiled into every build today for a reason its
-comment gives at length (a package's C refers to it and package sources are collected whatever `main`
-does); `flan_dyn.c` has no such entanglement and can genuinely be left out.
+What the one-way dependency buys is the better mechanism anyway. The object is selected at the **file**
+level: `--no-gc` is a one-line change at each of the three sites that name `Runtime_src.dyn_source` — the
+same per-target selection `select_csrcs` already performs for a package's C — and once it is not
+compiled, nothing has to be dropped. That only works because nothing else in the runtime refers to it;
+`flan_dev.c` is compiled into every build today precisely because it *is* referred to (a package's C
+names it, and package sources are collected whatever `main` does), and its own comment says so at length.
+`flan_dyn.c` has no such entanglement, and keeping it that way is the constraint this section exists to
+record.
 
 The residual-dynamism refusal itself — deciding that a program is *not* fully annotated and saying which
 form is not — is the compiler's, and is not attempted here.
diff --git a/lib/build.ml b/lib/build.ml
index 738b7e8..11b9593 100644
--- a/lib/build.ml
+++ b/lib/build.ml
@@ -864,14 +864,19 @@ let executable ?(opts = default) ?(csrcs = []) ?(lflags = []) ?(pnames = [])
   let objs =
     cc ~warn:runtime_warnings Runtime_src.source "flan_rt.c"
     :: [ cc ~warn:runtime_warnings Runtime_src.dev_source "flan_dev.c";
-         (* The dynamic-value runtime. Compiled into every build for the
-            reason flan_dev.c is, and dropped by the same means: it is its own
-            translation unit and nothing in the other two names a symbol in
-            it, so a program with no dyn operation in it pulls nothing out of
-            this object and the linker leaves it behind. Selecting it away at
-            the file level — which is what `--no-gc` will do once the compiler
-            lane can prove a program is fully annotated — is then a one-line
-            change here rather than an argument with the linker. *)
+         (* The dynamic-value runtime. Compiled into every build today, as
+            flan_dev.c is, but for a weaker reason: nothing refers to it. It is
+            its own translation unit and no line of flan_rt.c or flan_dev.c
+            names a symbol in it, so leaving it out is a change *here* and
+            nowhere else — which is what `--no-gc` will be, once the compiler
+            lane can prove a program is fully annotated.
+
+            The linker is not the mechanism and would not be: a named object is
+            linked whole, and dropping unreached code inside one needs
+            -ffunction-sections and --gc-sections, which this line does not
+            pass. So the selection is at the file level, the same shape
+            [select_csrcs] applies to a package's C. See docs/SPIKE-DYNAMIC.md,
+            "Dropping the collector". *)
          cc ~warn:runtime_warnings Runtime_src.dyn_source "flan_dyn.c" ]
     (* wasi-libc's entry point, which is not [main]. See [wasm_main_source].
        Not the browser's: emscripten's start code calls [main] under that name,
diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c
index debba8c..a3001a9 100644
--- a/runtime/flan_dyn.c
+++ b/runtime/flan_dyn.c
@@ -15,12 +15,13 @@
  *
  * flan_rt.c, and nothing else in the tree. The dependency does not run the
  * other way: no line of flan_rt.c or flan_dev.c names anything defined here.
- * That is the whole of what makes a `--no-gc` build possible — a program that
- * calls no dyn operation references no symbol in this translation unit, so the
- * object contributes nothing but its own size, and the compiler lane is free
- * to refuse to link it at all. A single back-reference from the release
- * runtime would make the collector unconditional and the refusal a lie. See
- * the doc's "Dropping the collector".
+ * That is the whole of what makes a `--no-gc` build possible — not because the
+ * linker drops this object (it does not; a named object is linked whole, and
+ * `nm` on any corpus program finds flan_dyn_add in it), but because nothing
+ * else needs it, so *not compiling it* is a change at the three sites that
+ * name it and nowhere else. A single back-reference from the release runtime
+ * would make the collector unconditional and the refusal a lie. See the doc's
+ * "Dropping the collector".
  *
  * ── Threads ───────────────────────────────────────────────────────────
  *
@@ -780,12 +781,23 @@ int64_t flan_dyn_need_i64(flan_dyn v) {
  * an omission: typed Flan has no implicit widening anywhere — [(print-i64 x)]
  * used to force an explicit [(i64 x)] at every site — and a boundary that
  * quietly turned an int into a float would be the one place in the language
- * where a type changed without anybody writing it down. The dyn *operators*
- * promote, because arithmetic between a 2 and a 2.5 has an obvious answer and
- * refusing it makes dynamic code worse; the boundary into a typed f64
- * parameter does not, because there the annotation is somebody's stated
- * expectation and a mismatch is worth hearing about. That asymmetry is
- * deliberate and is argued at length in the doc. */
+ * where a *value* changed type without anybody writing it down. The dyn
+ * *operators* promote, because arithmetic between a 2 and a 2.5 has an obvious
+ * answer and refusing it makes dynamic code worse; the boundary into a typed
+ * f64 parameter does not, because there the annotation is somebody's stated
+ * expectation and a mismatch is worth hearing about.
+ *
+ * Where this is sharper than the typed language is a *literal*. `(g 1)`
+ * against `(defn g [x f64] ...)` compiles, because the checker gives the
+ * literal the type the parameter asks for; a dyn value written as `1` has
+ * already been through flan_dyn_from_i64 and cannot remember that it was a
+ * literal. So the same source read as dyn traps where read as typed it does
+ * not. That is a real divergence, it is the compiler's to close — by tagging
+ * such a literal as a float where it can see the context — and it is written
+ * down in the doc's boundary section so that closing it is a decision somebody
+ * makes rather than a surprise somebody meets. Softening the check here is the
+ * option not to take: this function sees a tag and nothing else, so it could
+ * not tell (g 1) from (g (len xs)). */
 double flan_dyn_need_f64(flan_dyn v) {
   if (flan_dyn_tag(v) != FLAN_DYN_TAG_FLOAT)
     trap1(TYPE_TRAP, "f64", "a float was wanted", v);