diff --git a/bench/orchestrator-stats/2026-05-12-iter-23.5.json b/bench/orchestrator-stats/2026-05-12-iter-23.5.json
new file mode 100644
index 0000000..1de815a
--- /dev/null
+++ b/bench/orchestrator-stats/2026-05-12-iter-23.5.json
@@ -0,0 +1,44 @@
+{
+  "iter_id": "23.5",
+  "date": "2026-05-12",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 8,
+  "tasks_completed": 8,
+  "reloops_per_task": {
+    "1": 0,
+    "2": 0,
+    "3": 0,
+    "4": 0,
+    "5": 0,
+    "6": 0,
+    "7": 0,
+    "8": 0
+  },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null,
+  "bench_results": {
+    "check_py_exit": 0,
+    "compile_check_py_exit": 1,
+    "compile_check_py_note": "one sub-ms check_ms regression (check_ms.local_rec_capture +26.36% over 25% tolerance) — ratifiable per audit tolerance, prelude grew by 5 polymorphic Def::Fns this iter",
+    "cross_lang_py_exit": 0
+  },
+  "inline_implementer_fixes": [
+    {
+      "file": "crates/ailang-check/src/linearity.rs",
+      "summary": "Workspace-aware visibility for imported poly free fns + class methods; symmetric extension of iter 23.4-prep",
+      "surfaced_by": "Task 3 user-defined at_most calling prelude gt"
+    },
+    {
+      "file": "crates/ailang-check/src/mono.rs",
+      "summary": "Distinguish rigid Type::Var (skip) from $m-prefixed metavars (Unit-default) in free-fn target collection",
+      "surfaced_by": "Task 3 — at_most's polymorphic body emitted spurious gt__Unit target"
+    },
+    {
+      "file": "examples/test_22b1_missing_method.ail.json",
+      "summary": "Rename class method ne→tne to avoid collision with new prelude free fn ne",
+      "surfaced_by": "Task 1 — workspace registry method-name uniqueness check"
+    }
+  ]
+}
diff --git a/crates/ail/tests/eq_float_noinstance.rs b/crates/ail/tests/eq_float_noinstance.rs
new file mode 100644
index 0000000..6fecd70
--- /dev/null
+++ b/crates/ail/tests/eq_float_noinstance.rs
@@ -0,0 +1,45 @@
+//! Pins the Float-aware `NoInstance` diagnostic added in milestone 23.
+//!
+//! Property protected: a polymorphic Eq/Ord helper invoked at Float
+//! fires `no-instance` (since Float has neither Eq nor Ord instance
+//! per DESIGN.md §"Float semantics") AND the diagnostic message
+//! cross-references the canonical Float-semantics section so the
+//! LLM author immediately learns the partial-Float story rather
+//! than seeing a bare "no instance" message.
+
+use ailang_check::check_workspace;
+use ailang_core::workspace::load_workspace;
+use std::path::PathBuf;
+
+fn fixture(name: &str) -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("../../examples")
+        .join(name)
+}
+
+#[test]
+fn eq_at_float_fires_float_aware_noinstance() {
+    let ws = load_workspace(&fixture("eq_float_noinstance.ail.json")).expect("load");
+    let diags = check_workspace(&ws);
+
+    assert!(!diags.is_empty(), "expected NoInstance diagnostic, got none");
+
+    let no_inst = diags
+        .iter()
+        .find(|d| d.code == "no-instance")
+        .unwrap_or_else(|| panic!("expected diagnostic with code 'no-instance', got: {diags:#?}"));
+
+    assert!(
+        no_inst.message.contains("Float"),
+        "expected Float-aware NoInstance diagnostic, got message: {:?}",
+        no_inst.message
+    );
+
+    // Cross-ref to DESIGN.md §Float semantics — the LLM author should be
+    // pointed at the canonical explanation of partial Float orderability.
+    assert!(
+        no_inst.message.contains("Float semantics") || no_inst.message.contains("DESIGN"),
+        "expected NoInstance message to cross-reference DESIGN.md §Float semantics, got: {:?}",
+        no_inst.message
+    );
+}
diff --git a/crates/ail/tests/eq_ord_e2e.rs b/crates/ail/tests/eq_ord_e2e.rs
new file mode 100644
index 0000000..8efc4aa
--- /dev/null
+++ b/crates/ail/tests/eq_ord_e2e.rs
@@ -0,0 +1,126 @@
+//! End-to-end tests for the Eq/Ord prelude shipped in milestone 23.
+//!
+//! These tests compile a `.ail.json` workspace via the `ail build`
+//! subcommand, run the resulting native binary, and assert on stdout.
+//! Together they protect:
+//!
+//! 1. Polymorphic-helper composition over the prelude free fns at
+//!    three primitive types (`eq_ord_polymorphic_runs_end_to_end`).
+//!    Property: a user-defined `forall a. Ord a => …` helper that
+//!    calls `gt`/`not` is monomorphised correctly at Int / Bool / Str.
+//! 2. User-ADT integration with the unified mono pass
+//!    (`eq_ord_user_adt_runs_end_to_end`). Property: `instance Eq T`
+//!    + `instance Ord T` for a user-defined `T` produces working
+//!    mono symbols when invoked through the prelude.
+//! 3. Mono-symbol body-hash stability for `eq__IntBox`
+//!    (`eq_ord_user_adt_eq_intbox_hash_stable`). Property: the user
+//!    instance body that the unified pass emits for IntBox is
+//!    bit-stable across refactors; drift here means either a
+//!    legitimate emission change (re-record) or a regression
+//!    (investigate). Mirrors `crates/ail/tests/mono_hash_stability.rs`.
+
+use ailang_check::{check_workspace, monomorphise_workspace};
+use ailang_core::ast::Def;
+use ailang_core::hash::def_hash;
+use ailang_core::workspace::load_workspace;
+use std::path::PathBuf;
+use std::process::Command;
+
+fn fixture_path(name: &str) -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("../../examples")
+        .join(name)
+}
+
+fn build_and_run(fixture: &str) -> String {
+    let src = fixture_path(fixture);
+    let out = std::env::temp_dir().join(format!("ail_{}.bin", fixture.replace('.', "_")));
+
+    let build = Command::new(env!("CARGO_BIN_EXE_ail"))
+        .args(["build", src.to_str().unwrap(), "-o", out.to_str().unwrap()])
+        .output()
+        .expect("ail build");
+    assert!(
+        build.status.success(),
+        "ail build failed:\nstdout: {}\nstderr: {}",
+        String::from_utf8_lossy(&build.stdout),
+        String::from_utf8_lossy(&build.stderr),
+    );
+
+    let run = Command::new(&out).output().expect("run binary");
+    assert!(
+        run.status.success(),
+        "binary exited non-zero:\nstdout: {}\nstderr: {}",
+        String::from_utf8_lossy(&run.stdout),
+        String::from_utf8_lossy(&run.stderr),
+    );
+    String::from_utf8_lossy(&run.stdout).trim().to_string()
+}
+
+#[test]
+fn eq_ord_polymorphic_runs_end_to_end() {
+    let stdout = build_and_run("eq_ord_polymorphic.ail.json");
+    // Helper `at_most(3, 5)` at Int = true → 1
+    // `at_most(true, false)` at Bool = false → 0
+    // `at_most("abc", "abd")` at Str = true → 1
+    // `io/print_int` emits one int per line, so stdout is "1\n0\n1"
+    // after `.trim()` strips the trailing newline.
+    assert_eq!(stdout, "1\n0\n1", "expected 1\\n0\\n1, got {stdout:?}");
+}
+
+#[test]
+fn eq_ord_user_adt_runs_end_to_end() {
+    let stdout = build_and_run("eq_ord_user_adt.ail.json");
+    // eq(MkIntBox 3, MkIntBox 3) = true → 1
+    // eq(MkIntBox 3, MkIntBox 5) = false → 0
+    // `io/print_int` emits one int per line; trimmed stdout is "1\n0".
+    assert_eq!(stdout, "1\n0", "expected 1\\n0, got {stdout:?}");
+}
+
+#[test]
+fn eq_ord_user_adt_eq_intbox_hash_stable() {
+    let ws = load_workspace(&fixture_path("eq_ord_user_adt.ail.json")).expect("load");
+    let diags = check_workspace(&ws);
+    assert!(diags.is_empty(), "typecheck failed: {diags:#?}");
+    let mono = monomorphise_workspace(&ws).expect("mono");
+
+    // The mono symbol for `eq` at a user-defined ADT uses the
+    // `<method>__<8-hex-prefix>` mangling per DESIGN.md
+    // §"Mangling scheme" (primitives use the bare type name; compound
+    // / user-defined types use the 8-hex BLAKE3 prefix of the
+    // canonical type bytes). We look up the single `eq__` symbol
+    // synthesised at `IntBox` — there is only one user instance,
+    // so the find-by-prefix is unambiguous in this fixture.
+    let eq_intbox = mono
+        .modules
+        .values()
+        .flat_map(|m| m.defs.iter())
+        .find_map(|d| match d {
+            Def::Fn(f) if f.name.starts_with("eq__") && f.name != "eq__Int"
+                && f.name != "eq__Bool" && f.name != "eq__Str" =>
+            {
+                Some(f)
+            }
+            _ => None,
+        })
+        .expect("eq__<IntBox-hash> not synthesised");
+
+    // The 8-hex-prefix in the mono-symbol name is the BLAKE3 prefix
+    // of the canonical IntBox type bytes (DESIGN.md §"Mangling
+    // scheme"). Drift here means either the canonical-form encoding
+    // changed or the type's canonical bytes changed — both warrant
+    // investigation before re-pinning.
+    assert_eq!(
+        eq_intbox.name, "eq__cde77856",
+        "eq__IntBox mono-symbol name drifted — type-mangling regression?"
+    );
+
+    // The body hash pins the unified mono pass's IntBox eq emission.
+    // Drift means either a legitimate refactor (re-record) or a
+    // regression in user-instance body propagation (investigate).
+    let h = def_hash(&Def::Fn(eq_intbox.clone()));
+    assert_eq!(
+        h, "9daaffa7528d2a1c",
+        "eq__IntBox body hash drifted — see mono_hash_stability.rs for the resolution pattern"
+    );
+}
diff --git a/crates/ail/tests/prelude_free_fns.rs b/crates/ail/tests/prelude_free_fns.rs
new file mode 100644
index 0000000..3b51dab
--- /dev/null
+++ b/crates/ail/tests/prelude_free_fns.rs
@@ -0,0 +1,82 @@
+//! Workspace-level tests for the polymorphic prelude free fns
+//! `ne` / `lt` / `le` / `gt` / `ge` shipped in milestone 23.
+//!
+//! Property protected: each free fn is monomorphised on demand at the
+//! call site's concrete type, producing a mono symbol named
+//! `<fn>__<TypeName>`. If the unified mono pass (iter 23.4) stops
+//! emitting the free-fn mono arm, or the prelude entry for the fn
+//! gets renamed / dropped, these tests fail.
+//!
+//! See `crates/ail/tests/mono_unification.rs` (iter 23.4) for the
+//! end-to-end runtime correctness checks; this file checks only that
+//! the mono symbols are produced.
+
+use ailang_check::{check_workspace, monomorphise_workspace};
+use ailang_core::workspace::load_workspace;
+use std::path::PathBuf;
+
+fn fixture(name: &str) -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("../../examples")
+        .join(name)
+}
+
+fn mono_symbol_names(workspace_name: &str) -> Vec<String> {
+    let ws = load_workspace(&fixture(workspace_name)).expect("load");
+    let diags = check_workspace(&ws);
+    assert!(diags.is_empty(), "typecheck failed: {:#?}", diags);
+    let mono = monomorphise_workspace(&ws).expect("mono");
+    mono.modules
+        .values()
+        .flat_map(|m| m.defs.iter())
+        .filter_map(|d| match d {
+            ailang_core::ast::Def::Fn(f) => Some(f.name.clone()),
+            _ => None,
+        })
+        .collect()
+}
+
+#[test]
+fn ne_at_int_produces_mono_symbol() {
+    let names = mono_symbol_names("ne_at_int_smoke.ail.json");
+    assert!(
+        names.iter().any(|n| n == "ne__Int"),
+        "expected ne__Int in workspace, found: {names:#?}"
+    );
+}
+
+#[test]
+fn lt_at_int_produces_mono_symbol() {
+    let names = mono_symbol_names("lt_at_int_smoke.ail.json");
+    assert!(
+        names.iter().any(|n| n == "lt__Int"),
+        "expected lt__Int in workspace, found: {names:#?}"
+    );
+}
+
+#[test]
+fn le_at_str_produces_mono_symbol() {
+    let names = mono_symbol_names("le_at_str_smoke.ail.json");
+    assert!(
+        names.iter().any(|n| n == "le__Str"),
+        "expected le__Str in workspace, found: {names:#?}"
+    );
+}
+
+#[test]
+fn gt_at_bool_produces_mono_symbol() {
+    let names = mono_symbol_names("gt_at_bool_smoke.ail.json");
+    assert!(
+        names.iter().any(|n| n == "gt__Bool"),
+        "expected gt__Bool in workspace, found: {names:#?}"
+    );
+}
+
+#[test]
+fn ge_at_int_produces_mono_symbol() {
+    let names = mono_symbol_names("ge_at_int_smoke.ail.json");
+    assert!(
+        names.iter().any(|n| n == "ge__Int"),
+        "expected ge__Int in workspace, found: {names:#?}"
+    );
+}
diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index 7c14bed..0868fed 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -706,6 +706,24 @@ impl CheckError {
                 body_form_a.clone(),
             );
         }
