Skip to content

Commit 38802f8

Browse files
committed
docs(manifest): replace stale "67/67 Qed" claim with honest proof-debt pointer
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.
1 parent a54ecb7 commit 38802f8

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

0-AI-MANIFEST.a2ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ These 6 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY:
2323

2424
## CORE INVARIANTS
2525

26-
1. **Formal Proof Integrity** - No `Admitted` in Coq or `believe_me`/`assert_total` in Idris2. All proofs MUST remain closed (67/67 Qed).
26+
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.
2727
2. **Dyadic Separation** - The boundary between affine and linear types must be strictly enforced.
2828
3. **SPDX Headers** - All source files MUST carry `SPDX-License-Identifier: PMPL-1.0-or-later`.
2929
4. **Author Attribution** - Always "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>".

0 commit comments

Comments
 (0)