From 907f4d6e7f0364836cbacea8873f7260e36f5abc Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 17:51:55 +0100 Subject: [PATCH] docs: seed docs/proof-debt.md per trusted-base policy MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per the trusted-base reduction policy (hyperpolymath/standards#203), enumerates the soundness-relevant escape hatches in this repo with their initial disposition (§(d) DEBT, awaiting triage). scripts/check-trusted-base.sh (from hyperpolymath/standards) detected 129 markers; this PR is the initial seed. The maintainer should triage each marker into §(a) DISCHARGED, §(b) BUDGETED (extraction-boundary code covered by property tests with a refutation budget), or §(c) NECESSARY AXIOM (metatheoretic assumption with citation). Markers that remain in §(d) need an owner + deadline. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/proof-debt.md | 76 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) create mode 100644 docs/proof-debt.md diff --git a/docs/proof-debt.md b/docs/proof-debt.md new file mode 100644 index 0000000..b72d383 --- /dev/null +++ b/docs/proof-debt.md @@ -0,0 +1,76 @@ + + +# Proof Debt — absolute-zero + +**Schema**: [hyperpolymath/standards `TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) (standards#203). + +## Initial inventory + +The 2026-05-26 estate proof-debt audit +([standards#195](https://github.com/hyperpolymath/standards/pull/195)) +detected **129 soundness-relevant escape hatches** in this +repo. This file is the **initial seed** — every marker starts in §(d) +DEBT and the maintainer triages each into §(a) / §(b) / §(c) / §(d) as +classification proceeds. + +## (a) DISCHARGED in this repo + +*(None yet — entries move here when the proof lands or the construct +is removed.)* + +## (b) BUDGETED — tested with a refutation budget + +*(None yet — entries belong here when the construct is at an +extraction boundary and is covered by a documented property-test +budget.)* + +## (c) NECESSARY AXIOM + +*(None yet — entries belong here when the construct encodes a +metatheoretic assumption that cannot be discharged within the working +logic.)* + +## (d) DEBT — actively to be closed + +All 129 markers below start in this section. As the +maintainer classifies each, it should be moved into §(a) / §(b) / +§(c) as appropriate. Markers that genuinely belong in §(d) need a +deadline and an owner. + +``` +(no markers; check-trusted-base passes already) +``` + +> If `129` > 30, the list above shows the first 30 only. +> The full list is reproducible via: +> +> ```bash +> bash /path/to/standards/scripts/check-trusted-base.sh . +> ``` + +## Suggested triage process + +1. Run `scripts/check-trusted-base.sh` locally; it lists every marker + with file:line. +2. For each marker, decide: + - Can this be proven? → §(a) DISCHARGED via a PR that adds the proof. + - Is this at an FFI / extraction / opaque-primitive boundary? → + §(b) or §(c). Add a property test and document the refutation + budget for §(b), or cite the metatheoretic justification for §(c). + - Is this temporary debt? → §(d) with a deadline. +3. Update this file in the same PR that lands the disposition. +4. The `check-trusted-base` CI job (standards#211) ensures markers + are never un-annotated AND un-enumerated simultaneously. + +## Companion documents + +- [standards#195](https://github.com/hyperpolymath/standards/pull/195) — estate proof-debt audit. +- [standards#203](https://github.com/hyperpolymath/standards/pull/203) — trusted-base reduction policy (the schema this file follows). +- [standards#211](https://github.com/hyperpolymath/standards/pull/211) — `check-trusted-base.sh` CI enforcement. + +--- + +🤖 Initial seed by Claude Code, 2026-05-26.