diff --git a/docs/specs/0055-intrinsic-bodies.md b/docs/specs/0055-intrinsic-bodies.md
index e20aa96..3f6b858 100644
--- a/docs/specs/0055-intrinsic-bodies.md
+++ b/docs/specs/0055-intrinsic-bodies.md
@@ -106,21 +106,58 @@ Three landing points, two iterations.
 
 **Iteration `intrinsic-bodies.2` — the migration + the lock.**
 
-6. **Prelude migration.** All eighteen dummy bodies (the `eq__*`,
-   `compare__*`, and `lt|le|gt|ge|ne__*` instance methods enumerated
-   by `intercepts::INTERCEPTS`) swap their `(body <dummy>)` for
-   `(intrinsic)`.
-7. **Hard-lockstep pin.** A test asserts a **bijection** between
-   `INTERCEPTS` entries and `(intrinsic)` definitions reachable in
-   the loaded workspace (prelude + kernel-tier modules): every
-   registry entry has exactly one intrinsic marker and vice versa.
-   Drift in either direction is a red test. This extends the
+6. **Prelude migration.** The **thirteen authored dummy bodies** in
+   `examples/prelude.ail` swap their inner `(body <dummy>)` for
+   `(intrinsic)`: the seven Eq/Ord instance methods (`eq` for
+   Int/Bool/Str/Unit, `compare` for Int/Bool/Str) and the six `float_*`
+   free fns (`float_eq/ne/lt/le/gt/ge`). These are exactly the
+   `INTERCEPTS` entries that today carry a placeholder body a reader
+   would mistake for the implementation.
+
+   **Not migrated, and why** (the count reconciliation — the registry
+   has nineteen entries, not eighteen-all-dummies):
+   - `lt__Int`, `le__Int`, `gt__Int`, `ge__Int`, `ne__Int` (5) intercept
+     the *monomorphised* `__Int` specialisations of the polymorphic free
+     fns `lt/le/gt/ge/ne`, which carry **real bodies** in the prelude
+     (`(match (app compare x y) …)`, `(app not (app eq x y))`). Those
+     bodies are honest and live — they are lowered for every non-`Int`
+     instantiation; only the `Int` specialisation is intercepted for a
+     faster direct `icmp`. These are an **optimisation class**, not a
+     compiler-supplied-body class: there is no lie to fix and no source
+     body to replace, so they get **no** `(intrinsic)` marker.
+   - `answer` (1) is the `.1` ratifier, already `(intrinsic)` in
+     `STUB_AIL` — not a prelude site.
+
+   So: 13 prelude migrations + 5 optimisation-class entries + 1 already
+   migrated = 19 `INTERCEPTS` entries.
+7. **Hard-lockstep pin.** The registry splits into two classes: an
+   entry is **intrinsic-backed** when a `(intrinsic)` marker in the
+   loaded workspace resolves to its mangled name (the 13 prelude
+   migrations + `answer` = 14), or **optimisation-only** when it
+   intercepts a real-bodied fn's specialisation (the 5 `*__Int` icmp
+   family). The pin asserts a **bijection over the intrinsic-backed
+   class**: every workspace `(intrinsic)` marker has exactly one
+   `INTERCEPTS` entry, and every `INTERCEPTS` entry *not* on the
+   explicit optimisation-only allowlist has exactly one workspace
+   marker. The optimisation-only set is an explicit, documented
+   allowlist in the pin (the 5 names); adding a registry entry that is
+   neither marker-backed nor allowlisted is a red test, as is an
+   intrinsic marker with no entry. This extends the
    `registry_contains_all_legacy_arms` pin from raw-buf.1 from a
    one-directional name check to a two-directional source↔registry
    bijection.
-8. **Dead-path removal.** The dummy-body-execution path for
-   intercepted definitions is removed; nothing emits it once the
-   migration lands.
+8. **Dead-path confirmation.** `.1` already routes every intercepted
+   def by name (`try_emit_primitive_instance_body` consults
+   `intercepts::lookup` on the fn name *before* the body is inspected),
+   so a prelude dummy body is bypassed before it could reach
+   `lower_term` — the dummy is already dead, not lowered-then-discarded.
+   After migration the dummy is gone entirely (replaced by
+   `Term::Intrinsic`). This point is therefore a **verification, not a
+   removal**: confirm no codegen path lowers an intercepted body, and
+   delete now-stale comments that reference the discarded dummy. The
+   `Term::Intrinsic` internal-error guards in `lower_term` / the synth
+   walker (added in `.1`) STAY — they guard against an intrinsic body
+   escaping its definition slot, which is a different concern.
 
 ## Concrete code shapes
 
