design/ ledger: dense cross-linking via three topical splits + 88-link sweep

The first formal-links milestone shipped clause-5 + 8 links across the
existing file layout. Browsing surfaced that file-only granularity is
only as precise as the file boundaries — three files mixed two or
three navigation targets under one address, so the 8 links could not
multiply without ambiguity. This commit fixes the substrate, then
applies the sweep the original milestone deferred.

Splits (each extracts an already-self-contained section into its own
file so links land on the topic, not the parent doc's TOC):

  contracts/typeclasses.md
    → +contracts/prelude-classes.md  (Eq/Ord/Show ships, polymorphic `print`)
    → +contracts/method-dispatch.md  (5-step dispatch rule, candidate index)

  contracts/memory-model.md
    → +contracts/language-constraints.md  (the 4 binding constraints
                                           making RC sound without a
                                           cycle collector)

  models/authoring-surface.md
    → +models/prose-projection.md  (Form-B / `ail prose` / merge-prose)

Each new file enters design/INDEX.md as its own row (three contracts
share show_no_instance_e2e.rs / uniqueness.rs as ratifying tests;
prose-projection is a model). Two pre-existing links rebind to the
new topic-files (memory-model.md → method-dispatch.md;
float-semantics.md → prelude-classes.md).

Link sweep: 8 → 88 formal Markdown links over 23 files. Every file
in design/contracts/ + design/models/ now has at least one outgoing
link; the tree is fully connected. Links are file-relative
`[label](path)` per the established convention, fenced code blocks
are skipped (a `](` inside ```jsonc``` is literal text), the durable
tier (design/ + crates/ + runtime/) is enforced by clause-5.

Tests:
  - design_index_pin.rs (5/5 clauses): clean-cut, INDEX resolution,
    ratifying-test resolution, no decision-record prose in contracts/,
    body links durable + resolving.
  - docs_honesty_pin.rs (5/5): one assertion rebinds from typeclasses.md
    to prelude-classes.md (where the gated sentence now lives);
    design_corpus widens to include the 4 new files so the Wunschdenken
    / doc-archaeology sweeps continue to cover everything that used to
    live in the parents.

No spec/plan/journal for this batch — interactive collaboration after
the milestone closed; the user gated the splits explicitly before the
sweep.

design/contracts/authoring-surface.md

@@ -18,7 +18,7 @@ the same time, leaving only diagnostic helpers (`type_to_string`,
 The textual surface is **not** a replacement for the JSON-AST. It is
 one projection among potentially many. Concretely:
 
-- The JSON-AST keeps its role as the canonical, hashable, content-
+- The [JSON-AST](data-model.md) keeps its role as the canonical, hashable, content-
   addressed representation of a module. All hashing, content-
   addressing, cross-module references, and typecheck/codegen input
   flow through the JSON-AST. **No new hashable form is introduced.**
@@ -55,7 +55,7 @@ the AST and remain projection-agnostic.
    shape. The full bijection between `.ail.json` and `.ail` (both
    directions, BLAKE3-stable hashing, Float-bits-hex encoding,
    workspace-CI enforcement points) is anchored as the top-level
-   §"Roundtrip Invariant" — this constraint records that Decision
+   [Roundtrip Invariant](roundtrip-invariant.md) — this constraint records that Decision
    6's surface-design choice must satisfy that invariant; the
    invariant itself lives at top level because the property is
    load-bearing on the language identity, not on this Decision's

design/contracts/data-model.md

@@ -167,7 +167,8 @@ are real surface forms.
 ```
 
 In the MVP, `do` is only a direct call to a built-in effect op (no
-handler). A `lam` term constructs an anonymous function value; free
+handler); the effect system is described in [effects](../models/effects.md).
+A `lam` term constructs an anonymous function value; free
 variables of its body are captured from the enclosing scope.
 
 Loop binders are alloca-resident: typecheck binds them in the
@@ -237,6 +238,10 @@ Patterns are linear: each pattern variable may appear at most once.
 
 `implicit ≡ own` semantically; the distinction exists so existing
 unannotated fixtures continue to serialize without the mode wrapper and keep their
-canonical-JSON hash.
+canonical-JSON hash. The full mode contract (codegen consequences,
+the over-strict-mode lint, the `Suppress` mechanism) lives in
+[memory model](memory-model.md); the four language-design
+preconditions that make RC sound live in
+[language constraints](language-constraints.md).
 
 Ratified by: `crates/ailang-core/tests/design_schema_drift.rs`.

design/contracts/embedding-abi.md

@@ -47,8 +47,9 @@ ctx-threaded C signature is the M2 shape.
 
 Export parameters are written **bare**: a scalar type carries no
 `own`/`borrow` mode (a single-constructor record export parameter,
-by contrast, carries `own`/`borrow` — the ownership contract the
-frozen value layout below specifies). The
+by contrast, carries `own`/`borrow` — see [memory model](memory-model.md)
+for the full ownership contract; the
+frozen value layout below specifies how that contract lands at the C ABI). The
 canonical M1 export shape:
 
 ```

design/contracts/feature-acceptance.md

@@ -29,7 +29,8 @@ A proposed feature ships only if all three hold:
    RC-acyclicity guarantees were built to remove. The decisive
    question is whether the construct re-opens a class of mistakes
    (iterated-mutable-state reasoning, silently-unbounded recursion,
-   reference cycles) that a foundational invariant closes. If it does,
+   reference cycles) that a foundational invariant — see
+   [language constraints](language-constraints.md) — closes. If it does,
    it is cut even when 1 and 2 hold — *or* it must be reshaped until
    the bug class is structurally impossible rather than merely
    discouraged. A documentation note is not a reshape; the

design/contracts/float-semantics.md

@@ -66,7 +66,7 @@ no `f32` variant. The runtime / codegen contract:
 
 The same libc-`%g` rendering applies to `show 1.5` / `show nan` /
 `show inf` via `instance Show Float` (which calls `float_to_str`
-internally — see [Prelude (built-in) classes](typeclasses.md) for the Show ship).
+internally — see [Prelude (built-in) classes](prelude-classes.md) for the Show ship).
 The NaN-spelling caveat above is observable via `do print x` for
 Float-typed `x`; the rendering is libc-version-dependent and
 target-libc-specific. AILang does NOT canonicalise Float textual
