diff --git a/docs/specs/2026-05-11-23-eq-ord-prelude.md b/docs/specs/2026-05-11-23-eq-ord-prelude.md
new file mode 100644
index 0000000..737c356
--- /dev/null
+++ b/docs/specs/2026-05-11-23-eq-ord-prelude.md
@@ -0,0 +1,421 @@
+# 23 — Eq / Ord Prelude — Design Spec (revised)
+
+**Date:** 2026-05-11
+**Status:** Draft — awaiting user spec review
+**Authors:** Brummel (orchestrator) + Claude
+
+**Supersedes:** `docs/specs/2026-05-10-23-eq-ord-prelude.md` (retired
+2026-05-11 in iter gc.1; commit `f6d4ba3`). Iter 23.1–23.3 shipped
+under the original spec and remain in effect; this revised spec
+re-frames the remaining work on a corrected architecture.
+
+## Goal
+
+Complete milestone 23 by shipping the five free top-level utility
+functions `ne`, `lt`, `le`, `gt`, `ge` in the auto-loaded prelude,
+plus the E2E and DESIGN.md amendments that close the Eq/Ord
+surface. Establish the partial-Eq/Ord story for `Float` as a lived
+reality: `Float` has neither instance, so polymorphic `eq x y` /
+`compare x y` over a Float fires `NoInstance` at typecheck — exactly
+what DESIGN.md §"Float semantics" prescribes.
+
+The re-brainstorm exists because the original spec's architecture
+section silently assumed that polymorphic free fns with class
+constraints would be mono-specialised the same way class methods
+are. They are not — the typecheck-time mono pass
+(`crates/ailang-check/src/mono.rs`, iter 22b.3) operates only on
+class methods, while polymorphic free fns are specialised at codegen
+time by `crates/ailang-codegen/src/lib.rs::lower_polymorphic_call`
+(iter 12b). A polymorphic free fn whose body invokes class methods
+falls between the two passes. Iter 23.4 BLOCKED three times on this
+seam.
+
+The corrected architecture unifies the two specialisers (see
+Architecture below) and ships the remaining free fns on top of
+the unified pass. The three iter-23.4 prep commits are classified:
+prep1 (linearity + checker bare-name) stays load-bearing, prep2 +
+prep3 (codegen bare-name fall-throughs) become provably dead and
+are rolled back in 23.4.
+
+`Show`, operator routing, `print`-rewire, and the heap-Str ABI
+remain out of scope; each is its own milestone with substantive
+reasons (see "Out of scope" — unchanged from original spec).
+
+## Architecture
+
+The milestone no longer consumes the 22b.3 typeclass machinery
+unchanged. Four artefacts:
+
+### 1. Mono-Pass unification (the corrected centrepiece)
+
+`crates/ailang-check/src/mono.rs::monomorphise_workspace` is
+restructured into a single specialiser for every
+`Type::Forall`-quantified `Def::Fn` whose call sites supply
+fully-concrete substitutions. Two thin source-body entry points:
+
+- **Class-method entry:** look up the resolved instance body via
+  `Registry::entries[(class, type-hash)]`. Unchanged behaviour from
+  iter 22b.3.
+- **Free-fn entry:** take the source body directly from the
+  polymorphic `Def::Fn`, apply rigid-var substitution.
+
+Shared core mechanics — identical for both arms — are: rigid-var
+substitution via `crate::substitute_rigids`, fixpoint loop (`mono.rs`
+line 88) that keeps collecting targets until a round adds nothing
+new, dedup cache keyed by `(name, type-hash)`, and the
+call-site-rewrite walker.
+
+Output: synthesised `Def::Fn` entries with naming
+`<name>__<typesurfacename>` (extended to
+`<name>__<type1>__<type2>__…` for N-ary type vars in declaration
+order; concrete format is an Open commitment), appended to the
+defining module. The mono pass becomes the only specialiser; codegen
+sees no class machinery and no polymorphic call sites.
+
+The current codegen-time specialiser is retired in the same iter:
+`crates/ailang-codegen/src/lib.rs::lower_polymorphic_call`,
+`module_polymorphic_fns` (the per-module FnDef map), and `mono_queue`
+(the deduplicated emission queue) are removed. All today's call
+sites of `lower_polymorphic_call` (lines 1944, 1972) become direct
+calls to mono symbols after the typecheck-mono walker has rewritten
+them.
+
+### 2. Rollback of iter-23.4-prep2 + prep3
+
+Two existing codegen bare-name fall-throughs were anticipatory
+patches for the prelude free fns:
+
+- commit `a06159d` (prep2): codegen — bare-name fall-through to
+  implicit-imported free fns.
+- commit `c42a0f5` (prep3): codegen — polymorphic-free-fn bare-name
+  fall-through to implicit-imported modules.
+
+After Mono unification, codegen never sees bare polymorphic free-fn
+names — the unified mono pass rewrites every call site to its mono
+symbol before codegen runs. The two patches are provably dead and
+are rolled back in 23.4. The rollback lands in the same iter as
+the unification so the codebase never carries the fall-throughs
+as visible-but-dead code.
+
+The third iter-23.4-prep is kept:
+
+- commit `8d39f13` (prep.1): linearity — register `Def::Class` method
+  types in globals. Required independent of mono — linearity walks
+  pre-mono.
+- commit `aef4ab8` (prep.2): check — bare-name fall-through to
+  implicit-imported free fns. Required at typecheck time — bare `ne`
+  must resolve to the prelude `Def::Fn` *before* mono can specialise.
+
+### 3. Prelude AILang module
+
+`examples/prelude.ail.json` already contains, from iters 23.1–23.3:
+the `Ordering` ADT, the `Eq` class with `Eq Int`/`Bool`/`Str`
+instances, the `Ord` class with `Ord Int`/`Bool`/`Str` instances.
+Iter 23.5 adds the five free fns:
+
+- `ne : forall a. Eq a => (a borrow, a borrow) -> Bool`, body
+  `not (eq x y)`.
+- `lt`, `le`, `gt`, `ge`: `forall a. Ord a => (a borrow, a borrow) -> Bool`,
+  bodies pattern-matching `compare` against the appropriate
+  `Ordering` shapes.
+
+### 4. C-runtime functions
+
+`runtime/str.c` shipped its two functions in iter 23.2 and 23.3:
+`ail_str_eq(a, b) -> bool` (byte-equality on constant-string layouts)
+and `ail_str_compare(a, b) -> i32` (lex comparison returning
+-1/0/+1). No further runtime work.
+
+Existing primitive operators (`==`, `<`, `<=`, `>`, `>=`) remain
+primitive and per-type-routed at lowering, unchanged. Routing them
+through the class methods is the declared P2 follow-up; the
+redundancy between primitive `==` and class `eq x y` on
+Int/Bool/Str is acknowledged and ratified as transitional.
+
+## Components (iterations)
+
+| Iter | Status | Scope |
+|------|--------|-------|
+| 23.1 | shipped (2026-05-10) | `Ordering` ADT + prelude skeleton + auto-load via `check_workspace`. |
+| 23.2 | shipped (2026-05-10) | `class Eq` + `Eq Int/Bool/Str` + `ail_str_eq`. |
+| 23.3 | shipped (2026-05-10) | `class Ord extends Eq` + `Ord Int/Bool/Str` + `ail_str_compare`. |
+| 23.4-prep | shipped, **kept** | commits `8d39f13` (linearity registers `Def::Class` method types in globals) + `aef4ab8` (check bare-name fall-through to implicit-imported free fns). Both resolve names *before* mono; independent of B1. |
+| 23.4-prep2 / 23.4-prep3 | shipped, **rolled back in 23.4** | commits `a06159d` + `c42a0f5` — codegen bare-name fall-throughs. Provably dead after Mono unification. |
+| **23.4** (revised) | upcoming | **Mono-Pass unification.** Restructure `crates/ailang-check/src/mono.rs::monomorphise_workspace` into one specialiser with two source-body entry points (class-method via `Registry::entries`, free-fn direct). Extend `collect_mono_targets` to also produce targets for polymorphic free-fn calls with fully-concrete substitutions. Remove `lower_polymorphic_call` + `module_polymorphic_fns` + `mono_queue` from codegen. Rollback prep2 + prep3. Amend DESIGN.md §"Resolution and monomorphisation" to describe the pass as covering all `Type::Forall`-Defs. Tests: existing polymorphic fixtures (`poly_id`, `poly_apply`, `poly_box_proj`) green; new fixture `cmp_max_smoke` proves cross-cutting (`cmp_max : forall a. Ord a => (a, a) -> a` at Int synthesises both `cmp_max__Int` and nested `compare__Int` in one fixpoint). |
+| **23.5** (revised) | upcoming | **Prelude free fns + E2E.** Add `ne`/`lt`/`le`/`gt`/`ge` to `examples/prelude.ail.json`. E2E fixtures: (a) positive polymorphic helper at Int/Bool/Str, (b) negative — `eq f g` at Float typecheck-rejects with Float-aware diagnostic, (c) user-ADT — `IntBox` with `Eq`/`Ord` instances + polymorphic helper monomorphises to the user instance. Amend DESIGN.md §"Decision 11 / Prelude classes" — Eq/Ord shipped; the "Milestone 22 ships no built-in Prelude classes" wording stays as historical accuracy with a forward-pointing addendum. Roadmap: P1 Post-22 Prelude entry from `[~]` to `[x]` for Eq/Ord half; Show half stays. |
+
+## Data flow
+
+Two trajectories show the unification at work.
+
+### Class-method call `(eq x y)` with `x : Int` (unchanged)
+
+1. **Typecheck.** `eq` resolves to
+   `forall a. Eq a => (a borrow, a borrow) -> Bool`. Constraint solver
+   matches `Eq Int` against `instance Eq Int`; constraint
+   discharged.
+2. **Mono (class-method entry).** `Registry::entries[(Eq, Int)]`
+   lookup, body from `InstanceMethod`, rigid-var subst `a → Int`,
+   synth `eq__Int`. Call site `eq x y` → `eq__Int x y`.
+3. **Codegen.** `eq__Int` lowers to `icmp eq i64` + `zext i1 i8`.
+
+### Polymorphic free-fn call `(ne x y)` with `x : Int` (new with B1)
+
+1. **Typecheck.** `ne` resolves to a polymorphic `Def::Fn` with
+   `forall a. Eq a => (a borrow, a borrow) -> Bool`. Bare-name lookup
+   reaches the prelude via prep1's `env.module_globals` fall-through.
+   Constraint `Eq Int` discharged as above.
+2. **Mono (free-fn entry).** Body taken directly from
+   `Def::Fn.body`, rigid-var subst `a → Int`, synth `ne__Int`. In
+   the same fixpoint round, the body walker detects the nested
+   `eq` call at concrete `Int` and schedules it as a class-method
+   target. The next round synthesises `eq__Int` (or cache-hits).
+   `ne__Int`'s body refers directly to `eq__Int`. Call site
+   `ne x y` → `ne__Int x y`.
+3. **Codegen.** `ne__Int` lowers as any monomorphic fn would; the
+   nested `eq__Int` is a direct call. No `lower_polymorphic_call`
+   path involved — the codegen-time specialiser no longer exists.
+
+The fixpoint loop in `monomorphise_workspace` (line 88) already
+iterates until a round adds nothing new. The change is in the
+target collector: it must additionally emit `MonoTarget`s for
+"call site to polymorphic free-fn `Def::Fn` with fully-concrete
+substitution", not only for class-constraint residuals.
+
+## Error handling
+
+Unchanged from original spec:
+
+- **`NoInstance Eq Float` / `NoInstance Ord Float`** — fired at
+  typecheck when class resolution selects Float. Diagnostic must
+  cross-reference DESIGN.md §"Float semantics" so the LLM-author
+  immediately learns the partial-Float story.
+- **`NoInstance Eq <UserType>` / `NoInstance Ord <UserType>`** —
+  re-uses 22's existing diagnostic path.
+- **`OrphanInstance`** — Decision 11 unchanged. Prelude instances
+  are non-orphan.
+
+New categories under B1:
+
+- **Polymorphic-free-fn specialisation failures** are
+  `CheckError::Internal`. The mono pass runs post-typecheck, so
+  every substitution must have been validated by then. A failure
+  here is a caller-contract violation; mirrors the existing
+  convention in `synthesise_mono_fn` (mono.rs line 549).
+- **Recursive polymorphic free fns with concrete substitutions** —
+  the existing fixpoint loop closes transitively, same mechanism
+  used for class-method bodies calling other class methods (e.g.
+  `default ne x y = not (eq x y)`).
+- **Codegen-side errors remain not expected.** The unification
+  reduces codegen's responsibility (removes
+  `lower_polymorphic_call`), it does not expand it. Any
+  fall-through that survives must be
+  `CodegenError::Internal`-shaped per the iter-4.4 Floats precedent
+  — never `unimplemented!()` panic.
+
+## Testing strategy
+
+### 23.4 — Mono unification
+
+- **Regression: existing polymorphic fixtures stay green.**
+  `examples/poly_id.ail.json`, `examples/poly_apply.ail.json`,
+  `examples/poly_box_proj.ail.json`, and every 22b.3 typeclass
+  fixture must compile and run unchanged. These are the
+  load-bearing proof that codegen-time specialisation was
+  structurally replaceable.
+- **New: composition fixture.** `examples/cmp_max_smoke.ail.json`
+  with `fn cmp_max : forall a. Ord a => (a, a) -> a` (body:
+  `match compare x y with LT -> y | _ -> x`), invoked at Int. The
+  test asserts that after mono, the workspace contains both
+  `cmp_max__Int` and `compare__Int` as `Def::Fn`, both produced
+  by the unified pass. This pins the cross-cutting case that
+  iter-23.4-prep3 unsuccessfully tried to patch.
+- **Hash-stability of existing mono symbols.** `eq__Int`,
+  `compare__Str`, and the four other already-synthesised symbols
+  must produce identical bodies (and therefore identical hashes)
+  under the unified pass. Pin test in the style of
+  `crates/ailang-core/src/hash.rs::ct4_migrated_fixtures_have_canonical_form_hashes`.
+- **Rollback proof.** `cargo test --workspace` green after removal
+  of `lower_polymorphic_call` + `module_polymorphic_fns` +
+  `mono_queue`. No test relies on the removed symbols.
+- **Bench regression check.** `bench/check.py` /
+  `bench/compile_check.py` re-run after 23.4. The mono pass does
+  more work (two entry points, larger target sets per round); a
+  measurable compile-time shift is expected and ratified per audit
+  convention or rebaselined.
+
+### 23.5 — Prelude free fns + E2E
+
+- **Workspace tests per free fn:** `ne`, `lt`, `le`, `gt`, `ge`
+  produce correct `Bool` on Int/Bool/Str, agree with their
+  primitive-operator counterparts on a small smoke suite.
+- **Positive E2E** `examples/eq_ord_polymorphic.ail.json`:
+  polymorphic helper invoked at three primitives, prints expected
+  output, compiles and runs end-to-end.
+- **Negative E2E:** `eq f g` at Float typecheck-rejects with a
+  Float-aware diagnostic; gold-standard test pins the message
+  verbatim.
+- **User-ADT integration:** `examples/eq_ord_user_adt.ail.json` —
+  `data IntBox = MkIntBox Int` + `instance Eq IntBox` +
+  `instance Ord IntBox` + polymorphic helper monomorphises to the
+  user instances.
+- **Round-trip:** prelude module + every new fixture passes
+  Form-A parser + canonicaliser bit-stable.
+- **Bench regression check** at milestone close: the three bench
+  scripts exit 0 or audit-ratified.
+
+## Acceptance criteria
+
+The milestone closes when:
+
+1. **23.4 has landed:** `crates/ailang-check/src/mono.rs::monomorphise_workspace`
+   synthesises both class-method and polymorphic-free-fn mono Defs
+   in one fixpoint loop. `crates/ailang-codegen/src/lib.rs::lower_polymorphic_call` +
+   `module_polymorphic_fns` + `mono_queue` are removed. Commits
+   `a06159d` (prep2) + `c42a0f5` (prep3) are rolled back.
+2. **DESIGN.md §"Resolution and monomorphisation" amended:** the
+   pass description covers all `Type::Forall`-quantified Defs, not
+   only class methods.
+3. **23.5 has landed:** `examples/prelude.ail.json` contains `ne`,
+   `lt`, `le`, `gt`, `ge` with correct constraint signatures and
+   bodies.
+4. **DESIGN.md §"Decision 11 / Prelude classes" amended:** reflects
+   Eq/Ord shipping in milestone 23; the "Milestone 22 ships no
+   built-in Prelude classes" wording stays as historical accuracy
+   with a forward-pointing addendum.
+5. **Tests pass:** `cargo test --workspace` green; existing
+   polymorphic fixtures (`poly_id`, `poly_apply`, `poly_box_proj`)
+   unchanged; new composition fixture (`cmp_max_smoke`) green; E2E
+   fixtures from 23.5 green.
+6. **Bench regression ratified:** `bench/check.py && bench/compile_check.py && bench/cross_lang.py`
+   exit 0 or audit-ratified with journal entry.
+7. **Surface acceptance from original spec:** a polymorphic helper
+   `forall a. Ord a => (a, a) -> Bool` compiles, monomorphises at
+   three primitive types, runs, and prints the expected output for
+   at least Int and Str; the same helper on Float fires
+   `NoInstance Ord Float` at typecheck with a Float-aware
+   diagnostic.
+8. **Roadmap update:** P1 Post-22 Prelude entry from `[~]` to `[x]`
+   for Eq/Ord half; Show half stays as a separate entry.
+
+## Out of scope (deferred, with substantive rationale)
+
+Unchanged from original spec:
+
+- **`Show` typeclass.** Defers behind a heap-Str-ABI milestone.
+  `instance Show Int` needs `int_to_str` to allocate a heap-Str —
+  a runtime primitive AILang does not have today.
+- **Operator routing through `Eq` / `Ord`.** `==`, `<`, etc. stay
+  primitive this milestone. Routing them through the class methods
+  is the declared P2 todo, gated on bench rebaseline confirmation.
+- **`print`-rewire through `Show.show`.** Same heap-Str dependency.
+- **`Eq` / `Ord` on Float.** No instance per DESIGN.md §"Float
+  semantics". A future iter exposing a partial
+  `compare : Float -> Float -> Maybe Ordering` is a separate
+  brainstorm.
+- **`deriving (Eq, Ord)` for user ADTs.** No auto-derivation.
+- **`Ord Ordering` instance.** Cute but no concrete demand.
+
+New under B1 unification:
+
+- **Higher-rank polymorphism.** Stays out of scope per DESIGN.md
+  §"Polymorphism via Type::Forall" (line 2138-2140). The unified
+  mono pass requires fully-concrete substitution at each call site;
+  the same constraint as today, not weakened.
+- **Polymorphic constants** (`Type::Forall` on `ConstDef`). The mono
+  pass operates on `Def::Fn`; `const_as_pseudo_fn` (mono.rs line
+  261) is the only `ConstDef` bridge and stays unchanged.
+- **User-customisable mono-symbol naming.** The naming format is
+  implementation-finalised in 23.4; no user-facing knob.
+
+## Open commitments (23.4 / 23.5 implementer)
+
+- **Mono-symbol naming for N-ary type vars.** Today's class-method
+  naming `<method>__<typesurfacename>` is single-type-var.
+  Polymorphic free fns can have N type vars (e.g. `poly_apply : forall a b.`).
+  Default proposal: `<name>__<typename1>__<typename2>__…` in
+  Forall-vars declaration order, hash-stable, covered by the
+  canonical-type-names layer. Implementer may raise an alternative
+  via `NEEDS_CONTEXT`.
+- **Target-collector heuristic.** `collect_mono_targets` (mono.rs
+  line 422) today filters on residual class-constraints. For
+  polymorphic free fns, the collector must additionally detect
+  "call site to polymorphic free-fn `Def::Fn` with fully-concrete
+  substitution, regardless of constraints". Implementer decides
+  between extending the existing `synth`-residual path or adding a
+  separate walker; both shapes are structurally viable.
+- **Original Free-Fn `Def::Fn` retention post-mono.** `Def::Class` /
+  `Def::Instance` are kept in the workspace after mono (mono.rs
+  line 40-42, for `ail describe`). Polymorphic Free-Fn `Def::Fn`s
+  should be kept analogously — both the source-Def and the
+  synthesised mono-Defs visible.
+- **Float-NoInstance diagnostic wording.** Implementer drafts a
+  one-line Float-aware message; orchestrator reviews in
+  spec-compliance phase.
+
+## Known costs
+
+- **23.4 mono refactor:** estimated +150 / −50 LOC in
+  `crates/ailang-check/src/mono.rs` (target-collector extension,
+  source-body entry points, naming helper).
+- **23.4 codegen cleanup:** estimated −200 LOC in
+  `crates/ailang-codegen/src/lib.rs` (`lower_polymorphic_call`,
+  `module_polymorphic_fns` fields, `mono_queue` machinery). Net
+  code reduction expected.
+- **23.4 rollback:** `git revert a06159d c42a0f5` plus adaptation
+  to the newly-dead code paths in codegen, estimated −80 LOC.
+- **23.5 prelude additions:** `examples/prelude.ail.json` +30-40
+  lines (five free fns with Forall-constraint signatures and
+  bodies). Three new E2E `.ail.json` fixtures, ~60 lines JSON.
+  Diagnostic test ~20 lines Rust.
+- **Compile-time shift:** mono pass does more work (additional
+  body walks over free fns, potentially larger fixpoint
+  convergence). Quantified by `bench/compile_check.py` post-23.4;
+  audit-ratified or rebaselined.
+- **DESIGN.md amendments:** §"Resolution and monomorphisation"
+  (line 1513+) extends to cover polymorphic free fns; §"Decision
+  11 / Prelude classes" (line 1659+) reflects Eq/Ord shipping.
+
+## Load-bearing assumptions about current behaviour
+
+Surfaced explicitly so the Step 7.5 grounding-check agent has a
+canonical list to ratify. Each assumption is something this spec
+relies on as currently-true.
+
+1. `crates/ailang-check/src/mono.rs::monomorphise_workspace`
+   today is the only typecheck-time specialiser, and it operates
+   exclusively on class-method residuals (no free-fn handling).
+2. `crates/ailang-codegen/src/lib.rs::lower_polymorphic_call`
+   today is the only codegen-time specialiser, and it operates
+   exclusively on polymorphic free-fn calls (no class-method
+   handling).
+3. The mono pass produces `Def::Fn` entries in the workspace; the
+   codegen-time specialiser emits LLVM symbols without
+   corresponding workspace Defs.
+4. `examples/prelude.ail.json` today contains no free fns (only
+   ADT, classes, instances).
+5. Commits `a06159d` (prep2) and `c42a0f5` (prep3) added codegen
+   bare-name fall-throughs that were anticipatory patches for the
+   prelude free fns; they have no currently-active load-bearing
+   case outside the still-not-shipped 23.4 free fns.
+6. Commit `8d39f13` (prep.1, linearity) and commit `aef4ab8`
+   (prep.2, check bare-name) operate at typecheck / linearity time
+   — before any mono pass — and are load-bearing for any prelude
+   free-fn resolution regardless of mono architecture.
+7. `crates/ailang-codegen/src/lib.rs::lower_polymorphic_call` is
+   invoked from two call sites today (lines 1944, 1972), both of
+   which become direct mono-symbol calls after 23.4.
+8. `examples/poly_id.ail.json` and `examples/poly_apply.ail.json`
+   today rely on the codegen-time specialiser path; under B1 they
+   transition to the typecheck-time mono pass without surface
+   behavioural change.
+9. The mono pass's fixpoint loop (mono.rs line 88) iterates until a
+   round adds nothing new, and already supports transitive
+   specialisation across nested class-method calls; the same
+   mechanism handles a free-fn body whose specialisation triggers
+   a class-method specialisation.
+10. The canonical-form layer (per
+    `docs/specs/2026-05-10-canonical-type-names.md`, ct.4 closure)
+    treats mono Defs as post-typecheck artefacts not in
+    `CheckedModule.symbols`, so renaming or extending mono symbols
+    does not affect surface-level hash pins.