docs(policy): fill in trusted-base policy — Lean + Idris2 OWED + #211 cross-link (#222)

## Summary
Fills three gaps in the trusted-base reduction policy (standards#203,
merged) so per-repo proof-debt triage prompts can classify cleanly:

- **Idris2 `||| OWED:` + `0`-multiplicity form** added as the canonical
axiom annotation (disposition (c)). Distinguishes proof-only
declarations from the run-time `believe_me` form already documented
under (b).
- **Lean annotation block** added (was missing). Shows `axiom` for
necessary-axiom (c) and named `sorry` for debt (d).
- **Marker disambiguation**: `TRUSTED:` (run-time soundness break /
(b)), `AXIOM:` (named top-level axiom / (c)), `OWED:` (erased /
cross-language debt / (c) or (d)).
- **Enforcement section** rewired to cross-link standards#211 (merged)
with the concrete script path, marker set, and 5-line annotation window
— replacing the "future PR" placeholder.
- **Status table** updated: #203 merged, #211 merged, #213 seeded
`standards`' own `proof-debt.md`. `:status:` PROPOSED → ADOPTED.
- Companion documents expanded to link #211 and #213.

## Why
The per-repo proof-debt triage prompts queued behind this (followup
chain #8/#9/#10) need a concrete classification grammar and annotation
syntax for every prover the estate uses. Without the Lean example, the
OWED erased form, and the cross-link to the actual enforcement script,
the prompts fall back to ad-hoc judgment per repo and the trusted base
won't shrink coherently.

## Scope
Single doc file; no code, no CI changes. The Companion PRs (#211
enforcement, #213 schema-example seed) have already merged — this is
purely the in-policy fill-in those merges enabled.

## Test plan
- [ ] Asciidoctor render is well-formed (no broken cross-refs, source
blocks close).
- [ ] `scripts/check-trusted-base.sh` on a sample repo recognises
`OWED:`, `TRUSTED:`, and `AXIOM:` markers as documented (already
verified per #211 PR body).
- [ ] CI green on PR.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/TRUSTED-BASE-REDUCTION-POLICY.adoc

@@ -1,11 +1,12 @@
 // SPDX-License-Identifier: MPL-2.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
 = Trusted-Base Reduction Policy
-:revdate: 2026-05-26
-:status: PROPOSED
+:revdate: 2026-05-27
+:status: ADOPTED
 :audit: hyperpolymath/standards#195
 :audit-licence: hyperpolymath/standards#196
 :audit-docs: hyperpolymath/standards#197
+:enforcement: hyperpolymath/standards#211
 :precedent: hyperpolymath/boj-server backend-assurance harness
 
 This document is the canonical estate-wide policy for managing
@@ -129,6 +130,41 @@ wasm_marshal_u64 : Bits64 -> ByteArray
 wasm_marshal_u64 x = believe_me ...
 ----
 
+For Idris2 *axioms* (disposition (c)), prefer the canonical form: a
+doc-comment header (`|||`) starting with `OWED:` and a `0`-multiplicity
+(erased) declaration. The erased multiplicity makes the term proof-only —
+it cannot escape into runtime code and disappears from compiled output —
+so the unproven assumption is structurally scoped to type-level reasoning:
+
+[source,idris]
+----
+||| OWED: function extensionality at the typed-wasm export interface.
+||| Necessary; not derivable in Idris2 0.8.0 without UIP.
+||| See docs/proof-debt.md §(c) entry "funExtTW".
+||| Citation: echo-types `Echo.FunExt`, Mathlib4 `Function.funext_iff`.
+0 funExtTW : (f, g : a -> b) -> ((x : a) -> f x = g x) -> f = g
+----
+
+The `OWED:` token is recognised by `scripts/check-trusted-base.sh`
+alongside `TRUSTED:` and `AXIOM:`. Use `OWED:` for proof-only erased
+declarations (Idris2 0-multiplicity, Coq `Axiom`-of-Prop, Lean `axiom` in
+`Prop`) and `TRUSTED:` for run-time soundness breaks (`believe_me`,
+`unsafePerformIO`, `unsafe`).
+
+[source,lean]
+----
+-- AXIOM: function extensionality; necessary; see docs/proof-debt.md §(c).
+--   Citation: Mathlib4 `Function.funext_iff` (commit abc1234).
+axiom funExt {α β : Type} (f g : α → β) :
+  (∀ x, f x = g x) → f = g
+
+-- For debt-style markers (disposition (d)), prefer the named sorry:
+-- DEBT: substitution preservation; owner @maintainer; deadline 2026-08-01.
+--   See docs/proof-debt.md §(d) entry "subst_preservation".
+theorem subst_preservation : ∀ {Γ τ e e'}, Subst e e' → Typed Γ e τ → Typed Γ e' τ :=
+  sorry
+----
+
 [source,coq]
 ----
 (* AXIOM: function extensionality.
@@ -145,25 +181,51 @@ postulate
   ∥_∥ : Set → Set
 ----
 
-The leading-comment marker (`TRUSTED:` / `AXIOM:`) is itself part of the
-contract — the audit script in section "Enforcement" below greps for it.
+The leading-comment marker (`TRUSTED:` / `AXIOM:` / `OWED:`) is itself
+part of the contract — the audit script in section "Enforcement" below
+greps for it. Choose the marker by run-time vs proof-time scope:
+
+* `TRUSTED:` — run-time soundness break (`believe_me`, `unsafe`,
+  `unsafePerformIO`, `assume val`, `:axiom`). Pair with disposition (b)
+  BUDGETED and a property-test budget.
+* `AXIOM:` — top-level named axiom (Coq `Axiom`, Lean `axiom`, Agda
+  `postulate`). Pair with disposition (c) NECESSARY AXIOM and a
+  citation.
+* `OWED:` — Idris2-style erased (`0`-multiplicity) axiom or any
+  cross-language self-documented debt marker. Pair with either (c)
+  NECESSARY AXIOM (with citation) or (d) DEBT (with deadline and
+  owner).
 
 == Enforcement
 
-A future PR will wire `scripts/check-trusted-base.sh` into
-`governance-reusable.yml`. The script:
-
-. Counts every soundness-relevant escape hatch in the caller repo.
-. Verifies each is either preceded by a `TRUSTED:` or `AXIOM:` comment,
-  OR enumerated in `docs/proof-debt.md`.
+Enforcement landed at link:{enforcement}[standards#211] as
+`scripts/check-trusted-base.sh`, wired into `governance-reusable.yml`
+as a `trusted-base` job. The script:
+
+. Greps every soundness-relevant escape hatch in the caller repo
+  (`Axiom`, `Admitted`, `admit.`, `axiom`, `sorry`, top-level `postulate`,
+  `believe_me`, `really_believe_me`, `assert_total`, top-level `partial`,
+  `assume val`, `admit_p`, `:axiom`, plus cross-language `TODO PROOF` /
+  `OWED:` / `FIXME PROOF` markers in soundness-relevant positions).
+. Verifies each is either preceded within 5 lines by a `TRUSTED:`,
+  `AXIOM:`, or `OWED:` leading comment, OR enumerated by path in
+  `docs/proof-debt.md` (or `.adoc`).
 . Fails CI when a marker is naked (no annotation AND no proof-debt.md
   entry).
-. Optionally fails CI when `docs/proof-debt.md` §(d) DEBT entries are
-  past their deadline.
+. No-ops cleanly on repos with zero proof-bearing files (true for most
+  of the estate).
+
+A follow-up may extend it to fail CI when `docs/proof-debt.md` §(d) DEBT
+entries are past their stated deadline.
+
+This is the same shape as `check-licence-consistency.sh` (standards#201)
+— local script, called from the governance bundle, no network
+dependencies.
 
-This is the same shape as `check-licence-consistency.sh`
-(standards#201) — local script, called from the governance bundle, no
-network dependencies.
+The seed `docs/proof-debt.md` for the `standards` repo itself landed at
+standards#213 as the canonical example of the schema in action (15
+markers triaged, 11 §(d) entries with named owners and discharge
+recipes).
 
 == Precedent: boj-server backend-assurance harness
 
@@ -193,10 +255,10 @@ first (rough P0/P1/P2 ordering):
 
 | P0 | `ephapax`             | 1 `Admitted` in `formal/Semantics.v` (`preservation`); was 3 at audit time, 2 discharged via https://github.com/hyperpolymath/ephapax/pull/146[ephapax#146]. Discharge plan in `ROADMAP.adoc` § "Preservation closure plan" + `formal/PRESERVATION-DESIGN.md` (four-layer redesign on branch `proof/l1-region-threading-design`). Migration filed: https://github.com/hyperpolymath/ephapax/pull/164[ephapax#164].
 | P0 | `boj-server`          | Reference implementation — formalise the existing harness as the canonical example.
-| P1 | `absolute-zero`       | 72 Coq + 315 Lean markers across 6638 proof files; needs the schema before any single-repo close-out is tractable.
+| P1 | `absolute-zero`       | Phase-1 triage MERGED via https://github.com/hyperpolymath/absolute-zero/pull/58[absolute-zero#58] + https://github.com/hyperpolymath/absolute-zero/pull/59[#59]: **72 Coq Axioms classified** (52 §(c) + 17 §(a)-backlog + 3 §(b)). Remaining outside Phase 1: **52 Lean `axiom` decls + 7 Idris2 `postulate`s + 124 Lean `sorry`s** (canonical count via `check-trusted-base.sh`; the audit-time "315 Lean across 6638 proof files" figure was debunked — no source reproduces 315). Phase 2 work tracked in absolute-zero.
 | P1 | `maa-framework`       | 134 markers in 25 files (high density); investigate whether vendored or original.
 | P1 | `betlang`             | Single named axiom (`substTop_preserves_typing`) — clean (b) or (c) classification.
-| P1 | `proven`              | 372 `TODO PROOF` markers; convert to §(d) entries with deadlines.
+| P1 | `proven`              | Real debt surface (per Phase-1 triage 2026-05-27, `docs/proof-debt-triage.md`): **280 `\|\|\| OWED:` annotations** across 44 `Proofs.idr` modules (Fork A form), **4 `@ Assumed:` postulate tags** in `src/Proven/SafeDigest.idr` (needs migration to Fork A), and **~70 `Safe*.idr` modules** with `Prevents:`/`Guarantees:` overclaim docs and no discharged theorem. ("372 `TODO PROOF`" from the original audit prompt does not match the codebase — the string `TODO PROOF` is absent; 280 OWED is the canonical count.)
 | P2 | `standards`           | 4 Agda postulate + 11 Idris partial — set the example for downstream.
 | P2 | `typed-wasm`, `stapeln`, `vcl-ut`, `hypatia`, `snifs`, `somethings-fishy` | Each 5–15 `believe_me`; audit and classify in a single PR each.
 |===
@@ -207,14 +269,18 @@ first (rough P0/P1/P2 ordering):
 |===
 | Date | Event
 
-| 2026-05-26 | Policy filed (standards#202).
-| TBD       | `scripts/check-trusted-base.sh` filed (separate PR).
-| TBD       | Per-repo `docs/proof-debt.md` files seeded across P0 repos.
+| 2026-05-26 | Policy filed and merged (standards#203).
+| 2026-05-26 | `scripts/check-trusted-base.sh` filed and merged (standards#211); wired into `governance-reusable.yml` as the `trusted-base` job.
+| 2026-05-26 | Seed `docs/proof-debt.md` landed for `standards` itself (standards#213) as the schema reference.
+| 2026-05-27 | Fill-in pass: Idris2 `OWED:` + 0-multiplicity form, Lean annotation block, Enforcement cross-link to #211 (this PR). Status promoted from PROPOSED → ADOPTED.
+| TBD       | Per-repo `docs/proof-debt.md` files seeded across P0/P1 repos via the triage prompts that this policy unblocks.
 |===
 
 == Companion documents
 
 * link:{audit}[standards#195] — estate proof-debt audit (the empirical motivation)
 * link:{audit-licence}[standards#196] — estate licence-debt audit
 * link:{audit-docs}[standards#197] — estate documentation-debt audit
-* `scripts/check-licence-consistency.sh` (standards#201) — the precedent for the eventual `check-trusted-base.sh`
+* link:{enforcement}[standards#211] — `scripts/check-trusted-base.sh` and the `trusted-base` job in `governance-reusable.yml`
+* https://github.com/hyperpolymath/standards/pull/213[standards#213] — seed `docs/proof-debt.md` for the `standards` repo itself (canonical schema example)
+* `scripts/check-licence-consistency.sh` (standards#201) — the structural precedent for `check-trusted-base.sh`