@@ -83,12 +83,16 @@ use case appears.
 
 **Form-A serialisation:** Float literals carry the IEEE-754
 bit pattern as a 16-character lowercase hex string in the canonical
-JSON: `{"kind":"float","bits":"<16-hex>"}`. Routing through the
+JSON: `{"kind":"float","bits":"<16-hex>"}` (see
+[Data model](data-model.md) for the literal schema). Routing through the
 JSON *string* path (not `serde_json::Number`) preserves bit
 stability across `serde_json` versions and lets NaN / ±Inf
 round-trip through Form-A — JSON numbers cannot represent them.
+This bits-hex encoding is what keeps Floats inside the
+[Roundtrip Invariant](roundtrip-invariant.md).
 
-**Pattern matching:** `Pattern::Lit` on `Literal::Float` is hard-
+**Pattern matching:** `Pattern::Lit` on `Literal::Float` (see
+[Data model](data-model.md) for the pattern schema) is hard-
 rejected at typecheck (`CheckError::FloatPatternNotAllowed`). IEEE
 semantics make Float patterns semantically dubious — NaN never
 matches via IEEE-`==`, and bit-exact equality is rarely what an

design/contracts/frozen-value-layout.md

@@ -3,7 +3,8 @@
 ## Frozen value layout (M3 — one-way commitment)
 
 For a single-constructor `data T` whose `n` fields are each `Int`
-or `Float`, a value of `T` crossing the embedding C boundary is a
+or `Float`, a value of `T` crossing the
+[embedding C boundary](embedding-abi.md) is a
 bare payload pointer `p`:
 
 | bytes | content |
@@ -27,8 +28,9 @@ offsets above. A raw `malloc` is a contract violation:
 `own`-consume and `ailang_rc_dec` both require the runtime's 8-byte
 header at `p - 8` initialised to `1`.
 
