docs(ledger): fix two coherence gaps surfaced by the project skim

A read-only coherence skim across the project (the contract edits
themselves verified code-true, INDEX bijection exact, all pins green)
surfaced two pre-existing drifts — both predating this audit, neither
from the contract pass. Fixed in the same conservative style.

1. Model 0008 (ownership-totality) §1+§2 narrated the `Implicit`
   leak in the PRESENT tense, contradicting the file's own STATUS
   header (Implicit deleted via #55, 76b21c0), contract 0008 ("There
   is no `Implicit`"), and the live fixture. §1 claimed "This is
   documented intentional behaviour today ... the fixture asserts
   `live = 1`"; the `rc_let_implicit_returning_app.ail` fixture now
   asserts `live = 0` (its own comment marks the `live = 1` lane as
   "Pre-0062"). §2 claimed "the typechecker already treats
   `Implicit ≡ Own` (`ParamMode::mode_eq`)"; that variant and fn no
   longer exist. Rewrote both to past tense (the leak the cutover
   fixed). The STATUS header had been updated at cutover; these two
   bodies had not. The design argument (§2-§8) is untouched — the
   header frames it as the whitepaper's reasoning and points readers
   to the contract for current state.

2. Contract 0010 (scope-boundaries) referenced 18 example fixtures as
   `examples/*.ail.json` — files that exist only as `.ail` since the
   form-A-default migration (JSON is derived in-process; only the
   twelve carve-outs remain `.ail.json` on disk). All 18 → `.ail`
   (every target verified present). Same single stale file-path ref in
   model 0001 §3 (`list_map_poly`) corrected; model 0001's other two
   `.ail.json` mentions are intentional references to the canonical
   JSON *form* (the whitepaper's subject) and were left.

Honesty sweep clean; design_index_pin / docs_honesty_pin /
effect_doc_honesty_pin green; no dangling example path remains.

design/contracts/0010-scope-boundaries.md

@@ -101,12 +101,12 @@ What **is** supported (and used as the smoke test for the pipeline):
   cover `Int` / `Bool` / `Str` / `Unit`; `Float` lit-patterns are
   hard-rejected at typecheck (`CheckError::FloatPatternNotAllowed`,
   see [float-semantics](0005-float-semantics.md)). `(pat-lit "hi")` over
-  a `Str` scrutinee is exercised by `examples/eq_demo.ail.json`.
+  a `Str` scrutinee is exercised by `examples/eq_demo.ail`.
 - **Imports + qualified cross-module references** via dotted names.
   Extends to **types and constructors**: a foreign
   module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as
   `(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`)
+  inside that scrutinee. Std-library demos (`examples/std_*_demo.ail`)
   exercise this end-to-end.
 - **AI-authoring text surface, form (A)** (see
   [authoring surface](0001-authoring-surface.md)). The `ailang-surface`
@@ -127,7 +127,7 @@ What **is** supported (and used as the smoke test for the pipeline):
   "Per-fn arena via stack `alloca`" subsection of
   [RC + uniqueness](../models/0004-rc-uniqueness.md). The per-fn-arena
   path is exercised end-to-end by
-  `examples/escape_local_demo.ail.json`.
+  `examples/escape_local_demo.ail`.
 - **First-class function references.** A top-level fn name (or
   qualified `prefix.def`) used as a `Term::Var` is a fn-value.
 - **Anonymous lambdas with capture.** `Term::Lam` constructs a
@@ -156,36 +156,36 @@ What **is** supported (and used as the smoke test for the pipeline):
   rather than a silent fallback to `ptr`.
 Pipeline regression smoke tests:
 
-- `examples/sum.ail.json` → prints 55 (recursion, arithmetic).
+- `examples/sum.ail` → prints 55 (recursion, arithmetic).
-- `examples/list.ail.json` → prints 42 (ADTs + match).
+- `examples/list.ail` → prints 42 (ADTs + match).
-- `examples/hof.ail.json` → prints 42 (first-class fn-refs, indirect call).
+- `examples/hof.ail` → prints 42 (first-class fn-refs, indirect call).
-- `examples/closure.ail.json` → prints 42 (lambda capturing a let-bound var).
+- `examples/closure.ail` → prints 42 (lambda capturing a let-bound var).
-- `examples/list_map.ail.json` → prints 2/4/6 (ADTs + closure + recursive
+- `examples/list_map.ail` → prints 2/4/6 (ADTs + closure + recursive
   HOF + IO; the dogfood smoke test).
-- `examples/sort.ail.json` → prints sorted [3,1,4,1,5,9,2,6,5,3,5]
+- `examples/sort.ail` → prints sorted [3,1,4,1,5,9,2,6,5,3,5]
   one-per-line (insertion sort over an 11-element list).
-- `examples/poly_id.ail.json` → prints 42 then "true" (polymorphic
+- `examples/poly_id.ail` → prints 42 then "true" (polymorphic
   identity at `Int` and `Bool`; two specialised fns emitted).
-- `examples/poly_apply.ail.json` → prints 42 (polymorphic `apply`
+- `examples/poly_apply.ail` → prints 42 (polymorphic `apply`
   with a fn-typed parameter; `apply(succ, 41)`).
-- `examples/box.ail.json` → prints 42 (parameterised ADT round-
+- `examples/box.ail` → prints 42 (parameterised ADT round-
   trip: `MkBox(42)` constructed, then projected by a polymorphic
   `unbox : forall a. (Box<a>) -> a` and printed).
-- `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match
+- `examples/maybe_int.ail` → prints 7 then 99 (pattern match
   over `Maybe<Int>`: `or_else(Some(7), 99)` then
   `or_else(None, 99)`).
-- `examples/std_list_demo.ail.json` → exercises
+- `examples/std_list_demo.ail` → exercises
   `std_list`'s combinators (length, sum, reverse, take/drop-style
   uses) end-to-end against `std_list`'s `List<a>`.
-- `examples/std_maybe_demo.ail.json` → exercises `std_maybe`
+- `examples/std_maybe_demo.ail` → exercises `std_maybe`
   combinators over `Maybe<Int>`, including `from_maybe` and `map`.
-- `examples/std_either_demo.ail.json` → first program with
+- `examples/std_either_demo.ail` → first program with
   three distinct type variables in a single fn (the `either`
   eliminator), monomorphised six different ways in the IR.
-- `examples/std_pair_demo.ail.json` → drives every
+- `examples/std_pair_demo.ail` → drives every
   `std_pair` combinator (fst, snd, swap, map_first, map_second);
   expected output 7, 9, 9, 7, 8, 18.
-- `examples/nested_pat.ail.json` → first program to use a
+- `examples/nested_pat.ail` → first program to use a
   nested `(pat-ctor Cons a (pat-ctor Cons b _))`; the desugar pass
   flattens it into a chain that the existing flat-match codegen
   consumes. Prints 30 for a 3-element input list.

design/models/0001-authoring-surface.md

@@ -2,7 +2,7 @@
 
 ## Candidate notations (same `map` encoded in each)
 
-The reference target — the polymorphic `map` from `examples/list_map_poly.ail.json`:
+The reference target — the polymorphic `map` from `examples/list_map_poly.ail`:
 
 ```
 data List a where Nil | Cons a (List a)

design/models/0008-ownership-totality.md

@@ -33,21 +33,21 @@ the sharpened §7 questions, and §8 (relation to Rust).*
 
 ---
 
-## 1. The leak that motivates it
+## 1. The leak that motivated it
 
-A user function whose return **type** is an RC-heap value (`Str`, or a
+A user function whose return **type** was an RC-heap value (`Str`, or a
-boxed ADT) but whose signature omits the ownership mode carries
+boxed ADT) but whose signature omitted the ownership mode carried
 `ret_mode == ParamMode::Implicit` — the parser's silent default, which
-nothing infers post-parse. Codegen reads `Implicit` faithfully: the
+nothing inferred post-parse. Codegen read `Implicit` faithfully: the
-caller does **not** `dec` the returned slab, so the owned allocation
+caller did **not** `dec` the returned slab, so the owned allocation
-leaks (`live = 1` under `AILANG_RC_STATS`). This is documented
+leaked (`live = 1` under `AILANG_RC_STATS`). The #55 cutover removed
-intentional behaviour today: `../contracts/0008-memory-model.md` states
+this lane: `../contracts/0008-memory-model.md` now requires an explicit
-`ret_mode` is author-required and never inferred, and the
+author-supplied `ret_mode`, and the
-`examples/rc_let_implicit_returning_app.ail` fixture asserts `live = 1`
+`examples/rc_let_implicit_returning_app.ail` fixture asserts `live = 0`
-as correct under the Implicit back-compat lane.
+(the returned cell frees at the call site).
 
-The leak is the symptom. The cause is that an ownership default exists
+The leak was the symptom. The cause was that an ownership default
-at all.
+existed at all.
 
 ## 2. The principle: ownership is authored, never defaulted
 
@@ -60,12 +60,11 @@ annotations are kept*; *machine readability over human readability*.
 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
+mode says who frees. The code made this concrete: the typechecker
-already treats `Implicit ≡ Own` (`ParamMode::mode_eq`,
+treated `Implicit ≡ Own`, yet codegen read `Implicit` separately and omitted the
-`crates/ailang-core/src/ast.rs`), yet codegen reads `Implicit`
+caller `dec`. The *same* fn-type was read two ways depending on
-separately and omits the caller `dec`. The *same* fn-type is read two
+whether one knew codegen's special-casing — exactly the trust break
-ways depending on whether one knows codegen's special-casing — exactly
+local reasoning exists to forbid.
-the trust break local reasoning exists to forbid.
 
 So the principle is: **ownership is authored, never defaulted.**