Skip to content

Commit fee5f06

Browse files
docs: seed docs/proof-debt.md index per trusted-base policy (#71)
Per the trusted-base reduction policy (hyperpolymath/standards#203), adds a schema-conformant index at docs/proof-debt.md that references PROOF-NEEDS.md as the source of truth. This repo already has substantive proof-debt documentation in PROOF-NEEDS.md — this PR doesn't duplicate that content, just adds the schema bridge so the check-trusted-base CI gate (standards#211) finds docs/proof-debt.md at the canonical filename and recognises this repo as documented. Marker count detected by check-trusted-base.sh: 34. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 42df211 commit fee5f06

1 file changed

Lines changed: 59 additions & 0 deletions

File tree

docs/proof-debt.md

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
-->
5+
6+
# Proof Debt — stapeln
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+
This file is the schema-conformant **index** for this repo's proof
11+
debt. The substantive content lives in
12+
[`PROOF-NEEDS.md`](../PROOF-NEEDS.md) — keep that file as the source of truth
13+
and use this one as the schema bridge for the
14+
`check-trusted-base.sh` CI gate ([standards#211](https://github.com/hyperpolymath/standards/pull/211)).
15+
16+
## Marker count (2026-05-26)
17+
18+
34 soundness-relevant escape hatches detected by
19+
`scripts/check-trusted-base.sh`. See `PROOF-NEEDS.md` for the per-site
20+
classification rationale.
21+
22+
## (a) DISCHARGED in this repo
23+
24+
See `PROOF-NEEDS.md` — any markers no longer present in source.
25+
26+
## (b) BUDGETED — tested with a refutation budget
27+
28+
See `PROOF-NEEDS.md` — markers at FFI / extraction boundaries with
29+
documented property-test budgets.
30+
31+
## (c) NECESSARY AXIOM
32+
33+
See `PROOF-NEEDS.md` — markers that encode metatheoretic assumptions.
34+
35+
## (d) DEBT — actively to be closed
36+
37+
See `PROOF-NEEDS.md` — markers still owed a proof or a §(b)/§(c)
38+
classification.
39+
40+
## How to update this file
41+
42+
When markers change in source:
43+
44+
1. Update `PROOF-NEEDS.md` first (source of truth).
45+
2. If the marker count changes substantially, update the count above
46+
so this index doesn't drift.
47+
3. The `check-trusted-base` CI gate (standards#211) reads BOTH
48+
`docs/proof-debt.md` AND `PROOF-NEEDS.md` for documentation lookups,
49+
so the index can stay light.
50+
51+
## Companion documents
52+
53+
- [standards#195](https://github.com/hyperpolymath/standards/pull/195) — estate proof-debt audit.
54+
- [standards#203](https://github.com/hyperpolymath/standards/pull/203) — trusted-base reduction policy (the schema).
55+
- [`PROOF-NEEDS.md`](../PROOF-NEEDS.md) — this repo's substantive proof-debt audit (source of truth).
56+
57+
---
58+
59+
🤖 Schema-conformant index seeded by Claude Code, 2026-05-26.

0 commit comments

Comments
 (0)