diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md
index 1020e26..05b62a5 100644
--- a/docs/JOURNAL.md
+++ b/docs/JOURNAL.md
@@ -13860,3 +13860,87 @@ The roadmap entry "Architect-iron-law standing-grep extension"
 under P2 is closed by this iteration. Future lockstep pairings, as
 they surface in JOURNAL entries, can extend the table inline
 without further iteration ceremony.
+
+## 2026-05-10 — Iteration 23.1: Ordering ADT + prelude skeleton + auto-load
+
+First iteration of milestone 23 (Eq/Ord Prelude). Lays the
+groundwork — no classes or instances ship yet — by establishing
+the prelude module as a real loaded module that every workspace
+implicitly contains, with bare-name resolution for its ctors via
+the existing import-fallback machinery (Iter 15a,
+`ailang-check/src/lib.rs::Pattern::Ctor` resolution).
+
+Three mechanisms compose:
+
+1. **Embedded prelude.** `examples/prelude.ail.json` is the
+   LLM-author-readable source; the loader embeds it via
+   `include_str!` at compile time. No runtime file IO, no CWD
+   dependency, no fixture-not-found failure mode.
+2. **Loader injection.** `load_workspace` inserts the prelude
+   into `ws.modules` after the user's import DFS finishes and
+   before `validate_classdefs` / `build_registry`, so the
+   workspace-wide registry passes see it like any other module.
+   A user module trying to claim the reserved name `prelude`
+   fails fast with `WorkspaceLoadError::ReservedModuleName`.
+3. **Implicit import.** `build_check_env` adds `prelude → prelude`
+   to every non-prelude module's `module_imports` map; the
+   parallel per-module overlay in `check_in_workspace` does the
+   same for the active `env.imports` table. The existing
+   bare-ctor fallback in `Pattern::Ctor` resolution finds prelude
+   ctors through this path, so the user writes `LT` instead of
+   `prelude.LT`.
+
+Verified end-to-end through `examples/ordering_match.ail.json`
+(pattern-matches a hard-coded `LT` value, prints `1`). Coverage
+spans the loader (`loads_workspace_auto_injects_prelude` +
+collision via `user_module_named_prelude_is_rejected`), the
+typechecker (`user_module_can_pattern_match_on_prelude_ordering_bare`),
+the new error path (`cross_module_term_ctor_ambiguous_type_errors`),
+and the full pipeline (`ordering_match_via_prelude_prints_1`
+through `cargo test -p ail`).
+
+**Scope expansion authorised mid-iter.** Task 3 surfaced a
+real asymmetry: `Pattern::Ctor` had Iter-15a imports-fallback
+for bare ctor names, but `Term::Ctor` synth resolved bare
+`type_name` via `env.types.get()` only — no fallback. The
+spec's bare-name goal for prelude ctors required closing that
+gap. Added local-first-then-imports-fallback to `Term::Ctor`
+synth (`crates/ailang-check/src/lib.rs:1944-2076`), plus
+`CheckError::AmbiguousType` mirroring `AmbiguousCtor`. The
+codegen side (`crates/ailang-codegen/src/lib.rs::lookup_ctor_by_type`)
+needed the same fallback in Task 4 — the typechecker accepts
+the bare reference but codegen's ctor-resolution path was
+strictly local. Both touched as part of the iter.
+
+**Three-site lockstep flagged.** The fix-pattern is now a
+three-site invariant: `Pattern::Ctor` imports-fallback (Iter 15a)
+↔ `Term::Ctor` typecheck imports-fallback (Iter 23.1.3) ↔
+`Term::Ctor` codegen imports-fallback (Iter 23.1.4). A new arm
+in any one site without the matching extension in the other two
+risks the silent-divergence failure mode the architect-iron-law
+extension just shipped to catch. Candidate for adding to the
+lockstep table in a future architect-iron-law iter, alongside
+the two already there (`lower_app ↔ is_static_callee`,
+`Pattern::Lit::Float reject ↔ pre_desugar_validation`).
+
+Out of scope for this iter (covered by later 23.x):
+- Eq / Ord class definitions (23.2 / 23.3).
+- Free top-level utility functions `ne` / `lt` / `le` / `gt` / `ge` (23.4).
+- Float-NoInstance diagnostic + DESIGN.md amendment (23.5).
+
+Per-task commits:
+
+- `cce3d97` iter 23.1.1: examples/prelude.ail.json — Ordering ADT skeleton
+- `3742583` iter 23.1.2: load_workspace auto-injects prelude module
+- `927f7ea` iter 23.1.2 fixup: align workspace-root idiom + add collision test for ReservedModuleName
+- `842df38` iter 23.1.3: implicit prelude import + symmetric bare-type-name imports-fallback in Term::Ctor synth
+- `24af13e` iter 23.1.3 fixup: cover AmbiguousType branch with cross-module test
+- `47d95d0` iter 23.1.3 fixup: clarify imports-fallback anchor + comment on env.imports vs env.module_imports duplication
+- `aace5e3` iter 23.1.4: E2E fixture — bare LT match via implicit prelude import
+- `1f24437` iter 23.1.4 fixup: local-hit with mismatching type_name falls through to imports-fallback
+
+Workspace at iter-23.1 close: 76 ailang-check tests + 5 env-pin
+tests + the new ail-crate E2E + the new workspace-loader tests,
+all green. Cross-language and the three regression scripts not
+re-run for this iter (no codegen-shape change to the existing
+fixtures); they'll run at milestone-23 close.