diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs
index dcfe130..7d6f110 100644
--- a/crates/ailang-prose/src/lib.rs
+++ b/crates/ailang-prose/src/lib.rs
@@ -54,9 +54,16 @@ fn write_module(out: &mut String, m: &Module) {
         }
     }
 
+    // Ct.4.3: the file's own module name is the owner-qualifier that
+    // the prose surface trims when it appears on intra-module
+    // `Type::Con.name`. Cross-module qualifiers (any other owner)
+    // round-trip verbatim. Threaded through every recursive write_*
+    // that can reach a `Type::Con`.
+    let owning_module = m.name.as_str();
+
     for def in &m.defs {
         out.push('\n');
-        write_def(out, def, 0);
+        write_def(out, def, 0, owning_module);
         out.push('\n');
     }
 }
@@ -72,13 +79,13 @@ fn write_import(out: &mut String, imp: &Import) {
 
 // ---- defs -----------------------------------------------------------------
 
-fn write_def(out: &mut String, def: &Def, level: usize) {
+fn write_def(out: &mut String, def: &Def, level: usize, owning_module: &str) {
     match def {
-        Def::Type(td) => write_type_def(out, td, level),
-        Def::Fn(fd) => write_fn_def(out, fd, level),
-        Def::Const(cd) => write_const_def(out, cd, level),
-        Def::Class(c) => write_class_def(out, c, level),
-        Def::Instance(i) => write_instance_def(out, i, level),
+        Def::Type(td) => write_type_def(out, td, level, owning_module),
+        Def::Fn(fd) => write_fn_def(out, fd, level, owning_module),
+        Def::Const(cd) => write_const_def(out, cd, level, owning_module),
+        Def::Class(c) => write_class_def(out, c, level, owning_module),
+        Def::Instance(i) => write_instance_def(out, i, level, owning_module),
     }
 }
 
@@ -184,7 +191,7 @@ fn wrap_words(piece: &str, budget: usize) -> Vec<String> {
     out
 }
 
-fn write_type_def(out: &mut String, td: &TypeDef, level: usize) {
+fn write_type_def(out: &mut String, td: &TypeDef, level: usize, owning_module: &str) {
     write_doc(out, &td.doc, level);
     indent(out, level);
     out.push_str("data ");
@@ -204,14 +211,14 @@ fn write_type_def(out: &mut String, td: &TypeDef, level: usize) {
         if i > 0 {
             out.push_str(" | ");
         }
-        write_ctor(out, c);
+        write_ctor(out, c, owning_module);
     }
     if td.drop_iterative {
         out.push_str(" with drop-iterative");
     }
 }
 
-fn write_ctor(out: &mut String, c: &Ctor) {
+fn write_ctor(out: &mut String, c: &Ctor, owning_module: &str) {
     out.push_str(&c.name);
     if !c.fields.is_empty() {
         out.push('(');
@@ -219,13 +226,13 @@ fn write_ctor(out: &mut String, c: &Ctor) {
             if i > 0 {
                 out.push_str(", ");
             }
-            write_type(out, f);
+            write_type(out, f, owning_module);
         }
         out.push(')');
     }
 }
 
-fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) {
+fn write_fn_def(out: &mut String, fd: &FnDef, level: usize, owning_module: &str) {
     // Iter 19b: render `suppress` entries as `// @suppress <code>: <reason>`
     // comment lines **above** the doc string. They are contract metadata
     // that the LLM-reader needs to see to understand why an annotation
@@ -263,7 +270,7 @@ fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) {
                 }
                 out.push_str(&c.class);
                 out.push(' ');
-                write_type(out, &c.type_);
+                write_type(out, &c.type_, owning_module);
             }
         }
         out.push('\n');
@@ -293,10 +300,10 @@ fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) {
                 .get(i)
                 .copied()
                 .unwrap_or(ParamMode::Implicit);
-            write_mode_type(out, ty, mode);
+            write_mode_type(out, ty, mode, owning_module);
         }
         out.push_str(") -> ");
-        write_mode_type(out, ret, *ret_mode);
+        write_mode_type(out, ret, *ret_mode, owning_module);
         if !effects.is_empty() {
             out.push_str(" with ");
             // Stable order: as written in the AST. Effects are
@@ -314,30 +321,30 @@ fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) {
         // nothing crashes; this path is unreachable for typechecked
         // input.
         out.push_str(") -> ");
-        write_type(out, fn_ty);
+        write_type(out, fn_ty, owning_module);
     }
     out.push_str(" {\n");
     indent(out, level + 1);
-    write_term(out, &fd.body, level + 1);
+    write_term(out, &fd.body, level + 1, owning_module);
     out.push('\n');
     indent(out, level);
     out.push('}');
 }
 