+        // Iter 23.5: Float-aware addendum on `NoInstance`. When the
+        // unresolved class is `Eq` or `Ord` AND the type is `Float`,
+        // append a cross-reference to DESIGN.md §"Float semantics" so
+        // the LLM author learns the partial-Float story immediately
+        // rather than seeing a bare "no instance" message. Float has
+        // neither Eq nor Ord by design (partial orderability per
+        // IEEE-754), and the polymorphic prelude helpers
+        // (`ne` / `lt` / `le` / `gt` / `ge` / direct `eq` / `compare`)
+        // are the natural surface where the LLM hits this.
+        if let CheckError::NoInstance { class, at_type, .. } = self.inner() {
+            if (class == "Eq" || class == "Ord") && at_type == "Float" {
+                d.message = format!(
+                    "{} — Float has no Eq/Ord instance by design (partial \
+                     orderability per IEEE-754); see DESIGN.md §\"Float semantics\".",
+                    d.message
+                );
+            }
+        }
         d
     }
 }
@@ -852,7 +870,28 @@ pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
         // all-explicit-mode fn are exactly the surface the check is
         // designed to inspect.
         if !had_typecheck_errors {
-            module_diags.extend(linearity::check_module(m));
+            // Iter 23.5: linearity check needs visibility into
+            // polymorphic free fns + class methods from implicitly-
+            // imported modules (currently just the auto-injected
+            // prelude). Without this, a Borrow-mode user fn that
+            // forwards its borrow params into a prelude poly fn
+            // (e.g. `gt x y`) fires `consume-while-borrowed`
+            // false positives because `callee_arg_modes` defaults
+            // to Consume when it cannot see the callee's
+            // `param_modes`. Symmetric to the class-method case
+            // closed in iter 23.4-prep.
+            let visible_extra: Vec<&Module> = ws
+                .modules
+                .iter()
+                .filter_map(|(other_name, other_mod)| {
+                    if other_name == name {
+                        None
+                    } else {
+                        Some(other_mod)
+                    }
+                })
+                .collect();
+            module_diags.extend(linearity::check_module_with_visible(m, &visible_extra));
             // Iter 18d.2: reuse-as shape compatibility check. Runs on
             // the same activation gate as linearity (all-explicit-mode
             // fns only). The check resolves each `(reuse-as <var>
diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs
index 4795510..5575160 100644
--- a/crates/ailang-check/src/linearity.rs
+++ b/crates/ailang-check/src/linearity.rs
@@ -183,13 +183,58 @@ struct BinderState {
 ///
 /// Output ordering: defs in declaration order; within a def, diagnostics
 /// in source-order discovery (depth-first left-to-right walk).
+/// Test-only convenience entry: linearity check on a single Module
+/// with no extra-visible siblings. Production code (`check_workspace`)
+/// uses [`check_module_with_visible`] directly to give the walker
+/// visibility into other workspace modules — in particular, the
+/// auto-injected prelude's polymorphic free fns and class methods.
+#[cfg(test)]
 pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
+    check_module_with_visible(m, &[])
+}
+
+/// Iter 23.5: workspace-aware entry. `visible_extra` is a slice of
+/// modules whose top-level fns and class methods should be visible
+/// to `callee_arg_modes` (so a Borrow-mode user fn that forwards its
+/// borrow params into an imported polymorphic free fn — e.g. the
+/// prelude's `gt` / `ne` / `lt` — sees the imported fn's
+/// `param_modes` and does not false-fire `consume-while-borrowed`).
+///
+/// Symmetric to the iter 23.4-prep extension that made class methods
+/// visible. Bodies of the visible-extra modules are NOT walked here
+/// — they are checked when their own module is processed.
+pub(crate) fn check_module_with_visible(m: &Module, visible_extra: &[&Module]) -> Vec<Diagnostic> {
     let mut globals: HashMap<String, Type> = HashMap::new();
     // Iter 19a.1: ctor name → field types, used by the
     // `over-strict-mode` lint to filter out primitive-typed
     // pattern-binders (Int / Bool / Str / Unit) — their consume
     // does not force ownership of the scrutinee.
     let mut ctors: HashMap<String, Vec<Type>> = HashMap::new();
+
+    // Iter 23.5: register fns + class methods from visible-extra
+    // modules first, so a name-clash inside `m` overwrites the
+    // imported entry (matching the synth-side scope rule that
+    // local-defs shadow implicit imports).
+    for em in visible_extra {
+        for def in &em.defs {
+            match def {
+                Def::Fn(f) => {
+                    globals.insert(f.name.clone(), strip_forall(&f.ty).clone());
+                }
+                Def::Class(c) => {
+                    for cm in &c.methods {
+                        globals.insert(cm.name.clone(), strip_forall(&cm.ty).clone());
+                    }
+                }
+                // Const / Type / Instance: not relevant for callee-arg-mode
+                // resolution (Const can't be a callee; Type's ctors are
+                // construction sites not fn calls; Instance bodies are
+                // walked separately as Def::Fn post-mono).
+                _ => {}
+            }
+        }
+    }
+
     for def in &m.defs {
         match def {
             Def::Fn(f) => {
diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs
index 2f7ab59..58b8b06 100644
--- a/crates/ailang-check/src/mono.rs
+++ b/crates/ailang-check/src/mono.rs
@@ -650,18 +650,40 @@ pub fn collect_mono_targets(
     // would have rejected; the Unit default is sound and
     // deterministic.
     for fc in free_fn_calls {
-        let type_args: Vec<Type> = fc
-            .metas
-            .iter()
-            .map(|m| {
-                let resolved = subst.apply(m);
-                if crate::is_fully_concrete(&resolved) {
-                    resolved
-                } else {
-                    Type::unit()
-                }
-            })
-            .collect();
+        // Iter 23.5: if any resolved type-arg is a rigid Type::Var
+        // (i.e. a forall var of the *enclosing* polymorphic fn,
+        // not a free metavar), skip this target. The enclosing fn
+        // will be monomorphised in its own right, and that mono
+        // synthesis re-walks the body with rigid → concrete
+        // substitution, at which point this same call site is
+        // re-observed with concrete type-args. Without the skip, a
+        // body like `at_most x y = not (gt x y)` (a polymorphic
+        // free fn calling another polymorphic free fn) would
+        // produce a spurious `gt__Unit` target whose body
+        // references `compare` at Unit — which has no Ord
+        // instance, so the synthesised body fails to typecheck.
+        //
+        // Unit-default for unbound metavars (e.g. `is_empty(Nil)`
+        // where the elem type is unobservable from the args alone)
+        // is preserved: a metavar resolves to a `$m`-prefixed
+        // Var via `subst.apply`, distinct from a rigid Var.
+        let mut type_args: Vec<Type> = Vec::with_capacity(fc.metas.len());
+        let mut has_rigid = false;
+        for m in &fc.metas {
+            let resolved = subst.apply(m);
+            if crate::is_fully_concrete(&resolved) {
+                type_args.push(resolved);
+            } else if contains_rigid_var(&resolved) {
+                has_rigid = true;
+                break;
+            } else {
+                // Unbound metavar — default to Unit (iter 23.4 behaviour).
+                type_args.push(Type::unit());
+            }
+        }
+        if has_rigid {
+            continue;
+        }
         out.push(MonoTarget::FreeFn {
             name: fc.name.clone(),
             type_args,
@@ -671,6 +693,24 @@ pub fn collect_mono_targets(
     Ok(out)
 }
 
+/// Iter 23.5: true iff `t` contains a non-metavar `Type::Var` anywhere.
+/// Used by free-fn target collection to distinguish rigid forall vars
+/// (skip — wait for the enclosing fn's mono pass) from unbound metavars
+/// (Unit-default — no later round will pin them). The naming
+/// convention is: metavars are `Type::Var { name: "$m<id>" }`; rigid
+/// forall vars use their source name (`a`, `b`, …) which cannot start
+/// with `$` per the identifier rules.
+fn contains_rigid_var(t: &Type) -> bool {
+    match t {
+        Type::Var { name } => !name.starts_with("$m"),
+        Type::Con { args, .. } => args.iter().any(contains_rigid_var),
+        Type::Fn { params, ret, .. } => {
+            params.iter().any(contains_rigid_var) || contains_rigid_var(ret)
+        }
+        Type::Forall { body, .. } => contains_rigid_var(body),
+    }
+}
+
 /// Iter 22b.3: produce a `FnDef` for a single (target, class,
 /// instance) triple. The synthesised fn:
 ///
diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs
index cf4484b..6877183 100644
--- a/crates/ailang-core/src/workspace.rs
+++ b/crates/ailang-core/src/workspace.rs
@@ -1780,10 +1780,11 @@ mod tests {
 
     /// Iter 22b.1: an instance that omits a required (non-default)
     /// method of its class fires `MissingMethod`. The fixture's
-    /// `class TEq` declares `teq` and `ne` as both non-default; the
-    /// instance only specifies `ne`, leaving `teq` missing.
-    /// (Class is `TEq` rather than `Eq` to avoid colliding with the
-    /// auto-loaded prelude's `class Eq`.)
+    /// `class TEq` declares `teq` and `tne` as both non-default; the
+    /// instance only specifies `tne`, leaving `teq` missing.
+    /// (Class is `TEq` (and method `tne`) rather than `Eq` / `ne` to
+    /// avoid colliding with the auto-loaded prelude's `class Eq` and
+    /// — since iter 23.5 — the prelude's polymorphic free fn `ne`.)
     #[test]
     fn iter22b1_missing_method_fires_diagnostic() {
         let entry = examples_dir().join("test_22b1_missing_method.ail.json");
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 391ba83..709e711 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -1701,6 +1701,16 @@ end-to-end path is the milestone's typeclass acceptance gate
 `instance Foo IntBox`); see `docs/specs/2026-05-09-22-typeclasses.md`
 "Amendments" for the substantive rationale.
 
+Milestone 23 amends the above: the prelude now ships the `Ordering`
+ADT, the `Eq` and `Ord` classes, primitive `Eq Int/Bool/Str` and
+`Ord Int/Bool/Str` instances, and the five polymorphic free-fn helpers
+`ne` / `lt` / `le` / `gt` / `ge`. `Show`, operator routing through
+`Eq`/`Ord`, and `print`-rewire remain out of scope per their original
+substantive reasons (heap-`Str` ABI, bench rebaseline). Float has
+neither `Eq` nor `Ord` instance per §"Float semantics"; a polymorphic
+helper invoked at Float fires `NoInstance` at typecheck with a
+Float-aware diagnostic cross-referencing this section.
+
 Primitive output goes through `io/print_int` / `io/print_bool` /
 `io/print_str` directly.
 
diff --git a/docs/journals/2026-05-12-iter-23.5.md b/docs/journals/2026-05-12-iter-23.5.md
new file mode 100644
index 0000000..f1153fc
--- /dev/null
+++ b/docs/journals/2026-05-12-iter-23.5.md
@@ -0,0 +1,200 @@
+# iter 23.5 — Prelude free fns + E2E (Eq/Ord milestone close)
+
+**Date:** 2026-05-12
+**Started from:** 35c6eb5
+**Status:** DONE
+**Tasks completed:** 8 of 8
+
+## Summary
+
+Closes milestone 23. Ships the five polymorphic prelude free fns
+`ne` / `lt` / `le` / `gt` / `ge` (Tasks 1-2), three end-to-end
+fixtures covering primitive composition + user-ADT integration +
+the Float negative case (Tasks 3-5), the Float-aware `NoInstance`
+diagnostic addendum (Task 5), the DESIGN.md §"Prelude classes"
+amendment (Task 6), and the roadmap split between shipped Eq/Ord
+and the pending Show + print-rewire half (Task 7). Bench check
+runs clean except a noisy sub-millisecond `check_ms.local_rec_capture`
+regression that sits just over the 25% tolerance — ratifiable per
+the audit-tolerance rule (the prelude grew by 5 polymorphic
+`Def::Fn`s, so the typecheck workload per workspace measurably
+shifts).
+
+Two implementer-phase fixes were needed beyond the plan, both
+symmetric to existing precedent (iter 23.4-prep). They surfaced
+when the natural test fixtures (user-defined `at_most x y = not (gt
+x y)` composing prelude poly fns) hit two distinct false-positive
+shapes:
+
+1. **Linearity check needed workspace-wide visibility** for
+   imported polymorphic free fns + class methods. Previously the
+   linearity pass only saw the current module's globals, so a
+   user `at_most` forwarding its borrow params into `gt` (defined
+   in the prelude) hit `callee_arg_modes("gt", 2) → []` →
+   default-Consume → `consume-while-borrowed` false positive. Fix
+   extends `linearity::check_module` to a `check_module_with_visible`
+   entry that takes additional Module references whose top-level fns
+   + class methods are registered in globals; the workspace-side
+   driver passes all sibling modules. Pure precedent extension of
+   23.4-prep, which added class-method visibility for the same
+   reason.
+
+2. **Mono pass needed to skip rigid-var-bearing free-fn targets.**
+   When a polymorphic free fn's body calls another polymorphic
+   free fn (e.g. `at_most`'s body calls `gt x y` with x, y of
+   type rigid `a`), the synth-channel observer recorded a
+   FreeFnCall whose type args were rigid `Type::Var { name: "a"
+   }`. The existing Unit-default fallback (correct for
+   `is_empty(Nil)`-shape unobservable metavars) was unsound here:
+   it produced `gt__Unit` whose body referenced `compare`, which
+   has no Unit instance → "unknown variable: compare" at the
+   synthesised body. Fix discriminates rigid vars
+   (Type::Var without `$m` prefix) from unbound metavars (`$m`
+   prefix) — rigids skip (they get re-collected with concrete
+   substitution when the enclosing fn itself monomorphises),
+   metavars keep their Unit-default.
+
+One existing fixture (`examples/test_22b1_missing_method.ail.json`)
+had to rename its class method `ne → tne` because `ne` is now a
+top-level prelude free fn and the workspace registry's
+method-name uniqueness check rejected the collision. The
+fixture's docstring already foreshadowed this case ("Class is
+`TEq` rather than `Eq` to avoid colliding…"); extended to also
+cover the `ne → tne` rename rationale.
+
+## Per-task notes
+
+- iter 23.5.1: `ne` free fn — added `Def::Fn ne` to prelude (body
+  `not (eq x y)`); created `crates/ail/tests/prelude_free_fns.rs`
+  with helpers `fixture()` and `mono_symbol_names()` + first test;
+  smoke fixture `examples/ne_at_int_smoke.ail.json`. RED→GREEN.
+  Adjusted `mono.modules.iter()` → `.values()` per the actual
+  `BTreeMap<String, Module>` shape (Boss pre-flight flagged).
+- iter 23.5.2: `lt` / `le` / `gt` / `ge` free fns — four
+  `Def::Fn`s in prelude (each pattern-matches on `compare x y`
+  against one of LT/GT plus a wildcard); four extending tests in
+  the same `prelude_free_fns.rs`; four smoke fixtures. RED→GREEN
+  per fn.
+- iter 23.5.3: positive E2E — `examples/eq_ord_polymorphic.ail.json`
+  with user-defined `at_most a a → Bool` composing prelude `not`
+  + `gt`; `crates/ail/tests/eq_ord_e2e.rs` with helpers
+  `fixture_path()` + `build_and_run()` plus
+  `eq_ord_polymorphic_runs_end_to_end`. Two implementer-phase
+  fixes (linearity + mono rigid-skip) landed during this task to
+  unblock the GREEN. Final stdout pinned at `"1\n0\n1"` (matches
+  `io/print_int`'s actual newline-separator behaviour; plan text
+  had `"101"` based on an incorrect concatenation assumption).
+- iter 23.5.4: user-ADT E2E — `examples/eq_ord_user_adt.ail.json`
+  with `type IntBox = MkIntBox Int` + user-written
+  `instance Eq IntBox` + `instance Ord IntBox` + `main` calling
+  `eq` twice. Two extending tests:
+  `eq_ord_user_adt_runs_end_to_end` (stdout `"1\n0"`) and
+  `eq_ord_user_adt_eq_intbox_hash_stable` (record-then-pin).
+  Mono symbol name is `eq__cde77856` (8-hex-prefix mangling for
+  compound types per DESIGN.md §"Mangling scheme"); body hash
+  pinned at `9daaffa7528d2a1c`. The Ord-IntBox instance's
+  retType needed qualifying as `prelude.Ordering` per the
+  canonical-type-names rule.
+- iter 23.5.5: Float-aware `NoInstance` addendum — implemented in
+  `CheckError::to_diagnostic()` (the per-iter spec-§"NoInstance"
+  conversion path; option-a from the plan's structural-choice
+  list). Addendum fires when `class ∈ {Eq, Ord}` AND `at_type ==
+  "Float"`: appends `— Float has no Eq/Ord instance by design
+  (partial orderability per IEEE-754); see DESIGN.md §"Float
+  semantics".` New `examples/eq_float_noinstance.ail.json` +
+  `crates/ail/tests/eq_float_noinstance.rs`. RED→GREEN.
+- iter 23.5.6: DESIGN.md amendment — inserted Milestone-23
+  amendment paragraph in §"Prelude (built-in) classes". Grep
+  gate RED→GREEN.
+- iter 23.5.7: roadmap split — replaced the single Post-22
+  Prelude entry with two: `[x]` Eq/Ord (shipped 23.5) and `[ ]`
+  Show + print rewire (gated on heap-`Str` ABI). Also
+  disambiguated the `depends on: Post-22 Prelude` reference at
+  line 73 to point specifically at the Eq/Ord half (Op routing's
+  actual dependency).
+- iter 23.5.8: bench gate — `bench/check.py` exit 0 (clean),
+  `bench/compile_check.py` exit 1 (one sub-ms `check_ms`
+  regression at the tolerance line — see Concerns), `bench/cross_lang.py`
+  exit 0 (clean).
+
+## Concerns
+
+- `bench/compile_check.py` exited 1 with one regression:
+  `check_ms.local_rec_capture` measured +26.36% over baseline
+  (1.1ms → 1.4ms, tolerance 25.0%). This is a sub-millisecond
+  noise-band metric, and the prelude grew by 5 polymorphic
+  `Def::Fn`s in this iter so a measurable typecheck-workload
+  shift is expected per the Boss-noted audit tolerance. Two
+  other check_ms metrics in the first run (`borrow_own_demo`,
+  `bench_list_sum`) crossed the line on one sample but stayed
+  inside on the rerun, confirming this is noise-band fluctuation
+  rather than a structural regression. Recommend ratifying at
+  iter close via `--update-baseline`; flagged as a Boss
+  judgement call.
+- The mono-pass rigid-var skip (Task 3 inline fix) preserves
+  the existing Unit-default for unbound metavars exactly (the
+  `is_empty(Nil)` shape from iter 23.4.8 is untouched). The
+  discrimination is by name prefix (`$m`) which is the same
+  convention `Subst::meta_id` uses; a future schema refactor
+  that drops the prefix convention would silently break the
+  skip rule. Code comment names this.
+- The linearity-side `check_module(&Module)` standalone entry
+  is now `#[cfg(test)]`-gated because production code uses
+  `check_module_with_visible(m, &visible_extra)` instead. Unit
+  tests still call the no-extra path. Acceptable; flagging in
+  case a future caller wants the standalone form back.
+
+## Known debt
+
+- The `eq_ord_user_adt` mono-symbol name (`eq__cde77856`) is
+  pinned by literal string match in the test. If the canonical
+  type-bytes encoding for `IntBox` ever changes (e.g. via a new
+  schema field on `TypeDef`), the test fails with a clear
+  type-mangling-regression message. That is the intended drift
+  alarm; no immediate debt.
+
+## Files touched
+
+- `crates/ailang-check/src/lib.rs` — Float-aware `NoInstance`
+  addendum in `to_diagnostic()`; linearity call site updated to
+  pass workspace siblings as visible-extra.
+- `crates/ailang-check/src/linearity.rs` — new
+  `check_module_with_visible(m, visible_extra)` entry;
+  `check_module(&Module)` made test-only.
+- `crates/ailang-check/src/mono.rs` — free-fn target collection
+  now distinguishes rigid `Type::Var` from `$m`-prefixed
+  metavars; rigid-bearing targets are skipped; new helper
+  `contains_rigid_var`.
+- `crates/ailang-core/src/workspace.rs` — docstring update on
+  the `iter22b1_missing_method` test naming the new `ne` reason
+  for the `TEq`/`tne` rename.
+- `crates/ail/tests/prelude_free_fns.rs` (new) — five workspace-level
+  tests, one per prelude free fn, plus helpers.
+- `crates/ail/tests/eq_ord_e2e.rs` (new) — three E2E tests:
+  polymorphic composition, user-ADT integration, mono-symbol
+  hash stability.
+- `crates/ail/tests/eq_float_noinstance.rs` (new) — Float-aware
+  NoInstance pin.
+- `examples/prelude.ail.json` — five new `Def::Fn` entries
+  (ne / lt / le / gt / ge).
+- `examples/ne_at_int_smoke.ail.json` (new), `lt_at_int_smoke.ail.json`
+  (new), `le_at_str_smoke.ail.json` (new), `gt_at_bool_smoke.ail.json`
+  (new), `ge_at_int_smoke.ail.json` (new) — five workspace-level
+  smoke fixtures.
+- `examples/eq_ord_polymorphic.ail.json` (new) — positive E2E:
+  polymorphic helper composing prelude fns at Int / Bool / Str.
+- `examples/eq_ord_user_adt.ail.json` (new) — user-ADT E2E:
+  `IntBox` with user-written Eq + Ord instances.
+- `examples/eq_float_noinstance.ail.json` (new) — negative-Float
+  fixture firing the addended diagnostic.
+- `examples/test_22b1_missing_method.ail.json` — `ne → tne`
+  rename to avoid collision with the new prelude `ne` free fn.
+- `docs/DESIGN.md` — Milestone-23 amendment paragraph inserted
+  in §"Prelude (built-in) classes".
+- `docs/roadmap.md` — Post-22 Prelude entry split into shipped
+  Eq/Ord + pending Show; Op-routing depends-on reference
+  disambiguated.
+
+## Stats
+
+bench/orchestrator-stats/2026-05-12-iter-23.5.json
diff --git a/docs/roadmap.md b/docs/roadmap.md
index 94020fe..84fcac6 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -41,27 +41,23 @@ context. Pick the next milestone from P1.)_
 
 ## P1 — Next
 
-- [ ] **\[milestone\]** Post-22 Prelude — ship `Show` / `Eq` / `Ord`
-  with the three total-orderable primitive instances (Int, Bool, Str);
-  rewire `print` through `Show.show`. Float gets `Show` but **not**
-  `Eq` / `Ord` (partial — see Floats milestone). Originally queued
-  as 22b.4 in the typeclass milestone, kept on hold pending demand.
-  - context: JOURNAL 2026-05-09 ("JOURNAL queue"). Floats milestone
-    closed 2026-05-10 — partial-Eq/Ord-for-Float story is documented
-    in DESIGN.md §"Float semantics", so the Prelude can decide
-    what's instanced (Show: yes, Eq/Ord: no for Float).
-  - context: Iter 23.1-23.3 shipped Ordering ADT, Eq / Ord classes,
-    primitive instances on Int / Bool / Str, and runtime helpers
-    (`ail_str_eq` / `compare`). Remaining: polymorphic free fns
-    (`ne` / `lt` / `le` / `gt` / `ge`), `Show` class, `print`
-    rewire. The original Spec-23 draft was retired 2026-05-11
-    because it silently assumed polymorphic free fns are
-    mono-specialised the same way as class methods; that assumption
-    is false today. Re-brainstorm pending — `ailang-grounding-check`
-    (gc.1) will be the gating mechanism on the new draft.
-  - depends on: polymorphic-free-fn mono-specialisation (symmetric
-    to class-method monomorphisation in 22b.3) — not currently
-    ratified by any green test.
+- [x] **\[milestone\]** Post-22 Prelude — Eq/Ord — shipped milestone
+  23 (2026-05-12). `Ordering` ADT, `Eq`/`Ord` classes, primitive
+  instances on Int / Bool / Str, polymorphic free fns
+  `ne`/`lt`/`le`/`gt`/`ge`, runtime `ail_str_eq` + `ail_str_compare`,
+  end-to-end coverage including user-ADT-instance integration. Float
+  has neither instance by design; polymorphic helpers at Float fire
+  Float-aware `NoInstance` per DESIGN.md §"Float semantics".
+
+- [ ] **\[milestone\]** Post-22 Prelude — Show + print rewire — ship
+  `Show` typeclass with `Show Int/Bool/Str/Float` instances; rewire
+  `print` through `Show.show`. Gated on heap-`Str` ABI runtime work
+  (`int_to_str` needs to allocate). Originally queued as 22b.4 in
+  the typeclass milestone, kept on hold pending demand and the
+  heap-`Str` prerequisite.
+  - context: brainstorm 2026-05-12 (iter 23.5 wrap). Heap-`Str` ABI
+    is the load-bearing prerequisite; until it ships, `Show Int`
+    cannot allocate a `Str` to return.
 
 ## P2 — Medium-term
 
@@ -70,7 +66,7 @@ context. Pick the next milestone from P1.)_
   primitive comparators. No commitment; gated on bench re-baselining
   to make sure the indirection doesn't tank latency.
   - context: JOURNAL 2026-05-09
-  - depends on: Post-22 Prelude
+  - depends on: Post-22 Prelude — Eq/Ord (shipped 23.5)
 - [ ] **\[todo\]** `types` / `ctor_index` overlay shape question —
   decide whether the env's two parallel ctor maps should collapse
   into one overlay, or stay split. Surfaced during the
diff --git a/examples/eq_float_noinstance.ail.json b/examples/eq_float_noinstance.ail.json
new file mode 100644
index 0000000..7a77a1e
--- /dev/null
+++ b/examples/eq_float_noinstance.ail.json
@@ -0,0 +1,32 @@
+{
+  "schema": "ailang/v0",
+  "name": "eq_float_noinstance",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "do", "op": "io/print_int",
+        "args": [{
+          "t": "if",
+          "cond": {
+            "t": "app",
+            "fn": { "t": "var", "name": "eq" },
+            "args": [
+              { "t": "lit", "lit": { "kind": "float", "bits": "3ff0000000000000" } },
+              { "t": "lit", "lit": { "kind": "float", "bits": "4000000000000000" } }
+            ]
+          },
+          "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+          "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+        }]
+      }
+    }
+  ]
+}
diff --git a/examples/eq_ord_polymorphic.ail.json b/examples/eq_ord_polymorphic.ail.json
new file mode 100644
index 0000000..dda5963
--- /dev/null
+++ b/examples/eq_ord_polymorphic.ail.json
@@ -0,0 +1,103 @@
+{
+  "schema": "ailang/v0",
+  "name": "eq_ord_polymorphic",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "at_most",
+      "doc": "Composition of prelude `gt` with `not` — semantically equivalent to `le`. Used to exercise polymorphic-helper-over-prelude-fns composition through the unified mono pass.",
+      "type": {
+        "k": "forall",
+        "vars": ["a"],
+        "constraints": [{ "class": "Ord", "type": { "k": "var", "name": "a" } }],
+        "body": {
+          "k": "fn",
+          "params": [
+            { "k": "var", "name": "a" },
+            { "k": "var", "name": "a" }
+          ],
+          "param_modes": ["borrow", "borrow"],
+          "ret": { "k": "con", "name": "Bool" },
+          "effects": []
+        }
+      },
+      "params": ["x", "y"],
+      "body": {
+        "t": "app",
+        "fn": { "t": "var", "name": "not" },
+        "args": [{
+          "t": "app",
+          "fn": { "t": "var", "name": "gt" },
+          "args": [
+            { "t": "var", "name": "x" },
+            { "t": "var", "name": "y" }
+          ]
+        }]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "seq",
+        "lhs": {
+          "t": "do", "op": "io/print_int",
+          "args": [{
+            "t": "if",
+            "cond": {
+              "t": "app",
+              "fn": { "t": "var", "name": "at_most" },
+              "args": [
+                { "t": "lit", "lit": { "kind": "int", "value": 3 } },
+                { "t": "lit", "lit": { "kind": "int", "value": 5 } }
+              ]
+            },
+            "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+            "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+          }]
+        },
+        "rhs": {
+          "t": "seq",
+          "lhs": {
+            "t": "do", "op": "io/print_int",
+            "args": [{
+              "t": "if",
+              "cond": {
+                "t": "app",
+                "fn": { "t": "var", "name": "at_most" },
+                "args": [
+                  { "t": "lit", "lit": { "kind": "bool", "value": true } },
+                  { "t": "lit", "lit": { "kind": "bool", "value": false } }
+                ]
+              },
+              "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+              "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+            }]
+          },
+          "rhs": {
+            "t": "do", "op": "io/print_int",
+            "args": [{
+              "t": "if",
+              "cond": {
+                "t": "app",
+                "fn": { "t": "var", "name": "at_most" },
+                "args": [
+                  { "t": "lit", "lit": { "kind": "str", "value": "abc" } },
+                  { "t": "lit", "lit": { "kind": "str", "value": "abd" } }
+                ]
+              },
+              "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+              "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+            }]
+          }
+        }
+      }
+    }
+  ]
+}
diff --git a/examples/eq_ord_user_adt.ail.json b/examples/eq_ord_user_adt.ail.json
new file mode 100644
index 0000000..1ff64c8
--- /dev/null
+++ b/examples/eq_ord_user_adt.ail.json
@@ -0,0 +1,156 @@
+{
+  "schema": "ailang/v0",
+  "name": "eq_ord_user_adt",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "type",
+      "name": "IntBox",
+      "vars": [],
+      "doc": "A one-field box around an Int, used to demonstrate that the unified mono pass synthesises eq__IntBox from a user-written instance, not from the primitive == operator.",
+      "ctors": [
+        { "name": "MkIntBox", "fields": [{ "k": "con", "name": "Int" }] }
+      ]
+    },
+    {
+      "kind": "instance",
+      "class": "Eq",
+      "type": { "k": "con", "name": "IntBox" },
+      "doc": "Eq IntBox by structural unwrap of the inner Int.",
+      "methods": [
+        {
+          "name": "eq",
+          "body": {
+            "t": "lam",
+            "params": ["a", "b"],
+            "paramTypes": [
+              { "k": "con", "name": "IntBox" },
+              { "k": "con", "name": "IntBox" }
+            ],
+            "retType": { "k": "con", "name": "Bool" },
+            "body": {
+              "t": "match",
+              "scrutinee": { "t": "var", "name": "a" },
+              "arms": [{
+                "pat": { "p": "ctor", "ctor": "MkIntBox", "fields": [{ "p": "var", "name": "ai" }] },
+                "body": {
+                  "t": "match",
+                  "scrutinee": { "t": "var", "name": "b" },
+                  "arms": [{
+                    "pat": { "p": "ctor", "ctor": "MkIntBox", "fields": [{ "p": "var", "name": "bi" }] },
+                    "body": {
+                      "t": "app",
+                      "fn": { "t": "var", "name": "==" },
+                      "args": [
+                        { "t": "var", "name": "ai" },
+                        { "t": "var", "name": "bi" }
+                      ]
+                    }
+                  }]
+                }
+              }]
+            }
+          }
+        }
+      ]
+    },
+    {
+      "kind": "instance",
+      "class": "Ord",
+      "type": { "k": "con", "name": "IntBox" },
+      "doc": "Ord IntBox by delegating to Int's compare on the inner field.",
+      "methods": [
+        {
+          "name": "compare",
+          "body": {
+            "t": "lam",
+            "params": ["a", "b"],
+            "paramTypes": [
+              { "k": "con", "name": "IntBox" },
+              { "k": "con", "name": "IntBox" }
+            ],
+            "retType": { "k": "con", "name": "prelude.Ordering" },
+            "body": {
+              "t": "match",
+              "scrutinee": { "t": "var", "name": "a" },
+              "arms": [{
+                "pat": { "p": "ctor", "ctor": "MkIntBox", "fields": [{ "p": "var", "name": "ai" }] },
+                "body": {
+                  "t": "match",
+                  "scrutinee": { "t": "var", "name": "b" },
+                  "arms": [{
+                    "pat": { "p": "ctor", "ctor": "MkIntBox", "fields": [{ "p": "var", "name": "bi" }] },
+                    "body": {
+                      "t": "app",
+                      "fn": { "t": "var", "name": "compare" },
+                      "args": [
+                        { "t": "var", "name": "ai" },
+                        { "t": "var", "name": "bi" }
+                      ]
+                    }
+                  }]
+                }
+              }]
+            }
+          }
+        }
+      ]
+    },
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "seq",
+        "lhs": {
+          "t": "do", "op": "io/print_int",
+          "args": [{
+            "t": "if",
+            "cond": {
+              "t": "app",
+              "fn": { "t": "var", "name": "eq" },
+              "args": [
+                {
+                  "t": "ctor", "type": "IntBox", "ctor": "MkIntBox",
+                  "args": [{ "t": "lit", "lit": { "kind": "int", "value": 3 } }]
+                },
+                {
+                  "t": "ctor", "type": "IntBox", "ctor": "MkIntBox",
+                  "args": [{ "t": "lit", "lit": { "kind": "int", "value": 3 } }]
+                }
+              ]
+            },
+            "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+            "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+          }]
+        },
+        "rhs": {
+          "t": "do", "op": "io/print_int",
+          "args": [{
+            "t": "if",
+            "cond": {
+              "t": "app",
+              "fn": { "t": "var", "name": "eq" },
+              "args": [
+                {
+                  "t": "ctor", "type": "IntBox", "ctor": "MkIntBox",
+                  "args": [{ "t": "lit", "lit": { "kind": "int", "value": 3 } }]
+                },
+                {
+                  "t": "ctor", "type": "IntBox", "ctor": "MkIntBox",
+                  "args": [{ "t": "lit", "lit": { "kind": "int", "value": 5 } }]
+                }
+              ]
+            },
+            "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+            "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+          }]
+        }
+      }
+    }
+  ]
+}
diff --git a/examples/ge_at_int_smoke.ail.json b/examples/ge_at_int_smoke.ail.json
new file mode 100644
index 0000000..caa0589
--- /dev/null
+++ b/examples/ge_at_int_smoke.ail.json
@@ -0,0 +1,32 @@
+{
+  "schema": "ailang/v0",
+  "name": "ge_at_int_smoke",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "do", "op": "io/print_int",
+        "args": [{
+          "t": "if",
+          "cond": {
+            "t": "app",
+            "fn": { "t": "var", "name": "ge" },
+            "args": [
+              { "t": "lit", "lit": { "kind": "int", "value": 3 } },
+              { "t": "lit", "lit": { "kind": "int", "value": 5 } }
+            ]
+          },
+          "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+          "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+        }]
+      }
+    }
+  ]
+}
diff --git a/examples/gt_at_bool_smoke.ail.json b/examples/gt_at_bool_smoke.ail.json
new file mode 100644
index 0000000..f85f5f0
--- /dev/null
+++ b/examples/gt_at_bool_smoke.ail.json
@@ -0,0 +1,32 @@
+{
+  "schema": "ailang/v0",
+  "name": "gt_at_bool_smoke",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "do", "op": "io/print_int",
+        "args": [{
+          "t": "if",
+          "cond": {
+            "t": "app",
+            "fn": { "t": "var", "name": "gt" },
+            "args": [
+              { "t": "lit", "lit": { "kind": "bool", "value": true } },
+              { "t": "lit", "lit": { "kind": "bool", "value": false } }
+            ]
+          },
+          "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+          "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+        }]
+      }
+    }
+  ]
+}
diff --git a/examples/le_at_str_smoke.ail.json b/examples/le_at_str_smoke.ail.json
new file mode 100644
index 0000000..785dc32
--- /dev/null
+++ b/examples/le_at_str_smoke.ail.json
@@ -0,0 +1,32 @@
+{
+  "schema": "ailang/v0",
+  "name": "le_at_str_smoke",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "do", "op": "io/print_int",
+        "args": [{
+          "t": "if",
+          "cond": {
+            "t": "app",
+            "fn": { "t": "var", "name": "le" },
+            "args": [
+              { "t": "lit", "lit": { "kind": "str", "value": "abc" } },
+              { "t": "lit", "lit": { "kind": "str", "value": "abd" } }
+            ]
+          },
+          "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+          "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+        }]
+      }
+    }
+  ]
+}
diff --git a/examples/lt_at_int_smoke.ail.json b/examples/lt_at_int_smoke.ail.json
new file mode 100644
index 0000000..e1728e0
--- /dev/null
+++ b/examples/lt_at_int_smoke.ail.json
@@ -0,0 +1,32 @@
+{
+  "schema": "ailang/v0",
+  "name": "lt_at_int_smoke",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "do", "op": "io/print_int",
+        "args": [{
+          "t": "if",
+          "cond": {
+            "t": "app",
+            "fn": { "t": "var", "name": "lt" },
+            "args": [
+              { "t": "lit", "lit": { "kind": "int", "value": 3 } },
+              { "t": "lit", "lit": { "kind": "int", "value": 5 } }
+            ]
+          },
+          "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+          "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+        }]
+      }
+    }
+  ]
+}
diff --git a/examples/ne_at_int_smoke.ail.json b/examples/ne_at_int_smoke.ail.json
new file mode 100644
index 0000000..3223fca
--- /dev/null
+++ b/examples/ne_at_int_smoke.ail.json
@@ -0,0 +1,32 @@
+{
+  "schema": "ailang/v0",
+  "name": "ne_at_int_smoke",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "do", "op": "io/print_int",
+        "args": [{
+          "t": "if",
+          "cond": {
+            "t": "app",
+            "fn": { "t": "var", "name": "ne" },
+            "args": [
+              { "t": "lit", "lit": { "kind": "int", "value": 3 } },
+              { "t": "lit", "lit": { "kind": "int", "value": 5 } }
+            ]
+          },
+          "then": { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+          "else": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+        }]
+      }
+    }
+  ]
+}
diff --git a/examples/prelude.ail.json b/examples/prelude.ail.json
index 9808c72..dae432e 100644
--- a/examples/prelude.ail.json
+++ b/examples/prelude.ail.json
@@ -218,6 +218,207 @@
           }
         }
       ]