@@ -272,11 +309,13 @@ all move in the same iteration as the variant.
 | `crates/ailang-check/src/mono.rs` | .1 | `synthesise_mono_fn` lambda-destructure unchanged; an inner `Term::Intrinsic` body flows through to an intrinsic synthesised `FnDef`. |
 | `crates/ailang-codegen/src/lib.rs` | .1 | A def whose body is `Term::Intrinsic` routes through `intercepts::lookup`; `lower_term` is never called on it. |
 | `crates/ailang-kernel-stub` + `ailang-surface` parse hop | .1 | `answer` smoke intrinsic added to the stub fixture; its intercept registered. |
-| `examples/prelude.ail` | .2 | 18 dummy bodies → `(intrinsic)`. |
-| `crates/ailang-codegen/src/intercepts.rs` (pin) | .2 | `registry_contains_all_legacy_arms` upgraded to a source↔registry bijection pin. |
-| codegen dummy-body path | .2 | Removed. |
+| `examples/prelude.ail` | .2 | 13 authored dummy bodies → `(intrinsic)` (7 Eq/Ord instance methods + 6 `float_*` fns). The 5 `*__Int` icmp-family and `answer` are NOT prelude sites. |
+| `crates/ailang-codegen/src/intercepts.rs` (pin) | .2 | `registry_contains_all_legacy_arms` upgraded to a bijection over the intrinsic-backed class + an explicit 5-name optimisation-only allowlist. Pin loads the workspace + monomorphises to recover mangled names for the marker direction. |
+| `crates/ailang-surface/tests/prelude_module_hash_pin.rs` | .2 | Rebaseline the prelude module hash (13 bodies change). |
+| `crates/ail/tests/mono_hash_stability.rs` | .2 | Rebaseline the 6 post-mono `eq__*`/`compare__*` def-hashes (body flips to `Term::Intrinsic`). The 4 `show__*` pins do NOT move. |
+| codegen dummy-body path | .2 | Already dead post-`.1` (intercept-by-name precedes body inspection); `.2` confirms + deletes stale comments, no behavioural removal. |
 | `design/contracts/0002-data-model.md` | .1 | New `{ "t": "intrinsic" }` Term entry; note in `fn`/`lam` that the body may be `Term::Intrinsic`. |
-| `design/contracts/0007-honesty-rule.md` | .2 | The prelude-dummy infraction is closed; note its resolution if the contract references it. |
+| `design/contracts/0007-honesty-rule.md` | .2 | Edit only if it names the prelude dummies; recon found it is a general rule that may not reference them — flag honestly, no forced edit. |
 
 ## Data flow
 
@@ -328,16 +367,27 @@ unrepresentable, not diagnosed.)
 
 **intrinsic-bodies.2:**
 
-- Hard-lockstep pin: bijection between `INTERCEPTS` and workspace
-  intrinsic markers. Add a marker without an entry → red; add an
-  entry without a marker → red; drop either → red.
+- Hard-lockstep pin: bijection over the intrinsic-backed class. Add an
+  intrinsic marker with no `INTERCEPTS` entry → red; add a
+  non-allowlisted `INTERCEPTS` entry with no marker → red; drop either
+  → red. The 5-name optimisation-only allowlist is explicit in the pin;
+  the pin loads the workspace, monomorphises, and walks post-mono
+  `FnDef` bodies for `Term::Intrinsic` to recover mangled names for the
+  marker direction.
 - All pre-existing E2E ratifiers stay green (the eq/compare/float
-  smoke suite named in raw-buf.1's commit body) — the migration is
-  behaviour-preserving by construction.
-- Prelude hash: the prelude module's hash *changes* in .2 (the dummy
-  bodies are gone); the `prelude_module_hash_pin.rs` baseline is
-  rebaselined in the same iteration, with the old→new hash recorded
-  in the commit body.
+  smoke suite named in raw-buf.1's commit body:
+  `eq_primitives_smoke_compiles_and_runs`,
+  `compare_primitives_smoke_prints_1_2_3_thrice`,
+  `float_compare_smoke_prints_true_true_false`,
+  `eq_ord_polymorphic_runs_end_to_end`) — the migration is
+  behaviour-preserving (the intercepts emit the same IR; only the
+  now-dead source body changes).
+- Hash rebaselines (both move; both recorded old→new in the commit
+  body): `prelude_module_hash_pin.rs` (prelude module hash; 13 bodies
+  change) and `mono_hash_stability.rs` (the 6 post-mono
+  `eq__*`/`compare__*` def-hashes flip to `Term::Intrinsic`; the 4
+  `show__*` pins do NOT move). IR snapshots do NOT change (no prelude
+  instance method is codegen'd into the user-program snapshots).
 
 ## Acceptance criteria