Skip to content

Commit 562f817

Browse files
docs: seed docs/proof-debt.md (zero-debt invariant) per trusted-base policy (#26)
## Summary - Adds `docs/proof-debt.md` declaring this repo's zero-soundness-debt invariant. - Verified: every syntactic `believe_me` / `assert_total` / `postulate` match in source is inside a docstring explicitly stating the file does NOT use that construct. - Closes part of the [estate trusted-base reduction policy](hyperpolymath/standards#203) follow-up (P1 seed). ## Effect Future PRs that introduce real escape hatches will be caught by [`check-trusted-base.sh`](hyperpolymath/standards#211) and must annotate inline OR enumerate here. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 86d6db8 commit 562f817

1 file changed

Lines changed: 57 additions & 0 deletions

File tree

docs/proof-debt.md

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
-->
5+
6+
# Proof Debt — snifs
7+
8+
**Schema**: [hyperpolymath/standards `TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) (standards#203).
9+
10+
## Current state
11+
12+
**Zero soundness-relevant escape hatches** in this repo as of 2026-05-26.
13+
14+
Verified by `scripts/check-trusted-base.sh` from
15+
[hyperpolymath/standards](https://github.com/hyperpolymath/standards)
16+
all matches found by syntactic scan were inside docstrings explicitly
17+
stating the file does NOT use `believe_me` / `assert_total` /
18+
`postulate` / `sorry` / `Admitted` (the "no escape hatches"
19+
discipline pattern).
20+
21+
## (a) DISCHARGED in this repo
22+
23+
*(None — never any to discharge.)*
24+
25+
## (b) BUDGETED — tested with a refutation budget
26+
27+
*(None.)*
28+
29+
## (c) NECESSARY AXIOM
30+
31+
*(None.)*
32+
33+
## (d) DEBT — actively to be closed
34+
35+
*(None.)*
36+
37+
## Preservation contract
38+
39+
This file exists to assert the **zero-debt invariant** for the
40+
`scripts/check-trusted-base.sh` CI gate (standards#211). Any future PR
41+
that introduces a soundness-relevant escape hatch MUST either:
42+
43+
1. annotate the call site with a leading `TRUSTED:` / `AXIOM:`
44+
comment, OR
45+
2. add an entry to this file under §(b) / §(c) / §(d).
46+
47+
PRs that introduce un-annotated escape hatches will fail CI.
48+
49+
## Companion documents
50+
51+
- [standards#195](https://github.com/hyperpolymath/standards/pull/195) — estate proof-debt audit.
52+
- [standards#203](https://github.com/hyperpolymath/standards/pull/203) — trusted-base reduction policy (the schema this file follows).
53+
- [standards#211](https://github.com/hyperpolymath/standards/pull/211)`check-trusted-base.sh` CI enforcement.
54+
55+
---
56+
57+
🤖 Initial seed by Claude Code, 2026-05-26.

0 commit comments

Comments
 (0)