docs: clarify preservation proof boundaries

.github/workflows/status-gate.yml

@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 # Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-# Status Gate — fail when the PROOF-NEEDS.md / TEST-NEEDS.md count markers
+# Status Gate — fail when the PROOF-NEEDS.adoc / TEST-NEEDS.adoc count markers
 # drift from coqc/cargo ground truth.
 #
 # Split into two independent jobs so the slow one is cancellable without
@@ -18,8 +18,8 @@ on:
   pull_request:
     paths:
       - 'formal/**'
-      - 'PROOF-NEEDS.md'
-      - 'TEST-NEEDS.md'
+      - 'PROOF-NEEDS.adoc'
+      - 'TEST-NEEDS.adoc'
       - 'scripts/status-gate.sh'
       - 'Cargo.toml'
       - 'Cargo.lock'
@@ -36,7 +36,7 @@ concurrency:
 
 jobs:
   # CORE — fast, no toolchain. Keep this one required: a new Admitted that
-  # isn't reflected in PROOF-NEEDS.md fails here in ~1 second.
+  # isn't reflected in PROOF-NEEDS.adoc fails here in ~1 second.
   status-gate-core:
     name: status-gate-core
     runs-on: ubuntu-latest
@@ -56,7 +56,7 @@ jobs:
     steps:
       - name: Notice — this is the slow, skippable job
         run: |
-          echo "::notice title=Slow check — safe to cancel::status-gate-tests runs a full cargo build just to verify the TEST-NEEDS.md test count. The core proof-count gate (status-gate-core) is a separate, independent job and is already enforced. If you're in a rush you can cancel THIS job without letting any core gating go."
+          echo "::notice title=Slow check — safe to cancel::status-gate-tests runs a full cargo build just to verify the TEST-NEEDS.adoc test count. The core proof-count gate (status-gate-core) is a separate, independent job and is already enforced. If you're in a rush you can cancel THIS job without letting any core gating go."
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
       - name: Install Rust toolchain

.machine_readable/6a2/STATE.a2ml

@@ -5,10 +5,17 @@
 # See: standards/a2ml-templates/STATE.a2ml.v2.spec.adoc
 
 @state(version="2.0"):
+# current_* fields below supersede the 2026-06 journal text and the dated
+# owner-directive snapshot; see CLAUDE.md and PROOF-NEEDS.adoc for policy.
 phase: "implementation"
-next_action: "Phase D slice 4 Phase 3b Stages 2-4 (#240/#241/#242): Stage 1 (both 1a + 1b) complete. Stages 2-4 sequenced per the owner-approved 4-stage plan: Stage 2 (#240) ELam annotation extension — independent of Stage 1, ships when prioritised; Stage 3 (#241) CPS + relaxed Phase 3b — blocked on Stage 2; Stage 4 (#242) compound non-linear + unconditional preservation_l2 — blocked on Stage 3. Stage 4's destination collapses Stage 1b's three preconditions (P1 = tfuneff_lambda_free, P2 = regions_introduced_by ⊆ R_in_v, P3 = expr_closed_below 0 v) once typing-derived closure invariants land. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted`; no touching `Semantics.v` / `Typing.v` / `Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
+next_action: "Owner-approved L1/L2 soundness redesign: preserve the legacy five-Qed counterexample and durable Admitted; do not prove the refuted step_pop_disjoint_from_type_l1 or preservation_l1 statements; do not claim unconditional L2 preservation. First classify each exact obligation under hyperpolymath/mathesis/estate-mathematical-architecture and standards/3-practice/PROOF-POLICY.adoc. Grade 3 is Agda-only; current Coq witnesses are not Grade 3, and Ephapax-specific engineering claims map to Idris2 unless an implementation-independent Agda theory statement is explicitly defined. Update the proof ledger after policy resolution; no proof build was run in this environment."
 last_action: "Proof + stdlib wave 2026-06-01 → 02 landed (13 PRs): canonical-forms L1 modality-polymorphic (#274, P43, 7 lemmas axiom-free, prerequisite for progress_l1/P42); Print Assumptions audit framework across L1 + L3 keystones (#270, closes P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (#280, P06, HARD cases blocked on #240/#241/#242); Rust↔Coq is_linear_ty truth-table mechanical assertion (#273, P28); OwnershipKind from_byte/to_byte round-trip (#277, P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions as linear scopes (#275, D04), Allen's interval algebra (#272, D11), MessageHandle as linear typestate (#279, D17), monoidal aggregates (#281, D18); doc truth-restore + banned-preservation framing buried (#263); cluster-D L3/L4 status meander (#278); Track C panic-attack triage (#271); coq-build noble apt CI fix (#282, unblocks ~5 PRs); R5b standards SHA bump (#276). Plus CHANGELOG sync (#283). Build oracle clean across all 12 .v files. Print Assumptions: canonical_*_l1_m + most new lemmas zero-axiom; expected residuals (preservation_l1, region_liveness_at_split_l1_gen, region_shrink_preserves_typing_l1_gen_m) tracked. Stages 2-4 (#240/#241/#242) still un-touched. Wiki Proof-status.md refreshed 2026-06-02. | INFRA (2026-06-24, non-proof track): governance docs landed (#314 — CODEOWNERS/GOVERNANCE.adoc/MAINTAINERS.adoc); standards reusable-workflow pins remediated (#315) and current at d135b05 (#316); Hypatia neurosymbolic gate now active and reporting 37 pre-existing findings (5 crit / 7 high / 25 med) — triage handed off (docs/governance/HYPATIA-HANDOFF.md), standards visibility patch drafted-not-applied. No .v files touched; no proof-state change."