-fn write_const_def(out: &mut String, cd: &ConstDef, level: usize) {
+fn write_const_def(out: &mut String, cd: &ConstDef, level: usize, owning_module: &str) {
     write_doc(out, &cd.doc, level);
     indent(out, level);
     out.push_str("const ");
     out.push_str(&cd.name);
     out.push_str(": ");
-    write_type(out, &cd.ty);
+    write_type(out, &cd.ty, owning_module);
     out.push_str(" = ");
-    write_term(out, &cd.value, level);
+    write_term(out, &cd.value, level, owning_module);
 }
 
 /// Render a class declaration in Rust-flavoured Form-B:
 /// `class Name a [extends Super] { <methods> }`.
-fn write_class_def(out: &mut String, c: &ClassDef, level: usize) {
+fn write_class_def(out: &mut String, c: &ClassDef, level: usize, owning_module: &str) {
     write_doc(out, &c.doc, level);
     indent(out, level);
     out.push_str("class ");
@@ -350,7 +357,7 @@ fn write_class_def(out: &mut String, c: &ClassDef, level: usize) {
     }
     out.push_str(" {\n");
     for m in &c.methods {
-        write_class_method(out, m, level + 1);
+        write_class_method(out, m, level + 1, owning_module);
     }
     indent(out, level);
     out.push('}');
@@ -359,7 +366,7 @@ fn write_class_def(out: &mut String, c: &ClassDef, level: usize) {
 /// Render one method line of a class: signature plus optional
 /// `default { <body> }`. Class methods carry no parameter names
 /// in the AST, so slots are named `x`, `x1`, ….
-fn write_class_method(out: &mut String, m: &ClassMethod, level: usize) {
+fn write_class_method(out: &mut String, m: &ClassMethod, level: usize, owning_module: &str) {
     indent(out, level);
     out.push_str("fn ");
     out.push_str(&m.name);
@@ -379,10 +386,10 @@ fn write_class_method(out: &mut String, m: &ClassMethod, level: usize) {
             }
             out.push_str(": ");
             let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
-            write_mode_type(out, p, mode);
+            write_mode_type(out, p, mode, owning_module);
         }
         out.push_str(") -> ");
-        write_mode_type(out, ret, *ret_mode);
+        write_mode_type(out, ret, *ret_mode, owning_module);
         if !effects.is_empty() {
             out.push_str(" with ");
             for (i, e) in effects.iter().enumerate() {
@@ -397,12 +404,12 @@ fn write_class_method(out: &mut String, m: &ClassMethod, level: usize) {
         // bare type so nothing crashes; this path is unreachable for
         // typechecked input.
         out.push_str(") -> ");
-        write_type(out, &m.ty);
+        write_type(out, &m.ty, owning_module);
     }
     if let Some(body) = &m.default {
         out.push_str(" default {\n");
         indent(out, level + 1);
-        write_term(out, body, level + 1);
+        write_term(out, body, level + 1, owning_module);
         out.push('\n');
         indent(out, level);
         out.push_str("}\n");
@@ -413,16 +420,16 @@ fn write_class_method(out: &mut String, m: &ClassMethod, level: usize) {
 
 /// Render an instance declaration in Form-B:
 /// `instance Class Type { <method bodies> }`.
-fn write_instance_def(out: &mut String, i: &InstanceDef, level: usize) {
+fn write_instance_def(out: &mut String, i: &InstanceDef, level: usize, owning_module: &str) {
     write_doc(out, &i.doc, level);
     indent(out, level);
     out.push_str("instance ");
     out.push_str(&i.class);
     out.push(' ');
-    write_type(out, &i.type_);
+    write_type(out, &i.type_, owning_module);
     out.push_str(" {\n");
     for m in &i.methods {
-        write_instance_method(out, m, level + 1);
+        write_instance_method(out, m, level + 1, owning_module);
     }
     indent(out, level);
     out.push('}');
@@ -431,13 +438,13 @@ fn write_instance_def(out: &mut String, i: &InstanceDef, level: usize) {
 /// Render one method body of an instance: `fn name { <body> }`.
 /// The signature is recoverable from the class declaration via
 /// `InstanceDef.class` lookup, so it is intentionally elided.
-fn write_instance_method(out: &mut String, m: &InstanceMethod, level: usize) {
+fn write_instance_method(out: &mut String, m: &InstanceMethod, level: usize, owning_module: &str) {
     indent(out, level);
     out.push_str("fn ");
     out.push_str(&m.name);
     out.push_str(" {\n");
     indent(out, level + 1);
-    write_term(out, &m.body, level + 1);
+    write_term(out, &m.body, level + 1, owning_module);
     out.push('\n');
     indent(out, level);
     out.push_str("}\n");
@@ -445,32 +452,42 @@ fn write_instance_method(out: &mut String, m: &InstanceMethod, level: usize) {
 
 // ---- types ----------------------------------------------------------------
 
-fn write_mode_type(out: &mut String, t: &Type, mode: ParamMode) {
+fn write_mode_type(out: &mut String, t: &Type, mode: ParamMode, owning_module: &str) {
     match mode {
-        ParamMode::Implicit => write_type(out, t),
+        ParamMode::Implicit => write_type(out, t, owning_module),
         ParamMode::Own => {
             out.push_str("own ");
-            write_type(out, t);
+            write_type(out, t, owning_module);
         }
         ParamMode::Borrow => {
             out.push_str("borrow ");
-            write_type(out, t);
+            write_type(out, t, owning_module);
         }
     }
 }
 
-fn write_type(out: &mut String, t: &Type) {
+fn write_type(out: &mut String, t: &Type, owning_module: &str) {
     match t {
         Type::Var { name } => out.push_str(name),
         Type::Con { name, args } => {
-            out.push_str(name);
+            // Ct.4.3: trim a qualifier whose owner matches the current
+            // file's module: `prelude.Ordering` printed from inside
+            // `prelude` becomes bare `Ordering`. Cross-module qualifiers
+            // (any other owner) survive verbatim. Mirrors the post-ct.1
+            // canonical-form rule "bare = local, qualified = cross-
+            // module" on the prose surface.
+            let display_name = match name.split_once('.') {
+                Some((owner, suffix)) if owner == owning_module => suffix,
+                _ => name.as_str(),
+            };
+            out.push_str(display_name);
             if !args.is_empty() {
                 out.push('<');
                 for (i, a) in args.iter().enumerate() {
                     if i > 0 {
                         out.push_str(", ");
                     }
-                    write_type(out, a);
+                    write_type(out, a, owning_module);
                 }
                 out.push('>');
             }
@@ -493,10 +510,10 @@ fn write_type(out: &mut String, t: &Type) {
                     .unwrap_or(ParamMode::Implicit);
                 // In a bare `Type::Fn` outside a fn signature we have no
                 // parameter names, so render `mode T` only (no `name:`).
-                write_mode_type(out, p, mode);
+                write_mode_type(out, p, mode, owning_module);
             }
             out.push_str(") -> ");
-            write_mode_type(out, ret, *ret_mode);
+            write_mode_type(out, ret, *ret_mode, owning_module);
             if !effects.is_empty() {
                 out.push_str(" with ");
                 for (i, e) in effects.iter().enumerate() {
@@ -516,7 +533,7 @@ fn write_type(out: &mut String, t: &Type) {
                 out.push_str(v);
             }
             out.push_str("> ");
-            write_type(out, body);
+            write_type(out, body, owning_module);
         }
     }
 }
@@ -588,11 +605,11 @@ fn as_unary_not(t: &Term) -> Option<&Term> {
 /// is `PREC_NONE`, so a binary op at the root never wraps itself. All
 /// internal recursion goes through this same fn with the appropriate
 /// `parent_prec` for the sub-position.
-fn write_term(out: &mut String, t: &Term, level: usize) {
-    write_term_prec(out, t, level, PREC_NONE);
+fn write_term(out: &mut String, t: &Term, level: usize, owning_module: &str) {
+    write_term_prec(out, t, level, PREC_NONE, owning_module);
 }
 
-fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
+fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, owning_module: &str) {
     // Polish 1+2: infix binary operators with paren elision.
     if let Some((op, lhs, rhs, prec, left_assoc)) = as_binop(t) {
         let need_parens = prec < parent_prec;
@@ -611,11 +628,11 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
             // parens to avoid implying we accept it.
             (prec + 1, prec + 1)
         };
-        write_term_prec(out, lhs, level, lhs_floor);
+        write_term_prec(out, lhs, level, lhs_floor, owning_module);
         out.push(' ');
         out.push_str(op);
         out.push(' ');
-        write_term_prec(out, rhs, level, rhs_floor);
+        write_term_prec(out, rhs, level, rhs_floor, owning_module);
         if need_parens {
             out.push(')');
         }
@@ -626,7 +643,7 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
     // so anything below atomic (i.e. another binary op) wraps.
     if let Some(arg) = as_unary_not(t) {
         out.push('!');
-        write_term_prec(out, arg, level, PREC_ATOMIC);
+        write_term_prec(out, arg, level, PREC_ATOMIC, owning_module);
         return;
     }
 
@@ -642,7 +659,7 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
             }
             // Callee is rendered at PREC_ATOMIC: a binary op as callee
             // (rare, but legal) would need parens.
-            write_term_prec(out, callee, level, PREC_ATOMIC);
+            write_term_prec(out, callee, level, PREC_ATOMIC, owning_module);
             out.push('(');
             for (i, a) in args.iter().enumerate() {
                 if i > 0 {
@@ -650,7 +667,7 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
                 }
                 // Args sit in their own paren context — no outer prec
                 // floor. Pass NONE so binary ops inside don't wrap.
-                write_term_prec(out, a, level, PREC_NONE);
+                write_term_prec(out, a, level, PREC_NONE, owning_module);
             }
             out.push(')');
         }
@@ -675,20 +692,20 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
                 && count_free_var(name, body) == 1
                 && {
                     let mut buf = String::new();
-                    write_term(&mut buf, value, level);
+                    write_term(&mut buf, value, level, owning_module);
                     !buf.contains('\n') && buf.len() <= RHS_INLINE_BUDGET
                 };
             if inlinable {
                 let inlined = subst_var_with_term(body, name, value);
-                write_term_prec(out, &inlined, level, parent_prec);
+                write_term_prec(out, &inlined, level, parent_prec, owning_module);
             } else {
                 out.push_str("let ");
                 out.push_str(name);
                 out.push_str(" = ");
-                write_term(out, value, level);
+                write_term(out, value, level, owning_module);
                 out.push_str(";\n");
                 indent(out, level);
-                write_term(out, body, level);
+                write_term(out, body, level, owning_module);
             }
         }
         Term::LetRec {
@@ -722,10 +739,10 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
                         .get(i)
                         .copied()
                         .unwrap_or(ParamMode::Implicit);
-                    write_mode_type(out, pty, mode);
+                    write_mode_type(out, pty, mode, owning_module);
                 }
                 out.push_str(") -> ");
-                write_mode_type(out, ret, *ret_mode);
+                write_mode_type(out, ret, *ret_mode, owning_module);
                 if !effects.is_empty() {
                     out.push_str(" with ");
                     for (i, e) in effects.iter().enumerate() {
@@ -737,28 +754,28 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
                 }
             } else {
                 out.push_str(") -> ");
-                write_type(out, ty);
+                write_type(out, ty, owning_module);
             }
             out.push_str(" {\n");
             indent(out, level + 1);
-            write_term(out, body, level + 1);
+            write_term(out, body, level + 1, owning_module);
             out.push('\n');
             indent(out, level);
             out.push_str("};\n");
             indent(out, level);
-            write_term(out, in_term, level);
+            write_term(out, in_term, level, owning_module);
         }
         Term::If { cond, then, else_ } => {
             out.push_str("if ");
-            write_term(out, cond, level);
+            write_term(out, cond, level, owning_module);
             out.push_str(" {\n");
             indent(out, level + 1);
-            write_term(out, then, level + 1);
+            write_term(out, then, level + 1, owning_module);
             out.push('\n');
             indent(out, level);
             out.push_str("} else {\n");
             indent(out, level + 1);
-            write_term(out, else_, level + 1);
+            write_term(out, else_, level + 1, owning_module);
             out.push('\n');
             indent(out, level);
             out.push('}');
@@ -774,7 +791,7 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
                 if i > 0 {
                     out.push_str(", ");
                 }
-                write_term(out, a, level);
+                write_term(out, a, level, owning_module);
             }
             out.push(')');
         }
@@ -783,6 +800,12 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
             ctor,
             args,
         } => {
+            // Ct.4.3: the Ctor `type_name` field is intentionally
+            // elided from the prose surface — the type is recoverable
+            // from typecheck context, and showing it on every Ctor
+            // would clutter the read. The qualifier-trim that applies
+            // to `Type::Con.name` therefore has no analogue here:
+            // there is no `out.push_str(type_name)` site to trim.
             out.push_str(ctor);
             if !args.is_empty() {
                 out.push('(');
@@ -790,20 +813,20 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
                     if i > 0 {
                         out.push_str(", ");
                     }
-                    write_term(out, a, level);
+                    write_term(out, a, level, owning_module);
                 }
                 out.push(')');
             }
         }
         Term::Match { scrutinee, arms } => {
             out.push_str("match ");
-            write_term(out, scrutinee, level);
+            write_term(out, scrutinee, level, owning_module);
             out.push_str(" {\n");
             for (i, arm) in arms.iter().enumerate() {
                 indent(out, level + 1);
                 write_pattern(out, &arm.pat);
                 out.push_str(" => ");
-                write_term(out, &arm.body, level + 1);
+                write_term(out, &arm.body, level + 1, owning_module);
                 if i + 1 < arms.len() {
                     out.push(',');
                 }
@@ -827,10 +850,10 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
                 }
                 out.push_str(pname);
                 out.push_str(": ");
-                write_type(out, pty);
+                write_type(out, pty, owning_module);
             }
             out.push_str("| -> ");
-            write_type(out, ret_ty);
+            write_type(out, ret_ty, owning_module);
             if !effects.is_empty() {
                 out.push_str(" with ");
                 for (i, e) in effects.iter().enumerate() {
@@ -842,7 +865,7 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
             }
             out.push_str(" {\n");
             indent(out, level + 1);
-            write_term(out, body, level + 1);
+            write_term(out, body, level + 1, owning_module);
             out.push('\n');
             indent(out, level);
             out.push('}');
@@ -850,14 +873,14 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
         Term::Seq { lhs, rhs } => {
             // Semicolon-as-discard. `lhs;` on its own line, `rhs` on
             // the next at the same indent. The caller already indented us.
-            write_term(out, lhs, level);
+            write_term(out, lhs, level, owning_module);
             out.push_str(";\n");
             indent(out, level);
-            write_term(out, rhs, level);
+            write_term(out, rhs, level, owning_module);
         }
         Term::Clone { value } => {
             out.push_str("clone(");
-            write_term(out, value, level);
+            write_term(out, value, level, owning_module);
             out.push(')');
         }
         Term::ReuseAs { source, body } => {
@@ -869,10 +892,10 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
             // single-expression bodies (the 99% Ctor case) stay inline,
             // collapsing the whole match arm to one line.
             out.push_str("reuse ");
-            write_term(out, source, level);
+            write_term(out, source, level, owning_module);
             out.push_str(" as ");
             let mut body_buf = String::new();
-            write_term(&mut body_buf, body, level + 1);
+            write_term(&mut body_buf, body, level + 1, owning_module);
             if body_buf.contains('\n') {
                 out.push_str("{\n");
                 indent(out, level + 1);
@@ -1178,13 +1201,13 @@ mod tests {
 
     fn render_term(t: &Term) -> String {
         let mut out = String::new();
-        write_term(&mut out, t, 0);
+        write_term(&mut out, t, 0, "");
         out
     }
 
     fn render_type(t: &Type) -> String {
         let mut out = String::new();
-        write_type(&mut out, t);
+        write_type(&mut out, t, "");
         out
     }
 
@@ -1647,7 +1670,7 @@ mod tests {
             doc: None,
         };
         let mut out = String::new();
-        write_fn_def(&mut out, &fd, 0);
+        write_fn_def(&mut out, &fd, 0, "");
         assert!(out.contains("xs: own IntList"), "got:\n{out}");
         assert!(out.contains(") -> Int "), "got:\n{out}");
     }
@@ -1663,7 +1686,7 @@ mod tests {
             doc: None,
         };
         let mut out = String::new();
-        write_fn_def(&mut out, &fd, 0);
+        write_fn_def(&mut out, &fd, 0, "");
         assert!(out.contains("() -> Unit with IO {"), "got:\n{out}");
     }
 
@@ -1695,7 +1718,7 @@ mod tests {
             doc: Some("Take ownership.".into()),
         };
         let mut out = String::new();
-        write_fn_def(&mut out, &fd, 0);
+        write_fn_def(&mut out, &fd, 0, "");
         // Suppress line is the FIRST line, before the doc.
         let first_line = out.lines().next().unwrap();
         assert_eq!(
@@ -1735,7 +1758,7 @@ mod tests {
             doc: None,
         };
         let mut out = String::new();
-        write_fn_def(&mut out, &fd, 0);
+        write_fn_def(&mut out, &fd, 0, "");
         let lines: Vec<&str> = out.lines().collect();
         assert_eq!(lines[0], "// @suppress over-strict-mode: first reason");
         assert_eq!(lines[1], "// @suppress some-other-code: second reason");
@@ -1757,7 +1780,7 @@ mod tests {
             doc: Some("just a doc".into()),
         };
         let mut out = String::new();
-        write_fn_def(&mut out, &fd, 0);
+        write_fn_def(&mut out, &fd, 0, "");
         assert!(
             !out.contains("// @suppress"),
             "no @suppress line for empty Vec; got:\n{out}"
@@ -1782,7 +1805,7 @@ mod tests {
             drop_iterative: false,
         };
         let mut out = String::new();
-        write_type_def(&mut out, &td, 0);
+        write_type_def(&mut out, &td, 0, "");
         assert!(out.starts_with("/// line one\n/// line two\n"), "got:\n{out}");
     }
 
@@ -1804,7 +1827,7 @@ mod tests {
             drop_iterative: false,
         };
         let mut out = String::new();
-        write_type_def(&mut out, &td, 0);
+        write_type_def(&mut out, &td, 0, "");
         assert_eq!(out, "data IntList = Nil | Cons(Int, IntList)");
     }
 
@@ -1995,7 +2018,7 @@ mod tests {
             drop_iterative: false,
         };
         let mut out = String::new();
-        write_type_def(&mut out, &td, 0);
+        write_type_def(&mut out, &td, 0, "");
         let doc_lines: Vec<&str> = out.lines().take_while(|l| l.starts_with("///")).collect();
         assert!(doc_lines.len() >= 2, "expected wrap, got:\n{out}");
         for line in &doc_lines {
@@ -2025,7 +2048,7 @@ mod tests {
             drop_iterative: false,
         };
         let mut out = String::new();
-        write_type_def(&mut out, &td, 0);
+        write_type_def(&mut out, &td, 0, "");
         assert!(out.starts_with("/// Short and snappy.\n"), "got:\n{out}");
         let doc_count = out.lines().filter(|l| l.starts_with("///")).count();
         assert_eq!(doc_count, 1);
@@ -2047,7 +2070,7 @@ mod tests {
             drop_iterative: false,
         };
         let mut out = String::new();
-        write_type_def(&mut out, &td, 0);
+        write_type_def(&mut out, &td, 0, "");
         let doc_lines: Vec<&str> = out.lines().take_while(|l| l.starts_with("///")).collect();
         // First line = unwrapped first paragraph; the rest = wrapped
         // second paragraph (≥ 2 lines).
@@ -2072,7 +2095,7 @@ mod tests {
             drop_iterative: false,
         };
         let mut out = String::new();
-        write_type_def(&mut out, &td, 0);
+        write_type_def(&mut out, &td, 0, "");
         let doc_lines: Vec<&str> = out.lines().take_while(|l| l.starts_with("///")).collect();
         // The last doc line MUST have ≥ 2 words.
         let last = doc_lines.last().unwrap();
@@ -2150,6 +2173,99 @@ mod tests {
         );
     }
 
+    /// When a `Type::Con.name` is qualified with the owning
+    /// module's own name (e.g. `prelude.Ordering` inside
+    /// `prelude`'s own file), the prose printer must trim the
+    /// qualifier and emit bare `Ordering`. Cross-module qualified
+    /// refs (`prelude.Ordering` inside any non-prelude file)
+    /// round-trip verbatim.
+    #[test]
+    fn type_con_qualifier_trimmed_when_owner_matches_module() {
+        use ailang_core::ast::{Module, Def, FnDef, Type, Term, ParamMode};
+
+        let m = Module {
+            schema: "ailang/v0".into(),
+            name: "prelude".into(),
+            imports: vec![],
+            defs: vec![Def::Fn(FnDef {
+                name: "noop".into(),
+                ty: Type::Fn {
+                    params: vec![],
+                    ret: Box::new(Type::Con {
+                        name: "prelude.Ordering".into(),
+                        args: vec![],
+                    }),
+                    effects: vec![],
+                    param_modes: vec![],
+                    ret_mode: ParamMode::Implicit,
+                },
+                params: vec![],
+                body: Term::Ctor {
+                    type_name: "prelude.Ordering".into(),
+                    ctor: "EQ".into(),
+                    args: vec![],
+                },
+                doc: None,
+                suppress: vec![],
+            })],
+        };
+
+        let prose = module_to_prose(&m);
+        assert!(
+            prose.contains("-> Ordering"),
+            "expected bare `Ordering` in fn return type (owner == file's \
+             module); got prose:\n{}",
+            prose
+        );
+        assert!(
+            !prose.contains("prelude.Ordering"),
+            "expected NO `prelude.Ordering` after trim; got prose:\n{}",
+            prose
+        );
+    }
+
+    /// A cross-module Type::Con (owner != current file's module)
+    /// must round-trip verbatim — no trim.
+    #[test]
+    fn type_con_qualifier_preserved_when_owner_differs() {
+        use ailang_core::ast::{Module, Def, FnDef, Type, Term, ParamMode, Import};
+
+        let m = Module {
+            schema: "ailang/v0".into(),
+            name: "user".into(),
+            imports: vec![Import { module: "prelude".into(), alias: None }],
+            defs: vec![Def::Fn(FnDef {
+                name: "lt".into(),
+                ty: Type::Fn {
+                    params: vec![],
+                    ret: Box::new(Type::Con {
+                        name: "prelude.Ordering".into(),
+                        args: vec![],
+                    }),
+                    effects: vec![],
+                    param_modes: vec![],
+                    ret_mode: ParamMode::Implicit,
+                },
+                params: vec![],
+                body: Term::Ctor {
+                    type_name: "prelude.Ordering".into(),
+                    ctor: "LT".into(),
+                    args: vec![],
+                },
+                doc: None,
+                suppress: vec![],
+            })],
+        };
+
+        let prose = module_to_prose(&m);
+        assert!(
+            prose.contains("prelude.Ordering"),
+            "expected qualified `prelude.Ordering` preserved (owner != file's \
+             module); got prose:\n{}",
+            prose
+        );
+    }
+
     #[test]
     fn deeply_nested_match_keeps_each_level_at_its_own_indent() {
         // Three-deep nesting: each level lands one indent step deeper.
diff --git a/crates/ailang-prose/tests/snapshot.rs b/crates/ailang-prose/tests/snapshot.rs
index b64380d..adb2801 100644
--- a/crates/ailang-prose/tests/snapshot.rs
+++ b/crates/ailang-prose/tests/snapshot.rs
@@ -86,3 +86,17 @@ fn snapshot_test_22b2_instance_present() {
 fn snapshot_test_22b2_constraint_declared_via_superclass() {
     check_snapshot("test_22b2_constraint_declared_via_superclass");
 }
+
+/// Ct.4.3: snapshot for the canonical ordering-match fixture.
+/// `ordering_match.ail.json` is in the `ordering_match` module
+/// and references `prelude.Ordering` via a cross-module
+/// `Term::Ctor.type_name`. The prose printer drops Ctor
+/// `type_name`s entirely (recoverable from typecheck context),
+/// so the rendered prose carries `LT`/`EQ`/`GT` without any
+/// `prelude.` qualifier — the trim-on-print logic is exercised
+/// by the unit tests on `Type::Con`, which is the surface
+/// where the qualifier survives into the rendered text.
+#[test]
+fn snapshot_ordering_match() {
+    check_snapshot("ordering_match");
+}
diff --git a/examples/ordering_match.prose.txt b/examples/ordering_match.prose.txt
new file mode 100644
index 0000000..3d56346
--- /dev/null
+++ b/examples/ordering_match.prose.txt
@@ -0,0 +1,11 @@
+// module ordering_match
+
+/// Iter 23.1 fixture: pattern-match on prelude Ordering ctor without explicit
+/// prelude import.
+fn main() -> Unit with IO {
+  do io/print_int(match LT {
+    LT => 1,
+    EQ => 2,
+    GT => 3
+  })
+}