diff --git a/design/contracts/0003-embedding-abi.md b/design/contracts/0003-embedding-abi.md
index e3cc8cf..acff481 100644
--- a/design/contracts/0003-embedding-abi.md
+++ b/design/contracts/0003-embedding-abi.md
@@ -38,7 +38,7 @@ thread (`Ctx: !Send`) and each `ailang_ctx_t` is
 single-thread-per-ctx. The one datum a multi-threaded host shares
 is the global RC-stats fallback counter (used when no ctx is
 bound); it is atomic-relaxed so the swarm's leak accounting is
-exact. The swarm artefact is data-race-free, sanitiser-verified.
+exact. The swarm artefact is data-race-free by this split.
 The staticlib swarm artefact is **RC-only**:
 `ail build --emit=staticlib` rejects `--alloc=bump` (the bench
 stub is leak-only and not swarm-safe; `--alloc=gc` no longer
diff --git a/design/contracts/0008-memory-model.md b/design/contracts/0008-memory-model.md
index d475bff..6d78f30 100644
--- a/design/contracts/0008-memory-model.md
+++ b/design/contracts/0008-memory-model.md
@@ -162,15 +162,12 @@ Skipped from serialisation when empty so existing fixtures keep
 bit-identical canonical-JSON hashes (regression-pinned by
 `iter19b_empty_suppress_preserves_pre_19b_hashes` and
 `iter19b_schema_extension_preserves_pre_19b_hashes`).
-The canonical-form tightening for `Type::Con.name` shifted the
-hashes of two cross-module fixtures (`ordering_match.ail.json` and
-`test_22b1_dup_a.ail.json`); all intra-module fixtures, including
-the regression-pinned `sum.ail.json` and `list.ail.json`, remain
-bit-identical. The new pins are
-`ct4_migrated_fixtures_have_canonical_form_hashes` (locks the
-post-migration hashes) and
-`ct4_unmigrated_fixtures_remain_bit_identical` (re-asserts the
-pre-tightening hashes still hold).
+Two cross-module fixtures (`ordering_match.ail.json` and
+`test_22b1_dup_a.ail.json`) carry canonical-form `Type::Con.name`
+hashes, pinned by `ct4_migrated_fixtures_have_canonical_form_hashes`;
+all intra-module fixtures, including `sum.ail.json` and
+`list.ail.json`, are pinned bit-identical by
+`ct4_unmigrated_fixtures_remain_bit_identical`.
 
 ## Advisory diagnostics
 
diff --git a/design/contracts/0013-typeclasses.md b/design/contracts/0013-typeclasses.md
index cbb8450..876e5ff 100644
--- a/design/contracts/0013-typeclasses.md
+++ b/design/contracts/0013-typeclasses.md
@@ -115,10 +115,7 @@ Three invariants make this work:
    the callee against the workspace and emits
    `Callee::Static { module, fn_name, .. }` carrying the resolved owner.
    Codegen consumes that identity off the MIR `App` node and does
-   **not** re-resolve it — the former codegen-side
-   `import_map`-then-`module_user_fns` fallback (at `resolve_top_level_fn`,
-   `lower_app`'s cross-module arm, and the now-deleted
-   `synth_with_extras`) is retracted, per the
+   **not** re-resolve it, per the
    [check→codegen boundary](0018-check-codegen-boundary.md). Both ends
    were independently typechecked under their own module contexts before
    mono ran; the cross-module reference is a post-mono construct, not a
@@ -163,9 +160,8 @@ cross-module reference, invariant (2) makes codegen able to resolve
 post-mono references, invariant (3) makes the typecheck-time
 discharge fire correctly when no instance exists, invariant (4)
 makes bare prelude-fn names resolve from user modules at the source
-level. A future refactor that loosens any one of the four breaks
-the user-ADT trajectory or the Float-named-fn surface; the test
-pins at
+level. Loosening any one breaks the user-ADT trajectory or the
+Float-named-fn surface, so each is pinned:
 `crates/ail/tests/codegen_import_map_fallback_pin.rs` (invariant 2),
 `crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` (invariant 3
 + lockstep), `crates/ail/tests/float_compare_smoke_e2e.rs`
diff --git a/design/contracts/0017-prelude-classes.md b/design/contracts/0017-prelude-classes.md
index 2182c00..ad803f6 100644
--- a/design/contracts/0017-prelude-classes.md
+++ b/design/contracts/0017-prelude-classes.md
@@ -25,15 +25,13 @@ codegen intercept short-circuits this indirection: `lt__Int`,
 overridden to emit `icmp slt i64` / `sle i64` / `sgt i64` /
 `sge i64` / `ne i64` directly, bypassing the `compare__Int` →
 `Ordering`-ctor → `match` path. Without this short-circuit the
-`Ordering` ctor allocates per call inside hot loops — a real
-cost surfaced by the `bench_closure_chain` regression at the
-operator-routing-eq-ord milestone and pinned by
-`crates/ail/tests/ord_int_intercept_ir_pin.rs`. The short-circuit
+`Ordering` ctor allocates per call inside hot loops; the
+short-circuit is pinned by
+`crates/ail/tests/ord_int_intercept_ir_pin.rs`. It
 is *Int-only* by deliberate asymmetry: no current bench or
 example fixture exercises Ord-`lt`/`le`/`gt`/`ge` at Bool or
 Str at sufficient call frequency to justify the intercept-arm
-maintenance; the symmetric extensions are mechanical when the
-first such workload appears.
+maintenance.
 
 Float has neither `Eq` nor `Ord` instance per [Float semantics](
 0005-float-semantics.md); a polymorphic helper invoked at Float fires