docs: enumerate exploratory truncation postulates in docs/proof-debt.md (#172)

## Summary

- Adds `docs/proof-debt.md` enumerating the repo's sole
soundness-relevant escape hatch under Disposition (c) NECESSARY AXIOM
- Closes the recurring `governance / Trusted-base reduction policy` red
check estate-wide (consistently failing on echo-types main + every PR
since policy adoption)
- No code changes, no new postulates, no `.trusted-base-ignore`
additions

## Background

Standards #211 estate-wide gate (`governance / Trusted-base reduction
policy`) requires every soundness-relevant escape hatch in a
proof-bearing repo to be either:

- (a) discharged (proof landed → entry removed),
- (b) budgeted (`TRUSTED:` inline + entry in `docs/proof-debt.md` §(b)),
- (c) necessary axiom (`AXIOM:` inline + entry in §(c)),
- (d) debt (deadline + owner in §(d)).

echo-types has exactly one such hatch: the four propositional-truncation
postulates in `EchoImageFactorizationPropPostulated.agda`. They are
already:

- explicitly scoped exploratory by the file preamble,
- allowed by `hypatia: allow code_safety/agda_postulate`,
- exempted in `tools/check-guardrails.sh`,
- classified Tier-2 in `docs/echo-types/echo-kernel-note.adoc`.

This PR just adds the canonical enumeration so the gate goes green for
all future PRs.

## Verification

```
$ bash /tmp/check-trusted-base.sh .
[INFO] Found 1 soundness-relevant escape hatch(es).
[OK] proof-debt document(s) found: docs/proof-debt.md
[OK] All 1 escape hatch(es) are documented.
```

## Test plan

- [x] `bash check-trusted-base.sh` passes locally
- [ ] `governance / Trusted-base reduction policy` green on this PR
- [ ] Auto-merge SQUASH armed

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

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

Author: hyperpolymath

docs/proof-debt.md

@@ -0,0 +1,49 @@
+# Proof debt
+
+Per the estate Trusted-Base Reduction Policy
+(hyperpolymath/standards `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`), every
+soundness-relevant escape hatch in this repository is enumerated below
+under one of (a) discharged / (b) budgeted / (c) necessary axiom / (d) debt.
+
+## (a) Discharged in this repo
+
+- (none — entries are removed here when proofs land)
+
+## (b) Budgeted — tested with refutation budget
+
+- (none)
+
+## (c) Necessary axiom
+
+- `proofs/agda/EchoImageFactorizationPropPostulated.agda:102` — top-level
+  `postulate` introducing four propositional-truncation primitives
+  (`Trunc-pos`, `∣_∣-pos`, `is-prop-pos`, `rec-pos`)
+  - **Justification**: propositional truncation `∥_∥` cannot be
+    constructed in plain `--safe --without-K` Agda without HITs /
+    Cubical. The four postulates encode the standard `TruncInterface ℓ`
+    record (existence + propositionality + propositional-recursion +
+    introduction). The construction is **exploratory** — the base
+    module `EchoImageFactorizationProp.agda` remains `--safe
+    --without-K` with zero postulates; `…Postulated` exists solely
+    to demonstrate the interface concretely.
+  - **Citation**: see `docs/echo-types/echo-kernel-note.adoc` (Tier-2
+    classification — "Exploratory / postulated"); HoTT Book §3.7
+    (propositional truncation); agda-stdlib does not currently expose
+    this in `--safe --without-K`.
+  - **Guardrail status**: explicitly allow-listed in
+    `tools/check-guardrails.sh` and in the inline `hypatia: allow`
+    pragma at the head of the module.
+
+## (d) DEBT — actively to be closed
+
+- (none — the kernel is `--safe --without-K` clean; all
+  `…Postulated` modules are intentionally scoped to (c).)
+
+## Notes
+
+The `EchoDecorationBridge.agda` module is tagged exploratory in the
+guardrail but contains no escape hatches; it is excluded from the
+guardrail's "no postulates" rule for naming convenience (the
+`-Postulated` suffix would be misleading there). The trusted-base
+script does not flag this module because it scans for actual
+`^[[:space:]]*postulate` lines.