-**Ownership follows the declared mode** (the §"Mode metadata is
-load-bearing for codegen" contract, as the C ABI): a `(own (con
+**Ownership follows the declared mode** (the
+[Mode metadata is load-bearing for codegen](memory-model.md)
+contract, as the C ABI): a `(own (con
 T))` parameter transfers ownership in — the kernel consumes it
 (Iter-B drop-at-return); the host MUST NOT touch or `dec` it after
 the call. A `(borrow (con T))` parameter is retained by the host —

design/contracts/honesty-rule.md

@@ -15,9 +15,10 @@ Two things never belong in a contract or model file:
 
 A cross-reference that does belong stays: it is a formal,
 file-relative Markdown link into the durable tier (`design/` or
-source), enforced by `design_index_pin.rs` clause-5. A reference
-that cannot be expressed as such a link is, by that fact, the
-history-or-rationale prose the rule above removes.
+source), enforced by
+[`design_index_pin.rs`](../../crates/ailang-core/tests/design_index_pin.rs)
+clause-5. A reference that cannot be expressed as such a link is,
+by that fact, the history-or-rationale prose the rule above removes.
 
 The single legitimate exception is a present-tense reserved or
 deliberately-excluded claim that is explicitly and correctly

design/contracts/language-constraints.md

@@ -0,0 +1,40 @@
+# Language-design constraints (binding)
+
+## Language-design constraints (binding)
+
+The four constraints below are necessary preconditions for RC to
+be sound and complete *without* a cycle-collector backstop. They
+are not new — AILang already satisfies all four — but Decision 10
+makes them load-bearing rather than incidental:
+
+1. **Strict evaluation.** Every `Term::App` (see
+   [Data model](data-model.md)) argument is fully
+   evaluated before the call. No laziness, no thunks. (Already
+   true.)
+2. **No recursive value bindings.** `(let x EXPR ...)` evaluates
+   `EXPR` in a scope where `x` is *not* bound. Recursion is
+   exclusively via `Term::LetRec` (which binds a fn, not a value)
+   and module-level fn defs. (Already true.)
+3. **No shared mutable refs.** Values are immutable once
+   constructed. There is no `ref`, `IORef`, `Mutex`, or any
+   primitive that allows a value to be mutated from a position
+   outside its allocation. (Already true.)
+4. **ADTs are acyclic by construction.** Strict evaluation +
+   no-recursive-value-bindings + no-shared-mutable-refs together
+   guarantee that any value graph reachable from a binding is a
+   DAG. The reference graph has no cycles. (Follows from 1–3.)
+
+Laziness, recursive value bindings, shared mutable state, or any
+feature that creates cycles is rejected at design time unless the
+proposal proves the cycle is collectible by an extension (e.g.
+linear ownership).
+
+These constraints are the precondition for the
+[memory model](memory-model.md): a sound RC implementation without
+a cycle-collector backstop requires the reference graph to be a
+DAG, which constraint 4 establishes from 1–3. They are also the
+load-bearing structural reason behind several
+[feature-acceptance](feature-acceptance.md) clause-3 rejections
+(notably iterated-mutable-state reasoning).
+
+Ratified by: `crates/ailang-check/src/uniqueness.rs` (in-source mod tests).

design/contracts/memory-model.md

@@ -1,38 +1,19 @@
-# Memory model — language-design constraints and codegen contract
+# Memory model — schema, diagnostics, codegen contract
 
-## Language-design constraints (binding)
-
-The four constraints below are necessary preconditions for RC to
-be sound and complete *without* a cycle-collector backstop. They
-are not new — AILang already satisfies all four — but Decision 10
-makes them load-bearing rather than incidental:
-
-1. **Strict evaluation.** Every `Term::App` argument is fully
-   evaluated before the call. No laziness, no thunks. (Already
-   true.)
-2. **No recursive value bindings.** `(let x EXPR ...)` evaluates
-   `EXPR` in a scope where `x` is *not* bound. Recursion is
-   exclusively via `Term::LetRec` (which binds a fn, not a value)
-   and module-level fn defs. (Already true.)
-3. **No shared mutable refs.** Values are immutable once
-   constructed. There is no `ref`, `IORef`, `Mutex`, or any
-   primitive that allows a value to be mutated from a position
-   outside its allocation. (Already true.)
-4. **ADTs are acyclic by construction.** Strict evaluation +
-   no-recursive-value-bindings + no-shared-mutable-refs together
-   guarantee that any value graph reachable from a binding is a
-   DAG. The reference graph has no cycles. (Follows from 1–3.)
-
-Laziness, recursive value bindings, shared mutable state, or any
-feature that creates cycles is rejected at design time unless the
-proposal proves the cycle is collectible by an extension (e.g.
-linear ownership).
+The four language-design constraints that make RC sound without a
+cycle-collector backstop (strict evaluation, no recursive value
+bindings, no shared mutable refs, acyclic ADTs) live in
+[language constraints](language-constraints.md); this file covers
+the schema additions, advisory diagnostics, and codegen contract
+that build on them.
 
 ## Schema additions
 