+    },
+    {
+      "kind": "fn",
+      "name": "ne",
+      "doc": "Polymorphic disequality. `ne x y` ≡ not (eq x y). Ships in milestone 23 as the Eq-class free helper.",
+      "type": {
+        "k": "forall",
+        "vars": ["a"],
+        "constraints": [{ "class": "Eq", "type": { "k": "var", "name": "a" } }],
+        "body": {
+          "k": "fn",
+          "params": [
+            { "k": "var", "name": "a" },
+            { "k": "var", "name": "a" }
+          ],
+          "param_modes": ["borrow", "borrow"],
+          "ret": { "k": "con", "name": "Bool" },
+          "effects": []
+        }
+      },
+      "params": ["x", "y"],
+      "body": {
+        "t": "app",
+        "fn": { "t": "var", "name": "not" },
+        "args": [{
+          "t": "app",
+          "fn": { "t": "var", "name": "eq" },
+          "args": [
+            { "t": "var", "name": "x" },
+            { "t": "var", "name": "y" }
+          ]
+        }]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "lt",
+      "doc": "Polymorphic strict-less-than. `lt x y` ≡ case compare x y of LT -> True; _ -> False. Ships in milestone 23 as the Ord-class free helper.",
+      "type": {
+        "k": "forall",
+        "vars": ["a"],
+        "constraints": [{ "class": "Ord", "type": { "k": "var", "name": "a" } }],
+        "body": {
+          "k": "fn",
+          "params": [
+            { "k": "var", "name": "a" },
+            { "k": "var", "name": "a" }
+          ],
+          "param_modes": ["borrow", "borrow"],
+          "ret": { "k": "con", "name": "Bool" },
+          "effects": []
+        }
+      },
+      "params": ["x", "y"],
+      "body": {
+        "t": "match",
+        "scrutinee": {
+          "t": "app",
+          "fn": { "t": "var", "name": "compare" },
+          "args": [
+            { "t": "var", "name": "x" },
+            { "t": "var", "name": "y" }
+          ]
+        },
+        "arms": [
+          {
+            "pat": { "p": "ctor", "ctor": "LT", "fields": [] },
+            "body": { "t": "lit", "lit": { "kind": "bool", "value": true } }
+          },
+          {
+            "pat": { "p": "wild" },
+            "body": { "t": "lit", "lit": { "kind": "bool", "value": false } }
+          }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "le",
+      "doc": "Polymorphic less-than-or-equal. `le x y` ≡ case compare x y of GT -> False; _ -> True. Ships in milestone 23 as the Ord-class free helper.",
+      "type": {
+        "k": "forall",
+        "vars": ["a"],
+        "constraints": [{ "class": "Ord", "type": { "k": "var", "name": "a" } }],
+        "body": {
+          "k": "fn",
+          "params": [
+            { "k": "var", "name": "a" },
+            { "k": "var", "name": "a" }
+          ],
+          "param_modes": ["borrow", "borrow"],
+          "ret": { "k": "con", "name": "Bool" },
+          "effects": []
+        }
+      },
+      "params": ["x", "y"],
+      "body": {
+        "t": "match",
+        "scrutinee": {
+          "t": "app",
+          "fn": { "t": "var", "name": "compare" },
+          "args": [
+            { "t": "var", "name": "x" },
+            { "t": "var", "name": "y" }
+          ]
+        },
+        "arms": [
+          {
+            "pat": { "p": "ctor", "ctor": "GT", "fields": [] },
+            "body": { "t": "lit", "lit": { "kind": "bool", "value": false } }
+          },
+          {
+            "pat": { "p": "wild" },
+            "body": { "t": "lit", "lit": { "kind": "bool", "value": true } }
+          }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "gt",
+      "doc": "Polymorphic strict-greater-than. `gt x y` ≡ case compare x y of GT -> True; _ -> False. Ships in milestone 23 as the Ord-class free helper.",
+      "type": {
+        "k": "forall",
+        "vars": ["a"],
+        "constraints": [{ "class": "Ord", "type": { "k": "var", "name": "a" } }],
+        "body": {
+          "k": "fn",
+          "params": [
+            { "k": "var", "name": "a" },
+            { "k": "var", "name": "a" }
+          ],
+          "param_modes": ["borrow", "borrow"],
+          "ret": { "k": "con", "name": "Bool" },
+          "effects": []
+        }
+      },
+      "params": ["x", "y"],
+      "body": {
+        "t": "match",
+        "scrutinee": {
+          "t": "app",
+          "fn": { "t": "var", "name": "compare" },
+          "args": [
+            { "t": "var", "name": "x" },
+            { "t": "var", "name": "y" }
+          ]
+        },
+        "arms": [
+          {
+            "pat": { "p": "ctor", "ctor": "GT", "fields": [] },
+            "body": { "t": "lit", "lit": { "kind": "bool", "value": true } }
+          },
+          {
+            "pat": { "p": "wild" },
+            "body": { "t": "lit", "lit": { "kind": "bool", "value": false } }
+          }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "ge",
+      "doc": "Polymorphic greater-than-or-equal. `ge x y` ≡ case compare x y of LT -> False; _ -> True. Ships in milestone 23 as the Ord-class free helper.",
+      "type": {
+        "k": "forall",
+        "vars": ["a"],
+        "constraints": [{ "class": "Ord", "type": { "k": "var", "name": "a" } }],
+        "body": {
+          "k": "fn",
+          "params": [
+            { "k": "var", "name": "a" },
+            { "k": "var", "name": "a" }
+          ],
+          "param_modes": ["borrow", "borrow"],
+          "ret": { "k": "con", "name": "Bool" },
+          "effects": []
+        }
+      },
+      "params": ["x", "y"],
+      "body": {
+        "t": "match",
+        "scrutinee": {
+          "t": "app",
+          "fn": { "t": "var", "name": "compare" },
+          "args": [
+            { "t": "var", "name": "x" },
+            { "t": "var", "name": "y" }
+          ]
+        },
+        "arms": [
+          {
+            "pat": { "p": "ctor", "ctor": "LT", "fields": [] },
+            "body": { "t": "lit", "lit": { "kind": "bool", "value": false } }
+          },
+          {
+            "pat": { "p": "wild" },
+            "body": { "t": "lit", "lit": { "kind": "bool", "value": true } }
+          }
+        ]
+      }
     }
   ]
 }
diff --git a/examples/test_22b1_missing_method.ail.json b/examples/test_22b1_missing_method.ail.json
index 83bbd97..2eaf7f8 100644
--- a/examples/test_22b1_missing_method.ail.json
+++ b/examples/test_22b1_missing_method.ail.json
@@ -21,7 +21,7 @@
           }
         },
         {
-          "name": "ne",
+          "name": "tne",
           "type": {
             "k": "fn",
             "params": [
@@ -40,7 +40,7 @@
       "type": { "k": "con", "name": "Int" },
       "methods": [
         {
-          "name": "ne",
+          "name": "tne",
           "body": { "t": "lit", "lit": { "kind": "bool", "value": false } }
         }
       ]