diff --git a/crates/ail/tests/prelude_eq_alwaysinline_ir_pin.rs b/crates/ail/tests/prelude_eq_alwaysinline_ir_pin.rs
index 38ee3d1..c546a7b 100644
--- a/crates/ail/tests/prelude_eq_alwaysinline_ir_pin.rs
+++ b/crates/ail/tests/prelude_eq_alwaysinline_ir_pin.rs
@@ -14,13 +14,15 @@ use std::process::Command;
 fn prelude_eq_int_carries_alwaysinline_attribute_in_emitted_ir() {
     let manifest_dir = env!("CARGO_MANIFEST_DIR");
     let repo_root = PathBuf::from(manifest_dir).join("../..");
-    // Use a fixture that already invokes the class-method `eq` path
-    // (so prelude.eq__Int gets monomorphised into the emitted IR).
-    // `eq_demo.ail` calls `(app == …)` directly which today uses the
-    // `lower_eq` direct-emit short-circuit and never references the
-    // prelude eq__Int symbol; `eq_ord_user_adt.ail` calls `(app eq …)`
-    // on an IntBox whose user instance internally calls `(app eq ai bi)`
-    // on Int, monomorphising `eq__Int` into the IR.
+    // Use a fixture that invokes the class-method `eq` path so
+    // `prelude.eq__Int` gets monomorphised into the emitted IR.
+    // `eq_ord_user_adt.ail` calls `(app eq …)` on an IntBox whose
+    // user instance body internally calls `(app eq ai bi)` on Int —
+    // class-dispatch resolves both the outer (Eq IntBox) and inner
+    // (Eq Int) calls. The inner Eq Int path is the one we pin here:
+    // its `define i1 @ail_prelude_eq__Int(...) alwaysinline { ... }`
+    // must carry `alwaysinline` so the call folds to a single
+    // `icmp eq i64` at every use site under -O0.
     let fixture = repo_root.join("examples/eq_ord_user_adt.ail");
 
     let out = Command::new(env!("CARGO_BIN_EXE_ail"))
diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs
index 65addc6..fdc7744 100644
--- a/crates/ailang-codegen/src/lib.rs
+++ b/crates/ailang-codegen/src/lib.rs
@@ -2774,19 +2774,30 @@ impl<'a> Emitter<'a> {
     /// top-level fn gets so it is reachable as a `Term::Var` value).
     /// `Ok(false)` lets `emit_fn` continue with normal body lowering.
     ///
-    /// Currently inhabited arms: `eq__Str` (ships in 23.2.2) and
-    /// `compare__Int`, `compare__Bool`, `compare__Str` (this iter
-    /// 23.3). The two eq Int/Bool primitives (`eq__Int`, `eq__Bool`)
-    /// ride the natural `lower_eq` dispatch via their lambda body
-    /// `(== x y)` and do not need a hand-rolled body. The three
-    /// `compare` arms must be hand-rolled because there is no
-    /// type-polymorphic primitive that returns an Ordering ADT
-    /// value (Decision: `builtin_binop_typed` covers Int and Float
-    /// only — Bool is missing — so a surface-level
-    /// `if x < y { LT } else if x == y { EQ } else { GT }` body
-    /// would fail at codegen for `compare__Bool`). Hand-rolling all
-    /// three keeps the family consistent and the IR shape
-    /// predictable.
+    /// Currently inhabited arms (post-operator-routing-eq-ord
+    /// milestone): the `Eq` instance bodies `eq__Int`, `eq__Bool`,
+    /// `eq__Str`, `eq__Unit`; the `Ord` instance bodies `compare__Int`,
+    /// `compare__Bool`, `compare__Str`; the Int-direct short-circuits
+    /// for the Ord-class free helpers `lt__Int`, `le__Int`, `gt__Int`,
+    /// `ge__Int`, `ne__Int`; and the six Float-named comparison fns
+    /// `float_eq`, `float_ne`, `float_lt`, `float_le`, `float_gt`,
+    /// `float_ge`. Fourteen arms total; every arm pairs with an
+    /// `alwaysinline` attribute on the generated `define` line (via
+    /// `intercept_emit_wants_alwaysinline`) so the call folds to a
+    /// single instruction at every use site under -O0 as well as
+    /// -O2. The eq/compare/Float arms exist because there is no
+    /// type-polymorphic builtin that would lower to the right
+    /// per-type instruction (`lower_eq` was deleted in the
+    /// operator-routing-eq-ord milestone — `==` is no longer a
+    /// language identifier; the class-method dispatch through
+    /// `prelude.Eq` / `prelude.Ord` is the only path). The `lt/le/gt/
+    /// ge/ne` Int-direct arms exist as an asymmetric optimization
+    /// (Int-only) — without them the source-level body of `lt`/etc.
+    /// allocates an `Ordering` ctor per call via the
+    /// `compare__Int` → `match` path, which surfaces as a
+    /// `bench_closure_chain` regression. See
+    /// `design/contracts/prelude-classes.md` for the full surface
+    /// and the Int-only asymmetry rationale.
     fn try_emit_primitive_instance_body(
         &mut self,
         fn_name: &str,
diff --git a/design/contracts/prelude-classes.md b/design/contracts/prelude-classes.md
index ea777aa..41749fd 100644
--- a/design/contracts/prelude-classes.md
+++ b/design/contracts/prelude-classes.md
@@ -14,6 +14,26 @@ them with single-instruction bodies (`icmp eq i64` for `eq__Int`,
 `LT`/`EQ`/`GT` for `compare__T`) and attaches `alwaysinline` so
 the call folds to the single instruction at every use site.
 
+The five Ord-class free helpers (`ne`/`lt`/`le`/`gt`/`ge`) have
+source-level bodies that route through `eq` / `compare` plus
+`match` over `Ordering` — written that way so the surface form is
+LLM-natural and so user-ADT instances of `Eq`/`Ord` automatically
+pick up working helpers without any per-type opt-in. At Int the
+codegen intercept short-circuits this indirection: `lt__Int`,
+`le__Int`, `gt__Int`, `ge__Int`, and `ne__Int` are intercept-
+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
+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.
+
 Float has neither `Eq` nor `Ord` instance per [Float semantics](
 float-semantics.md); a polymorphic helper invoked at Float fires
 `NoInstance` at typecheck with a Float-aware diagnostic that names
diff --git a/design/contracts/typeclasses.md b/design/contracts/typeclasses.md
index 6ac2b66..45e8c86 100644
--- a/design/contracts/typeclasses.md
+++ b/design/contracts/typeclasses.md
@@ -135,15 +135,39 @@ Three invariants make this work:
    `unknown variable: show` from codegen instead of the right
    typecheck-phase NoInstance Show.
 
-The three invariants are lockstep partners: invariant (1) creates the
+4. **Bare-prelude-fn calls resolve via implicit-prelude-import at
+   typecheck AND at codegen.** A user-module source-level call
+   `(app float_eq 1.5 1.5)` writes the bare name `float_eq`, not
+   the qualified form `prelude.float_eq`. The typechecker resolves
+   this via the auto-injected prelude import (see invariant (2)
+   for the one-way auto-injection rule); codegen's
+   `lower_app::resolve_callee` + `is_static_callee` + `resolve_top_level_fn`
+   each carry a parallel prelude-fallback: when the bare name does
+   not resolve in the caller-module's symbol table, fall back to
+   `prelude.<name>`. This is the source-level counterpart to
+   invariant (2)'s post-mono fallback — both make the implicit-
+   prelude-import a workspace invariant rather than a typechecker-
+   only feature. The fallback is load-bearing for the surface
+   `(app float_eq …)` / `(app float_lt …)` / etc. of the
+   operator-routing-eq-ord milestone; without it the LLM-author
+   must write `prelude.float_eq` explicitly, which is exactly the
+   syntactic noise the implicit import exists to eliminate.
+
+The four invariants are lockstep partners: invariant (1) creates the
 cross-module reference, invariant (2) makes codegen able to resolve
-it, invariant (3) makes the typecheck-time discharge fire correctly
-when no instance exists. A future refactor that loosens any one of
-the three breaks the user-ADT trajectory; the test pins at
+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
 `crates/ail/tests/codegen_import_map_fallback_pin.rs` (invariant 2),
 `crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` (invariant 3
-+ lockstep), and the existing `crates/ail/tests/show_user_adt`
-fixture (full trajectory) collectively protect the contract.
++ lockstep), `crates/ail/tests/float_compare_smoke_e2e.rs`
+(invariant 4 — drives `(app float_eq …)` end-to-end across the
+implicit-prelude-import boundary), and the existing
+`crates/ail/tests/show_user_adt` fixture (full trajectory)
+collectively protect the contract.
 
 ## Defaults and superclasses