Skip to content

Commit 23a4718

Browse files
docs: seed docs/proof-debt.md index per trusted-base policy (#74)
## Summary - Adds a thin, schema-conformant index at `docs/proof-debt.md`. - References [`PROOF-NEEDS.md`](./PROOF-NEEDS.md) as the source of truth — no content duplication. - P1 seed in the [trusted-base reduction policy](hyperpolymath/standards#203) chain. ## What this PR does NOT do Migrate the substantive content out of `PROOF-NEEDS.md`. That file remains canonical; this file just makes the schema-conformant filename exist for the [`check-trusted-base.sh`](hyperpolymath/standards#211) CI gate. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent fe6883b commit 23a4718

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 — proven
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+
10 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)