-**Parameter modes on `Type::Fn`.**
+**Parameter modes on `Type::Fn`** (see [Data model](data-model.md)
+for the schema-level definition of `Type::Fn`).
 
-The form-A surface for fn signatures gains mode wrappers:
+The form-A surface (see [authoring surface](authoring-surface.md))
+for fn signatures gains mode wrappers:
 
 ```
 (fn-type (params (borrow (List Int))) (ret (con Int)))
@@ -102,7 +83,7 @@ Three schema fields carry class references in this form:
 `ClassDef.name` itself stays bare (defining-site context, like
 `TypeDef.name`).
 
-Method dispatch is type-driven post-mq.3 (see [Method dispatch](typeclasses.md)):
+Method dispatch is type-driven post-mq.3 (see [Method dispatch](method-dispatch.md)):
 synth resolves a `Term::Var { name: "show" }` by consulting
 the workspace's method-to-candidate-class index, filtering by
 argument type (concrete) or by declared constraint (rigid-var), and
@@ -167,8 +148,8 @@ until the fixture intentionally adopts the feature.
 **`FnDef.suppress`.** The `suppress` field on `FnDef` carries a
 list of advisory-diagnostic suppress entries; each entry has a
 `code` (the diagnostic being suppressed) and a `because` (a
-mandatory non-empty reason). See §"Data model" for the canonical
-schema.
+mandatory non-empty reason). See [Data model](data-model.md) for
+the canonical schema.
 
 Form-A surface: `(suppress (code "...") (because "..."))` clause
 between fn name and `(type ...)`. Multiple clauses allowed; one

design/contracts/method-dispatch.md

@@ -0,0 +1,54 @@
+# Method dispatch
+
+## Method dispatch
+
+The class-method resolution rule that pairs with the
+[typeclasses](typeclasses.md) contract; the `Show`/`Eq`/`Ord` instances
+the rule dispatches against live in [prelude classes](prelude-classes.md).
+
+Post-mq.3, dispatch is two-mode:
+
+**Polymorphic call sites** (inside a fn body with `forall` +
+constraint set): the constraint names the class via the qualified
+`Constraint.class` field (canonical-form per mq.1). Synth's
+residual carries the class name directly; constraint-discharge at
+fn-body-end matches against the workspace registry by
+`(class, type_hash)` key.
+
+**Monomorphic call sites**: synth consults the workspace-flat
+`Env.method_to_candidate_classes: BTreeMap<MethodName,
+BTreeSet<QualifiedClassName>>` index, then runs the 5-step
+dispatch rule:
+
+1. Parse the `Term::Var.name` for an optional class qualifier
+   (last-dot-segment is the method name; everything before is the
+   qualified class).
+2. If `method_to_candidate_classes` has no entry for the method
+   name, fall through to the existing Var-arm branches (free fn
+   lookup, dot-qualified cross-module).
+3. Qualifier present: filter candidates to the named class. Empty
+   result fires `UnknownClass`. Singleton survivor proceeds.
+4. Qualifier empty (bare-method form): singleton candidate proceeds
+   directly; multiple candidates yield a multi-candidate residual
+   for discharge-time refinement.
+5. At discharge, refinement runs: concrete `type_` filters
+   candidates via the workspace registry; rigid-var `type_` filters
+   via the active fn's declared constraints
+   (`env.active_declared_constraints`). Single survivor discharges;
+   multiple survivors fire `AmbiguousMethodResolution` (concrete) or
+   `MissingConstraint` (rigid-var); zero survivors fire `NoInstance`
+   (concrete) or `MissingConstraint` (rigid-var).
+
+The `method_to_candidate_classes` index is the load-bearing data
+structure for this routing — its construction in `build_check_env`
+inverts the per-module `class_methods` maps (themselves tuple-keyed
+by `(qualified-class, method)` post-mq.3) to a workspace-flat
+method-name-to-class-set map.
+
+Class-fn collisions resolve at the call site, not at workspace load
+time: the fn lookup precedence (locals → caller-module-fn →
+imported-fn) runs ahead of the class-method branch. When both
+sides have a match, the fn wins and a `class-method-shadowed-by-fn`
+warning surfaces the shadow.
+
+Ratified by: `crates/ail/tests/show_no_instance_e2e.rs`.

design/contracts/prelude-classes.md

@@ -0,0 +1,32 @@
+# Prelude (built-in) classes
+
+## Prelude (built-in) classes
+
+The prelude ships the `Ordering` ADT, the `Eq` and `Ord`
+[classes](typeclasses.md), primitive `Eq Int/Bool/Str` and
+`Ord Int/Bool/Str` instances, and the five polymorphic free-fn
+helpers `ne`/`lt`/`le`/`gt`/`ge`. 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 cross-referencing this section. The lookup
+machinery that turns a `show x` call site into the right monomorphic
+instance is documented in [method dispatch](method-dispatch.md).
+
+The prelude ships `class Show a where show : (a borrow) -> Str` and
+primitive `Show Int`, `Show Bool`, `Show Str`, `Show Float`
+instances. Float **is** included in Show (unlike Eq/Ord) — IEEE-754
+makes structural equality and total ordering semantically dubious,
+but textual representation of a Float is well-defined modulo the
+NaN-spelling caveat in [Float semantics](float-semantics.md). Each
+`Show <T>` instance body is a single-application lambda invoking the
+corresponding runtime primitive (`int_to_str`, `bool_to_str`,
+`str_clone`, `float_to_str`; see [Str ABI](str-abi.md) for the
+heap-Str primitives); no codegen intercept is required. The
+polymorphic helper `print : forall a. Show a => a -> () !IO` has body
+`\x -> let s = show x in do io/print_str s` (explicit let-binder for
+heap-Str RC discipline per eob.1 Str carve-out). The let-binder is
+structurally pinned by `crates/ail/tests/print_mono_body_shape.rs`.
+Routing through `print` is the path for non-`Str` primitives;
+`io/print_str` is the only built-in direct-output effect-op.
+
+Ratified by: `crates/ail/tests/show_no_instance_e2e.rs`.

design/contracts/roundtrip-invariant.md

@@ -3,11 +3,12 @@
 ## Roundtrip Invariant
 
 Every well-formed AILang module has a canonical `.ail.json`
-representation (the hashable, content-addressed JSON-AST) and a
-hand-authored `.ail` representation (Form A, the authoring
-projection). The JSON-AST is derived from `.ail` in-process by
-consumers that need it; the round-trip is now the *property* of
-that derivation, not the byte-level agreement of two on-disk forms.
+representation (the hashable, content-addressed
+[JSON-AST](data-model.md)) and a hand-authored `.ail` representation
+(Form A, the [authoring projection](authoring-surface.md)). The
+JSON-AST is derived from `.ail` in-process by consumers that need
+it; the round-trip is now the *property* of that derivation, not
+the byte-level agreement of two on-disk forms.
 
 Concretely:
 
@@ -46,9 +47,9 @@ approximation. The canonical encoding is
 `{"kind":"float","bits":"<16-lowercase-hex>"}` and the surface
 emits the same bits-hex string. NaN, ±Inf, signed zero, and subnormals all
 round-trip exactly because the JSON-number path is bypassed (see
-§"Float semantics", "Form-A serialisation"). Floats are not an
-exception to the invariant — the bits-hex encoding is the
-mechanism that keeps them *inside* it.
+[Float semantics](float-semantics.md), "Form-A serialisation").
+Floats are not an exception to the invariant — the bits-hex
+encoding is the mechanism that keeps them *inside* it.
 
 ### Enforcement
 

design/contracts/scope-boundaries.md

@@ -4,12 +4,14 @@
 
 Snapshot of the current boundary.
 
-- No effect handlers — only the built-in `IO` op (`io/print_str`).
+- No effect handlers — only the built-in `IO` op (`io/print_str`);
+  the effect system is described in [effects](../models/effects.md).
   `Diverge` is a reserved effect name with no op and no codegen.
 - No refinements / SMT escalation.
 - No HM inference inside bodies. Top-level def types are explicit;
-  polymorphism is opt-in via `Type::Forall { vars, body }`. Inside
-  a body, lambdas check monomorphically against their declared type.
+  polymorphism is opt-in via `Type::Forall { vars, body }` (see
+  [Data model](data-model.md)). Inside a body, lambdas check
+  monomorphically against their declared type.
 - Polymorphic fns must be **directly called** at the use site.
   Passing a polymorphic fn as a value (`let f = id in f(42)`) is
   not yet supported.
@@ -17,11 +19,12 @@ Snapshot of the current boundary.
   polymorphic fn (`apply(id, 42)`) is not supported.
 - No recursive `let` for non-fn values. Plain `let x = … in …` only
   sees `x` inside the body, not inside its own RHS — recursive value
-  bindings would break Decision 10's acyclicity invariant. Recursive
+  bindings would break the
+  [acyclicity invariant](language-constraints.md). Recursive
   *fn* bindings are supported via `Term::LetRec` (`{ "t": "letrec",
   ... }`); the desugar pass lifts most occurrences to a synthetic
   top-level fn, with `lift_letrecs` finishing the residue after
-  typecheck.
+  typecheck (see [pipeline](../models/pipeline.md)).
 - No visibility rules in imports. Every top-level def of an imported module
   is reachable; there is no `pub` / `priv`.
 
@@ -30,8 +33,9 @@ What **is** supported (and used as the smoke test for the pipeline):
 - Int, Bool, Unit, **Str**, **Float** as primitive types.
 - `if`, `let`, function calls, recursion.
 - Effects on function signatures, with `do op(args)` for direct effect
-  ops (`io/print_str`). The polymorphic `print` (§"Polymorphic print")
-  is the canonical output path for non-Str values.
+  ops (`io/print_str`). The polymorphic `print` (see
+  [prelude classes](prelude-classes.md)) is the canonical output
+  path for non-Str values.
 - **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`) of type
   `forall a. (a, a) -> a` (codegen-restricted to `{Int, Float}`);
   `%` of type `(Int, Int) -> Int` (Int-only — `fmod` semantics for
@@ -99,14 +103,17 @@ What **is** supported (and used as the smoke test for the pipeline):
   `(term-ctor std_pair.Pair MkPair x y)` and `(pat-ctor MkPair x y)`
   inside that scrutinee. Std-library demos (`examples/std_*_demo.ail.json`)
   exercise this end-to-end.
-- **AI-authoring text surface, form (A)** (Decision 6). The `ailang-surface` crate parses `.ail` form-A
-  text into a canonical `ailang-core::ast::Module` and prints any module
-  back as form-A text. `ail render` and `ail describe` use it as the
+- **AI-authoring text surface, form (A)** (see
+  [authoring surface](authoring-surface.md)). The `ailang-surface`
+  crate parses `.ail` form-A text into a canonical
+  `ailang-core::ast::Module` and prints any module back as form-A
+  text. `ail render` and `ail describe` use it as the
   sole text projection; `ail parse` is the inverse direction. Round-trip
   identity (text → AST → JSON → AST → text) is gated by
   `ailang-surface/tests/round_trip.rs` over every shipped fixture.
-- **Memory management via Boehm conservative GC** (Decision 9),
-  with **per-fn arena via stack `alloca` for non-escaping allocations**
+- **Memory management via Boehm conservative GC** (see
+  [RC + uniqueness](../models/rc-uniqueness.md)), with
+  **per-fn arena via stack `alloca` for non-escaping allocations**
   layered on top. Every ADT box, lambda env, and closure
   pair allocates either via `@GC_malloc` (escaping; Boehm-managed) or
   via LLVM `alloca` (non-escaping; freed at fn return). The decision

design/contracts/str-abi.md

@@ -12,13 +12,15 @@ and return an owned `Str`. Each is registered as a builtin in
 and backed by a `runtime/str.c` C helper.
 
 - `int_to_str : (borrow Int) -> Str` — decimal rendering
-  of an `Int`. Backs `Show Int` in the prelude.
+  of an `Int`. Backs `Show Int` in the
+  [prelude](prelude-classes.md).
 - `bool_to_str : (borrow Bool) -> Str` — `"true"`/`"false"`.
-  Backs `Show Bool` in the prelude.
+  Backs `Show Bool` in the [prelude](prelude-classes.md).
 - `float_to_str : (borrow Float) -> Str` —
   type-installed; codegen is reserved and not yet shipped.
 - `str_clone : (borrow Str) -> Str` — allocates a fresh
-  heap-Str copy of the input's bytes. Backs `Show Str` in the prelude.
+  heap-Str copy of the input's bytes. Backs `Show Str` in the
+  [prelude](prelude-classes.md).
 - `str_concat : (borrow Str, borrow Str) -> Str` — combines two `Str`
   values into a single owned `Str`.
   General-purpose; commonly used in Show bodies for labelled output
@@ -32,8 +34,8 @@ instance body that wants to combine fragments.
 
 Primitive output for `Str` values goes through `io/print_str`
 directly; values of other primitive types route through the
-polymorphic `print` helper (§"Polymorphic print"), which feeds
-the heap-Str result of `show x` into `io/print_str`.
+polymorphic `print` helper (see [prelude classes](prelude-classes.md)),
+which feeds the heap-Str result of `show x` into `io/print_str`.
 
 `==`, `<`, `<=`, `>`, `>=` REMAIN primitive operators. Class methods
 are accessed by name (`eq x y`, `lt x y`, …), not via these
@@ -57,7 +59,8 @@ bytes, regardless of realisation. The byte-comparison semantics
 are inherited from libc `strcmp` — locale-independent, NUL-
 terminated.
 
-The heap-Str realisation participates in standard RC: the
+The heap-Str realisation participates in standard RC (see
+[memory model](memory-model.md)): the
 `rc_header` slot eight bytes before the `len` field is managed
 by `ailang_rc_alloc` / `ailang_rc_inc` / `ailang_rc_dec` exactly
 like any other RC-allocated cell. The static-Str realisation has

design/contracts/tail-calls.md

@@ -12,7 +12,8 @@ hazard the language exists to eliminate.
 Solution: explicit, verified tail calls.
 
 - **AST.** `Term::App { fn, args, tail: bool }` and
-  `Term::Do { op, args, tail: bool }` gain a `tail` flag,
+  `Term::Do { op, args, tail: bool }` (see
+  [Data model](data-model.md)) gain a `tail` flag,
   serde-defaulting to `false` so existing fixtures load with
   `tail: false` and their hashes stay bit-identical.
 - **Typecheck.** A new pass `verify_tail_positions(fn_body)`
@@ -37,7 +38,8 @@ Solution: explicit, verified tail calls.
   Productions are positional analogues of `app`/`do` with
   `tail: true` set on the resulting term. EBNF gains 2 lines;
   total production count goes from ~28 to ~30, still inside
-  the constraint-1 budget.
+  the constraint-1 budget (see
+  [authoring surface](authoring-surface.md)).
 
 **What this does NOT promise.** Per the tail-call survey of existing fixtures,
 many existing recursive calls are *not* in tail position

design/contracts/typeclasses.md

@@ -1,8 +1,18 @@
 # Typeclasses
 
+The schema, registry, and diagnostic contract for the typeclass
+layer. The resolution/monomorphisation whitepaper lives at
+[models/typeclasses](../models/typeclasses.md); the call-site
+lookup rule at [method dispatch](method-dispatch.md); the built-in
+classes the prelude ships at [prelude classes](prelude-classes.md).
+
 ## Form-A schema (the JSON authoring surface)
 
 Three additive schema extensions; no existing module becomes invalid.
+The canonical schema for `ClassDef`, `InstanceDef`, and the
+`FnDef.type` constraints field lives in
+[Data model](data-model.md); this section is the typeclass-layer
+narrative.
 
 **`ClassDef`** — top-level definition kind, declares a class:
 
@@ -181,7 +191,7 @@ wording is fixed; the categories and their triggers are:
 Cross-class method sharing is structurally legal; ambiguity surfaces
 at the call site via `AmbiguousMethodResolution` or, for class-fn
 name overlap, via the `class-method-shadowed-by-fn` warning. See
-§"Method dispatch" below.
+[Method dispatch](method-dispatch.md).
 
 **Class-schema diagnostics** (validation of class declarations):
 
@@ -222,78 +232,6 @@ There is no `AmbiguousInstance` diagnostic at the registry level —
 coherence (`DuplicateInstance` at registry build, W2) makes
 per-`(class, type)` ambiguity structurally impossible. Cross-class
 method ambiguity is a separate concern resolved at the call site
-via `AmbiguousMethodResolution` (see §"Method dispatch" below).
-
-## Method dispatch
-
-Post-mq.3, dispatch is two-mode:
-
-**Polymorphic call sites** (inside a fn body with `forall` +
-constraint set): the constraint names the class via the qualified
-`Constraint.class` field (canonical-form per mq.1). Synth's
-residual carries the class name directly; constraint-discharge at
-fn-body-end matches against the workspace registry by
-`(class, type_hash)` key.
-
-**Monomorphic call sites**: synth consults the workspace-flat
-`Env.method_to_candidate_classes: BTreeMap<MethodName,
-BTreeSet<QualifiedClassName>>` index, then runs the 5-step
-dispatch rule:
-
-1. Parse the `Term::Var.name` for an optional class qualifier
-   (last-dot-segment is the method name; everything before is the
-   qualified class).
-2. If `method_to_candidate_classes` has no entry for the method
-   name, fall through to the existing Var-arm branches (free fn
-   lookup, dot-qualified cross-module).
-3. Qualifier present: filter candidates to the named class. Empty
-   result fires `UnknownClass`. Singleton survivor proceeds.
-4. Qualifier empty (bare-method form): singleton candidate proceeds
-   directly; multiple candidates yield a multi-candidate residual
-   for discharge-time refinement.
-5. At discharge, refinement runs: concrete `type_` filters
-   candidates via the workspace registry; rigid-var `type_` filters
-   via the active fn's declared constraints
-   (`env.active_declared_constraints`). Single survivor discharges;
-   multiple survivors fire `AmbiguousMethodResolution` (concrete) or
-   `MissingConstraint` (rigid-var); zero survivors fire `NoInstance`
-   (concrete) or `MissingConstraint` (rigid-var).
-
-The `method_to_candidate_classes` index is the load-bearing data
-structure for this routing — its construction in `build_check_env`
-inverts the per-module `class_methods` maps (themselves tuple-keyed
-by `(qualified-class, method)` post-mq.3) to a workspace-flat
-method-name-to-class-set map.
-
-Class-fn collisions resolve at the call site, not at workspace load
-time: the fn lookup precedence (locals → caller-module-fn →
-imported-fn) runs ahead of the class-method branch. When both
-sides have a match, the fn wins and a `class-method-shadowed-by-fn`
-warning surfaces the shadow.
-
-## Prelude (built-in) classes
-
-The prelude 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`. 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.
-
-The prelude ships `class Show a where show : (a borrow) -> Str` and
-primitive `Show Int`, `Show Bool`, `Show Str`, `Show Float`
-instances. Float **is** included in Show (unlike Eq/Ord) — IEEE-754
-makes structural equality and total ordering semantically dubious,
-but textual representation of a Float is well-defined modulo the
-NaN-spelling caveat in §"Float semantics". Each `Show <T>` instance
-body is a single-application lambda invoking the corresponding
-runtime primitive (`int_to_str`, `bool_to_str`, `str_clone`,
-`float_to_str`); no codegen intercept is required. The polymorphic
-helper `print : forall a. Show a => a -> () !IO` has body
-`\x -> let s = show x in do io/print_str s` (explicit let-binder for
-heap-Str RC discipline per eob.1 Str carve-out). The let-binder is
-structurally pinned by `crates/ail/tests/print_mono_body_shape.rs`.
-Routing through `print` is the path for non-`Str` primitives;
-`io/print_str` is the only built-in direct-output effect-op.
+via `AmbiguousMethodResolution` (see [Method dispatch](method-dispatch.md)).
 
 Ratified by: `crates/ail/tests/show_no_instance_e2e.rs`.

design/contracts/verification.md

@@ -4,7 +4,8 @@
 
 1. **Snapshot tests** for the pretty-printer and IR emit. The diff makes
    regressions visible immediately.
-2. **Property tests** for the JSON ↔ pretty-print roundtrip.
+2. **Property tests** for the JSON ↔ pretty-print
+   [roundtrip](roundtrip-invariant.md).
 3. **End-to-end tests** for `examples/` with expected program output.
 4. **Hash stability**: a test ensures the same def always produces the same
    hash.