-updated: 2026-06-24T18:13:15Z
+current_last_action: "2026-11-01 proof-honesty audit: updated local status surfaces, retained all proof terms, and recorded Mathesis Grade 3/standards mapping without promoting Coq evidence to Grade 3. No Coq build run; coqc unavailable."
+current_proof_boundary: "Legacy preservation is refuted and its Admitted is durable; step_pop_disjoint_from_type_l1 and modality-polymorphic preservation_l1 are refuted as stated; no unconditional preservation_l2 theorem is declared; preserve all Coq regressions."
+current_grade_target: "Mathesis Grade 3 requested but not claimed. Grade 3 requires local Agda checking; current regressions are Coq. Standards proof policy maps repo-specific engineering claims to Idris2 unless an implementation-independent Agda theory statement is explicitly identified."
+proof_policy_sources: ["https://github.com/hyperpolymath/mathesis/blob/main/estate-mathematical-architecture", "https://github.com/hyperpolymath/standards/blob/main/3-practice/PROOF-POLICY.adoc"]
+proof_status_source: "PROOF-NEEDS.adoc + EXPLAINME.adoc proof ledger"
+updated: 2026-11-01
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,
@@ -107,7 +114,7 @@ updated: 2026-06-24T18:13:15Z
 # Doc lockdown:
 #   CLAUDE.md                       — owner directive §
 #   formal/PRESERVATION-DESIGN.md   — CANONICAL banner
-#   formal/PRESERVATION-HANDOFF.md  — ARCHAEOLOGY ONLY banner
+#   formal/PRESERVATION-HANDOFF.adoc  — ARCHAEOLOGY ONLY banner
 #   ROADMAP.adoc                    — closure-plan section removed
 @end
 @end

CITATION.cff

@@ -2,7 +2,7 @@ cff-version: 1.2.0
 message: "If you use this software, please cite it as below."
 type: software
 title: "Ephapax"
-abstract: "Dyadic linear+affine type system for compile-time WASM memory safety — no use-after-free, no leaks, region-based allocation. Mechanically proved in Coq and Idris2."
+abstract: "Research language exploring dyadic linear/affine typing, region-based allocation, and WebAssembly. Includes Coq and Idris2 proof artifacts; current counterexamples refute unrestricted legacy and L1 preservation, no unconditional L2 preservation theorem is established, and implementation refinement remains unproved."
 authors:
   - family-names: "Jewell"
     given-names: "Jonathan D.A."