diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index 2757758..3cb24c7 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -1298,9 +1298,14 @@ fn check_in_workspace(
         import_map.insert(key, imp.module.clone());
     }
     // Iter 23.1: the prelude module is implicitly imported into
-    // every non-prelude module's body-check env. Mirrors the
-    // workspace-flat overlay in `build_check_env`. The prelude
-    // itself does not import itself.
+    // every non-prelude module's body-check env. The wiring here
+    // populates `env.imports` (the active per-module table the
+    // body-check pass reads); the sibling block in `build_check_env`
+    // populates `env.module_imports` (the workspace-wide table
+    // referenced when resolving qualified names across modules).
+    // Both fields need the prelude-injection rule applied, and they
+    // are populated from different code paths — hence the apparent
+    // duplication. The prelude itself does not import itself.
     if m.name != "prelude" {
         import_map
             .entry("prelude".to_string())
@@ -1978,8 +1983,10 @@ pub(crate) fn synth(
             } else {
                 // Iter 23.1.3: bare type-name not present locally —
                 // scan imported modules for a type by this name.
-                // Symmetric to `Pattern::Ctor`'s fallback at this
-                // file's ~lib.rs:2453; required so an LLM author can
+                // Symmetric to the Iter 15a imports-fallback applied
+                // to `Pattern::Ctor` resolution (search this file for
+                // "Iter 15a: try local ctor_index first" to find the
+                // canonical comment). Required so an LLM author can
                 // write `(con Ordering LT)` against a prelude type
                 // without qualifying it as `prelude.Ordering`. The
                 // result `Type::Con` carries the qualified name so