proof-debt.md

Proof Debt — snifs

Schema: hyperpolymath/standards TRUSTED-BASE-REDUCTION-POLICY.adoc (standards#203).

Current state

Zero soundness-relevant escape hatches in this repo as of 2026-05-26.

Verified by scripts/check-trusted-base.sh from hyperpolymath/standards — all matches found by syntactic scan were inside docstrings explicitly stating the file does NOT use believe_me / assert_total / postulate / sorry / Admitted (the "no escape hatches" discipline pattern).

(a) DISCHARGED in this repo

(None — never any to discharge.)

(b) BUDGETED — tested with a refutation budget

(None.)

(c) NECESSARY AXIOM

(None.)

(d) DEBT — actively to be closed

(None.)

Preservation contract

This file exists to assert the zero-debt invariant for the scripts/check-trusted-base.sh CI gate (standards#211). Any future PR that introduces a soundness-relevant escape hatch MUST either:

1. annotate the call site with a leading TRUSTED: / AXIOM: comment, OR
2. add an entry to this file under §(b) / §(c) / §(d).

PRs that introduce un-annotated escape hatches will fail CI.

Companion documents

• standards#195 — estate proof-debt audit.
• standards#203 — trusted-base reduction policy (the schema this file follows).
• standards#211 — check-trusted-base.sh CI enforcement.

---

🤖 Initial seed by Claude Code, 2026-05-26.