From 38802f84dc230b91cfe094b7d954fe224bb100b2 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 12:58:25 +0100 Subject: [PATCH] docs(manifest): replace stale "67/67 Qed" claim with honest proof-debt pointer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The CORE INVARIANTS section in 0-AI-MANIFEST.a2ml claimed "All proofs MUST remain closed (67/67 Qed)" — false as of mid-2026: - formal/Semantics.v `preservation` is Admitted (provably FALSE per Counterexample.v's 3 Qed lemmas). - formal/Semantics_L1.v carries 4+ admits + 1 Admitted Lemma region_liveness_at_split_l1_gen (post-#181) + 1 Admitted preservation_l1. The trusted-base reduction policy (standards#203) is the canonical enforcement mechanism — every escape hatch is enumerated by file:line in docs/proof-debt.adoc. Replace the 67/67 number with a pointer to that mechanism, and strengthen the rule: ANY new escape hatch must be enumerated in docs/proof-debt.adoc before the trusted-base CI check will pass. Refs PR #176 (L2 hybrid), PR #181 (Axiom→Lemma), PR #164 (proof-debt seed), standards#203. --- 0-AI-MANIFEST.a2ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 4b44e4b..7d2148d 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -23,7 +23,7 @@ These 6 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY: ## CORE INVARIANTS -1. **Formal Proof Integrity** - No `Admitted` in Coq or `believe_me`/`assert_total` in Idris2. All proofs MUST remain closed (67/67 Qed). +1. **Formal Proof Integrity** — Coq proofs are layered per the four-layer redesign (`formal/PRESERVATION-DESIGN.md`). The legacy `preservation` in `Semantics.v` is provably FALSE per `Counterexample.v` (3 Qed lemmas) and remains `Admitted`. The L1 preservation chain (`Semantics_L1.v`) is in flight; explicit `Admitted` / `admit.` / `Axiom` sites are enumerated by `file:line` in `docs/proof-debt.adoc` per the standards#203 trusted-base reduction policy. Idris2 source has no `believe_me` / `assert_total` / `sorry`. ANY new escape hatch must be enumerated in `docs/proof-debt.adoc` before the trusted-base CI check will pass. 2. **Dyadic Separation** - The boundary between affine and linear types must be strictly enforced. 3. **SPDX Headers** - All source files MUST carry `SPDX-License-Identifier: PMPL-1.0-or-later`. 4. **Author Attribution** - Always "Jonathan D.A. Jewell ".