docs+meta: cleanup after #58 — proof-debt cross-refs + STATE/META#59
Merged
Merged
Conversation
Cleanup follow-on to PR #58 (Phase 1 per-axiom triage of 72 Coq Axioms): - CHANGELOG.md: add #58 under Unreleased/Documentation. - docs/proof-debt.md: link to docs/proof-debt-triage.md from the seed; update §(a)/§(b)/§(c)/§(d) sections to reflect the Phase 1 disposition (52 c / 17 a / 3 b for Coq); update headline count 129 → 124 reflecting intervening closures. - .machine_readable/6a2/STATE.a2ml: bump last-updated; replace stale "begin classification sweep" next-action with the 17 §a discharge backlog + Phase 2 (Lean axioms + Idris2 postulates); add 2026-05-27 session-history entry; refresh coq-proofs component summary. - .machine_readable/6a2/META.a2ml: bump last-updated; add ADR-009 (was missing here vs. META.scm) + new ADR-010 for the Phase 1 triage. - .machine_readable/META.scm: add ADR-010 matching META.a2ml for parity. No code changes; documentation + machine-readable state only. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
5 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
…a triage (#60) ## Summary Phase 2a of the standards#203 trusted-base reduction policy rollout (follow-up to #58 / #59 Coq triage). First cluster: `proofs/coq/lambda/` + `proofs/lean4/LambdaCNO.lean`. ### Coq (2 markers, both §(c) AXIOM per #58 triage) - `proofs/coq/lambda/LambdaCNO.v:356` `y_not_cno` — inline `(* AXIOM: ... *)` annotation added. - `proofs/coq/lambda/LambdaCNO.v:376` `eta_equivalence` — inline `(* AXIOM: ... *)` annotation added. ### Lean (3 markers — new Phase 2a triage) | Line | Identifier | Disposition | |-----:|------------|-------------| | 183 | `subst_closed_term` | §(d) DEBT (provable; INDEFINITE) | | 232 | `y_combinator_not_identity` | §(c) AXIOM (inline annotation added) | | 258 | `eta_equivalence` | §(c) AXIOM (inline annotation added) | ### docs/proof-debt.md - New "Phase 2a triage — Lean Lambda cluster" section with per-marker table. - §(d) bucket gains the Lean `subst_closed_term` DEBT entry (owner + INDEFINITE deadline). ## Verification ``` $ bash ../standards/scripts/check-trusted-base.sh . [INFO] Found 129 soundness-relevant escape hatch(es). [OK] proof-debt document(s) found: docs/proof-debt.md [ERROR] 123/129 escape hatch(es) are undocumented. ``` **Lambda-specific errors: 0** (down from 5). The remaining 123 errors are the Quantum / Filesystem / Physics clusters, scheduled for follow-up PRs (Phase 2b/2c/2d). ## Test plan - [x] check-trusted-base.sh reports 0 errors on Lambda lines. - [x] All inline annotations precede Axiom / axiom within the script's 5-line lookback. - [x] Lean §(d) DEBT entry has owner + deadline per standards#203 schema. - [ ] Coq build still green (no semantic change — only added comments). - [ ] Lean build still green (no semantic change — only added comments). Refs standards#203, #58, #59. 🤖 Generated with [Claude Code](https://claude.com/claude-code) 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
Cleanup follow-on to #58 (Phase 1 per-axiom triage of 72 Coq Axioms). Wires the new triage doc into the existing seed and refreshes machine-readable state.
docs/proof-debt-triage.md; refresh §(a)/§(b)/§(c)/§(d) sections to reflect the Phase 1 disposition (52 c / 17 a / 3 b for Coq); update headline count 129 → 124 reflecting intervening closures.last-updatedto 2026-05-27; replace stale "begin classification sweep" next-action with the 17 §a discharge backlog + Phase 2 (Lean axioms + Idris2 postulates); add 2026-05-27 session-history entry; refreshcoq-proofscomponent summary.last-updated; add ADR-009 (was missing here vsMETA.scm) + new ADR-010 for the Phase 1 triage.META.a2mlfor parity.No code changes; documentation + machine-readable state only.
Test plan
check-trusted-base.shcount unchanged (124 — no axioms touched)🤖 Generated with Claude Code