docs: seed docs/proof-debt.md per trusted-base policy#52
Merged
Conversation
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) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
docs/proof-debt.mdenumerating this repo's 129 soundness-relevant escape hatches.Why this matters
Without this file,
check-trusted-base.shfails CI on every escape hatch as 'undocumented'. With this file, all 129 markers are at least enumerated and the maintainer can disposition them at their own pace.🤖 Generated with Claude Code