fix(governance): document Fidelity postulates for the Trusted-base reduction policy

#218 merged with the `governance / Trusted-base reduction policy` check
red — its 3 Fidelity postulates were undocumented escape hatches, so
the gate now fails on main and blocks subsequent PRs. The policy
(standards/scripts/check-trusted-base.sh) is satisfied by an inline
TRUSTED:/AXIOM: leading comment OR enumeration in docs/proof-debt.md.
Both applied:

  * Fidelity.agda — each of bh-notation / denotation /
    ordinal-upper-bound gets an `AXIOM:` leading comment immediately
    above its `postulate` (honest text: OPEN proof-debt for order-type
    fidelity D-2026-06-14, NOT a permanently accepted axiom).
  * docs/proof-debt.md — the three enumerated under (d) DEBT — actively
    to be closed, with classification, quarantine scope, and citations
    (D-2026-06-14 + Fidelity-OPEN-postulates.md).

No proof content changed; no status surface changed (appendix /
decision-log / roadmap still read "order-type fidelity OPEN").
Fidelity typechecks; guardrail green.

https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE

Author: claude

docs/proof-debt.md

@@ -36,8 +36,30 @@ under one of (a) discharged / (b) budgeted / (c) necessary axiom / (d) debt.
 
 ## (d) DEBT — actively to be closed
 
-- (none — the kernel is `--safe --without-K` clean; all
-  `…Postulated` modules are intentionally scoped to (c).)
+- `proofs/agda/Ordinal/Buchholz/Fidelity.agda` — three top-level
+  `postulate`s forming the trust boundary of the **order-type fidelity
+  scaffold** (open problem `D-2026-06-14`,
+  `docs/echo-types/decisions/ordinal-bh-order-type-fidelity-open.adoc`):
+  - `bh-notation` — assumed checked Bachmann–Howard order structure.
+  - `denotation` — assumed faithful, height-preserving order-embedding
+    `⟦·⟧ : BT → 𝒪` (the missing object; **not** `rank2`, which
+    deliberately collapses heights and is a termination measure only).
+  - `ordinal-upper-bound` — the `⟦·⟧`-level upper half of the sandwich
+    (downstream of `denotation`).
+  - **Classification**: DEBT, to be discharged when order-type fidelity
+    is proved — these are *not* permanently-accepted axioms. Each is
+    annotated inline with an `AXIOM:` leading comment.
+  - **Justification / scope**: the module is quarantined — `--without-K`
+    only, NOT imported by `All.agda` / `Smoke.agda` — so the `--safe`
+    kernel cone depends on none of these. Nothing in the module asserts
+    that order type ψ₀(Ω_ω) is *proven*; the status surfaces (appendix,
+    decision log, roadmap) read "written at WF milestone; order-type
+    fidelity OPEN".
+  - **Citation**: `D-2026-06-14`; full per-postulate spec (statement /
+    what closes it / owner) in `Fidelity-OPEN-postulates.md`.
+  - **Guardrail status**: allow-listed in `tools/check-guardrails.sh`
+    (`EXPLORATORY_EXEMPT`) and the inline `hypatia: allow` pragma at the
+    module head.
 
 ## Notes
 

proofs/agda/Ordinal/Buchholz/Fidelity.agda

@@ -126,6 +126,7 @@ record DenotesBH (N : BHNotation) : Set where
 -- TRUST BOUNDARY #1. Supplying a checked Bachmann–Howard structure is
 -- external mathematics (owner / external). This postulate is the
 -- assumption that such a structure exists; nothing here constructs it.
+-- AXIOM: bh-notation — assumed; OPEN proof-debt for order-type fidelity (D-2026-06-14); see docs/proof-debt.md (d) + Fidelity-OPEN-postulates.md. NOT a permanently accepted axiom — a hole to be discharged.
 postulate
   bh-notation : BHNotation
 
@@ -134,6 +135,7 @@ open BHNotation bh-notation
 -- TRUST BOUNDARY #2. The faithful, height-preserving denotation is the
 -- missing object. This postulate assumes it exists; this module makes
 -- its absence typed, not filled.
+-- AXIOM: denotation — assumed; OPEN proof-debt for order-type fidelity (D-2026-06-14); see docs/proof-debt.md (d) + Fidelity-OPEN-postulates.md. NOT a permanently accepted axiom — a hole to be discharged.
 postulate
   denotation : DenotesBH bh-notation
 
@@ -161,6 +163,7 @@ fidelity-lower = BH , (BH-wf , pins-BH)
 -- proved for real; the step from that shadow to this ⟦·⟧-level bound
 -- is the height calculation through a real `⟦·⟧`, available once
 -- `denotation` is discharged.
+-- AXIOM: ordinal-upper-bound — assumed; OPEN proof-debt for order-type fidelity (D-2026-06-14); see docs/proof-debt.md (d) + Fidelity-OPEN-postulates.md. NOT a permanently accepted axiom — a hole to be discharged.
 postulate
   ordinal-upper-bound : ∀ {t} → WfBT t → ¬ (bh-height <𝒪 ⟦ t ⟧)