|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: MPL-2.0 |
| 3 | +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) |
| 4 | +--> |
| 5 | + |
| 6 | +# Proof Debt — absolute-zero |
| 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 | +## Initial inventory |
| 11 | + |
| 12 | +The 2026-05-26 estate proof-debt audit |
| 13 | +([standards#195](https://github.com/hyperpolymath/standards/pull/195)) |
| 14 | +detected **129 soundness-relevant escape hatches** in this |
| 15 | +repo. This file is the **initial seed** — every marker starts in §(d) |
| 16 | +DEBT and the maintainer triages each into §(a) / §(b) / §(c) / §(d) as |
| 17 | +classification proceeds. |
| 18 | + |
| 19 | +## (a) DISCHARGED in this repo |
| 20 | + |
| 21 | +*(None yet — entries move here when the proof lands or the construct |
| 22 | +is removed.)* |
| 23 | + |
| 24 | +## (b) BUDGETED — tested with a refutation budget |
| 25 | + |
| 26 | +*(None yet — entries belong here when the construct is at an |
| 27 | +extraction boundary and is covered by a documented property-test |
| 28 | +budget.)* |
| 29 | + |
| 30 | +## (c) NECESSARY AXIOM |
| 31 | + |
| 32 | +*(None yet — entries belong here when the construct encodes a |
| 33 | +metatheoretic assumption that cannot be discharged within the working |
| 34 | +logic.)* |
| 35 | + |
| 36 | +## (d) DEBT — actively to be closed |
| 37 | + |
| 38 | +All 129 markers below start in this section. As the |
| 39 | +maintainer classifies each, it should be moved into §(a) / §(b) / |
| 40 | +§(c) as appropriate. Markers that genuinely belong in §(d) need a |
| 41 | +deadline and an owner. |
| 42 | + |
| 43 | +``` |
| 44 | +(no markers; check-trusted-base passes already) |
| 45 | +``` |
| 46 | + |
| 47 | +> If `129` > 30, the list above shows the first 30 only. |
| 48 | +> The full list is reproducible via: |
| 49 | +> |
| 50 | +> ```bash |
| 51 | +> bash /path/to/standards/scripts/check-trusted-base.sh . |
| 52 | +> ``` |
| 53 | +
|
| 54 | +## Suggested triage process |
| 55 | +
|
| 56 | +1. Run `scripts/check-trusted-base.sh` locally; it lists every marker |
| 57 | + with file:line. |
| 58 | +2. For each marker, decide: |
| 59 | + - Can this be proven? → §(a) DISCHARGED via a PR that adds the proof. |
| 60 | + - Is this at an FFI / extraction / opaque-primitive boundary? → |
| 61 | + §(b) or §(c). Add a property test and document the refutation |
| 62 | + budget for §(b), or cite the metatheoretic justification for §(c). |
| 63 | + - Is this temporary debt? → §(d) with a deadline. |
| 64 | +3. Update this file in the same PR that lands the disposition. |
| 65 | +4. The `check-trusted-base` CI job (standards#211) ensures markers |
| 66 | + are never un-annotated AND un-enumerated simultaneously. |
| 67 | +
|
| 68 | +## Companion documents |
| 69 | +
|
| 70 | +- [standards#195](https://github.com/hyperpolymath/standards/pull/195) — estate proof-debt audit. |
| 71 | +- [standards#203](https://github.com/hyperpolymath/standards/pull/203) — trusted-base reduction policy (the schema this file follows). |
| 72 | +- [standards#211](https://github.com/hyperpolymath/standards/pull/211) — `check-trusted-base.sh` CI enforcement. |
| 73 | +
|
| 74 | +--- |
| 75 | +
|
| 76 | +🤖 Initial seed by Claude Code, 2026-05-26. |
0 commit comments