diff --git a/design/models/0008-ownership-totality.md b/design/models/0008-ownership-totality.md
new file mode 100644
index 0000000..be3dd91
--- /dev/null
+++ b/design/models/0008-ownership-totality.md
@@ -0,0 +1,277 @@
+# Ownership totality — authored own/borrow everywhere whitepaper
+
+**STATUS.** *Design exploration — NOT current state, NOT an approved
+milestone.* Nothing here is shipped; the present surface still has
+`ParamMode::Implicit` as the parser default on both parameters and
+returns. This whitepaper records the **converged shape** of a possible
+direction — the points the design discussion has settled — and isolates
+the genuinely-open questions in §7. The honesty rule
+(`../contracts/0007-honesty-rule.md`) governs the contract ledger, not
+this exploratory model: this file exists precisely to fix a future
+shape before committing it. When a direction here is chosen, it becomes
+one or more specs under `docs/specs/`, and the current-state facts
+migrate into the contract ledger.
+
+---
+
+## 1. The leak that motivates it
+
+A user function whose return **type** is an RC-heap value (`Str`, or a
+boxed ADT) but whose signature omits the ownership mode carries
+`ret_mode == ParamMode::Implicit` — the parser's silent default, which
+nothing infers post-parse. Codegen reads `Implicit` faithfully: the
+caller does **not** `dec` the returned slab, so the owned allocation
+leaks (`live = 1` under `AILANG_RC_STATS`). This is documented
+intentional behaviour today: `../contracts/0008-memory-model.md` states
+`ret_mode` is author-required and never inferred, and the
+`examples/rc_let_implicit_returning_app.ail` fixture asserts `live = 1`
+as correct under the Implicit back-compat lane.
+
+The leak is the symptom. The cause is that an ownership default exists
+at all.
+
+## 2. The principle: ownership is authored, never defaulted
+
+AILang's identity (`../../CLAUDE.md`): *local reasoning — "every
+definition carries its full type and effect set, so a signature can be
+trusted without reading the body"*; *mandatory mode and type
+annotations are kept*; *machine readability over human readability*.
+
+`Implicit` violates that identity head-on. Whether the caller becomes
+the owner of a value crossing a signature boundary — and must free it
+— is **not recoverable from the type alone**: a `Str`-returning `own`
+and a `Str`-returning `borrow` are indistinguishable by type; only the
+mode says who frees. The code makes this concrete: the typechecker
+already treats `Implicit ≡ Own` (`ParamMode::mode_eq`,
+`crates/ailang-core/src/ast.rs`), yet codegen reads `Implicit`
+separately and omits the caller `dec`. The *same* fn-type is read two
+ways depending on whether one knows codegen's special-casing — exactly
+the trust break local reasoning exists to forbid.
+
+So the principle is: **ownership is authored, never defaulted.**
+
+This admits no half-application. A default cannot be partially removed:
+closing the Implicit lane on *returns* while leaving it open on
+*parameters* is the same default surviving on the input side;
+mandating a mode where it is meaningful (heap returns) while permitting
+it where it looks vacuous (a by-value `Int`) is a rule that forces
+truth in one direction and tolerates noise in the other. Totality is
+the only coherent stopping point: **`Implicit` is removed from the
+authorable surface, and every parameter and every return on every
+signature carries `own` or `borrow`.** There is no defaulted position
+anywhere.
+
+## 3. The shape: totality with a binary mode
+
+### 3.1 The polarity reframe (so the author needs no RC knowledge)
+
+The objection to totality is "now the author must know which types are
+heap." The reframe dissolves it: **`own` is the universal default;
+`borrow` is what implies aliasable (heap) data.**
+
+- `own` means "ownership is handed to the caller." For a fresh heap
+  allocation, the caller now frees it. For a by-value `Int`, ownership
+  of the copy is trivially the caller's — `own` is correct, just
+  trivially true.
+- `borrow` means "this is a view into data owned upstream; the caller
+  must not free it." You can only lend a view of something aliasable,
+  which presupposes heap data. So `(borrow (con Int))` is an **error**
+  — a value type has nothing to lend.
+
+The author's whole rule is then pure dataflow about their own body,
+with zero knowledge of the RC representation: **default to `own`; reach
+for `borrow` only when you are reading or passing through a value you
+were lent.** Every position has an answer — it is always either "I take
+it" (`own`) or "I lend/read it" (`borrow`); no position has `Implicit`
+as its uniquely-correct authored answer.
+
+### 3.2 Value types: trivial-`own`, `borrow` is an error
+
+Every position carries a mode, including value-type positions — the
+surface stays uniform. Over a by-value type (`Int`, `Float`, `Bool`),
+`own` is trivially true and `borrow` is a `check` error. This is chosen
+over the alternative (value-type positions take no mode slot at all)
+deliberately: forbidding the slot would re-introduce exactly the
+RC-representation knowledge the polarity reframe removes (the author
+would have to know which types are heap to know which positions take a
+mode), and it would make the surface non-uniform. For an LLM author,
+uniform structure beats the saving of a trivially-true token: the model
+is not burdened by the token, it is burdened by a conditional rule.
+
+The mode on a value-type position therefore carries no runtime
+information (`live = 0` regardless); it is the forced, only-legal
+`own`. This is the price of uniformity, named honestly.
+
+### 3.3 `ParamMode` is binary
+
+`ParamMode` becomes `{Own, Borrow}` — `Implicit` is deleted. Modes stay
+metadata fields on `Type::Fn` (`param_modes`, `ret_mode`), not new
+`Type` variants, preserving the 18a locality decision (modes belong to
+fn-parameter positions, not to types in general). There is **no** mode
+variable and **no** third polymorphic axis — see §4.
+
+## 4. Fixed modes suffice — why there is no mode-polymorphism
+
+A natural objection: passthrough functions — `id`, projections, `apply`
+— have a return whose ownership *is* the input's. Surely those need a
+mode variable (`id : (m a) -> (m a)`)? They do not, and the reasoning
+is load-bearing enough to state in full, because a reader will reach
+for mode-polymorphism on sight.
+
+### 4.1 Totality does not require mode-polymorphism
+
+Every position — **including a position over a type variable** — takes
+a concrete authored `own`/`borrow`. `fst : forall a b. (borrow (Pair a
+b)) -> (borrow a)` is total and hole-free: the `(ret (borrow a))` is an
+honest fixed claim ("I return a borrowed view"). A type-variable
+position is therefore never a *hole* under fixed modes; it simply
+commits the function to one mode. What a mode variable would buy is not
+totality but the removal of *duplication* — one definition serving an
+`own`-instantiation and a `borrow`-instantiation at once. The two
+notions must not be conflated: "cannot express passthrough with one
+definition" is not "cannot express anything."
+
+### 4.2 The reuse-across-modes need is confined to cut or better-split cases
+
+A single definition needs to serve both an `own`- and a
+`borrow`-instantiation only in two places:
+
+- **Higher-order routing combinators** (`compose`, `apply`, `id` as a
+  function argument, `twice`/`iterate` over an endofunction). Here the
+  seam modes must thread through, and one definition would have to
+  cover every mode combination. But these are **point-free style** —
+  cut by the language identity as human-attractive but LLM-neutral. The
+  duality bites only in code AILang does not have.
+
+- **The consume-vs-preserve container duality** (`map`/`filter`/`find`
+  applied to a container you discard vs. one you keep). This duality is
+  real, but it is a **meaningful semantic distinction the author should
+  state** — "do I destroy my input?" — not a routing detail to abstract
+  behind a variable. Expressing it as two named functions (a
+  borrow-reading variant and an owning-consuming variant) keeps the
+  decision explicit; a mode variable would *hide* it. This is an
+  argument against mode-polymorphism even where it technically applies.
+
+### 4.3 The structural reason it does not bite
+
+AILang's iteration idiom is **named tail-recursion** (`tail-app`, e.g.
+`examples/bench_compute_collatz.ail`), not a passed-function combinator
+like `iterate f n`. Owning accumulation — state stepping, fixpoint
+normalisation, fold-like loops — is written as a function recurring on
+itself with accumulator parameters. The own/borrow clash at a
+higher-order slot needs a *reused function-argument combinator*, which
+the language does not reach for. A survey of the canonical
+higher-order functions confirms each has a single determinate mode
+slot:
+
+| HOF | Mode slot | Reuse-across-modes clash? |
+|---|---|---|
+| `map f xs` | `f : (borrow a) -> (own b)`, reads the list | no — owning-consume is a separate optimisation, and RC lets an owner lend to the borrow form |
+| `filter p xs` | `p : (borrow a) -> Bool`, consumes input | no |
+| `fold f acc xs` | `f : (own acc) (borrow a) -> (own acc)` | no — a borrow-accumulator is meaningless |
+| `find p xs` | `p : (borrow a) -> Bool`, returns `(borrow a)` view | no |
+| `any`/`all p xs` | `p : (borrow a) -> Bool` | no |
+| `zipWith f xs ys` | reads elements, builds fresh | no |
+| `id`/`compose`/`apply`/`const`/`flip` | passthrough/seam modes | point-free — cut |
+| `iterate`/`twice` | borrow-navigation (`twice tail`); owning goes via `tail-app` | no |
+
+### 4.4 The authoring rule that replaces mode-polymorphism
+
+The discipline leans entirely on features the language already has:
+
+1. **Named projection / view → `borrow`.** `fst`, `snd`, field
+   accessors, `tail` return borrowed views.
+2. **Owning extraction → `match`.** Taking a piece and discarding the
+   rest is the primitive destructure: `match` transfers ownership of
+   bound components and drops the rest. No named owning-projection is
+   needed.
+3. **Ownership recovery from a borrowed view → explicit `clone`.**
+
+`ParamMode` stays binary; "every position carries a concrete
+`own`/`borrow`" holds literally, with no third-axis footnote.
+
+## 5. Two orthogonal axes: totality vs soundness
+
+These must not be conflated:
+
+- **Totality** (every position carries an authored mode; no `Implicit`,
+  no exemption). The *declaration* axis. It admits no holes. Because
+  "remove a default" is an atomic cutover (you cannot half-remove
+  `Implicit`), totality lands as one coherent step over the whole
+  surface.
+
+- **Soundness / verification** (the authored `own`/`borrow` is checked
+  against the body's actual ownership flow). The *correctness* axis. It
+  *may* phase: a mandatory-but-unverified mode (require-and-trust) is a
+  **soundness** gap, not a **totality** hole.
+
+The parameter side is already on the verification axis today:
+`consume-while-borrowed` rejects a consumed `borrow` param,
+`over-strict-mode` warns on a never-consumed `own` param, and the
+uniqueness pass computes per-param `consume_count`. So extending
+totality to *parameters* lands on already-verified ground and is
+**compiler-assisted** — the existing consume analysis can derive and
+propose each parameter's correct mode. The *return* side is the half
+with no verification yet; it needs new return-provenance ("escape")
+analysis.
+
+## 6. Costs and consequences (named honestly)
+
+- **Total migration.** Every signature in the corpus and prelude gains
+  explicit modes on every position. Mechanical for a controlled
+  single-author corpus, and compiler-assisted for parameters via the
+  existing consume analysis; still large.
+
+- **Canonical-form / hash reset.** The hashable canonical JSON omits
+  `param_modes` / `ret_mode` *while they are all `Implicit`*
+  (`skip_serializing_if`, `crates/ailang-core/src/ast.rs`), precisely
+  to keep pre-mode-annotation modules bit-identical. Remove `Implicit`
+  and every signature carries explicit modes → **every module hash
+  shifts**, once, across the whole corpus, and every hash-pin test
+  resets. This is the one genuinely irreversible consequence and the
+  one to sign off on deliberately.
+
+- **The dangerous failure mode motivates the verification axis.** Under
+  require-and-trust, the asymmetry of wrong annotations matters: a
+  wrong `borrow` (declared borrow, actually fresh) merely *leaks*; a
+  wrong `own` (declared own, actually a borrowed alias) makes the
+  caller `dec` data it does not own → **double-free / use-after-free**.
+  Totality pushes authors toward `own` as the default — the more
+  dangerous direction — so the return-side `own`-verification (the
+  first-order "is this return actually fresh?" check) is the
+  highest-value piece of the soundness axis.
+
+What is **not** a cost: mode-polymorphism. Dropping it (§4) removes
+mode variables, mode unification, and call-site instantiation from the
+scope entirely — a saving, not a debt.
+
+## 7. Open questions
+
+1. **Cutover shape.** `Implicit`-removal is atomic (you cannot
+   half-remove a default), so the first shippable state carries uniform
+   modes + full migration. Without mode-polymorphism the step is
+   smaller than the original cluster, but is there any hole-free
+   *smaller* increment, or is the cutover irreducibly one large step?
+   (Working hypothesis: irreducible.)
+
+2. **Verification sequencing.** Is require-and-trust an acceptable
+   interim on the soundness axis, given the double-free risk of a wrong
+   `own`? Or should return-side `own`-verification land *with* the
+   totality cutover rather than after it?
+
+3. **Naming.** If this lands, the glossary should pin the vocabulary
+   (mode, `own`/`borrow`, trivial-`own`, the projection/extraction/clone
+   rule) before drift sets in.
+
+**Resolved by the converged shape above** (no longer open): re-scope to
+totality (§2), value-type mode policy → trivial-`own` (§3.2),
+mode-polymorphism → not adopted; fixed modes suffice (§4).
+
+---
+
+*Cross-references:* memory model
+`../contracts/0008-memory-model.md` (current `param_modes`/`ret_mode`
+contract, the `over-strict-mode` / `consume-while-borrowed`
+machinery); RC + uniqueness whitepaper `0004-rc-uniqueness.md`; the
+fieldtest that surfaced the leak
+`../../docs/specs/0061-fieldtest-typed-mir.md`.