From 824a9a7d18a2635068d9ae39e8399b4dee5aaf57 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 27 May 2026 08:41:41 +0100
Subject: [PATCH] =?UTF-8?q?docs(policy):=20correct=20ephapax=20Admitted=20?=
 =?UTF-8?q?count=20(3=20=E2=86=92=201)=20+=20link=20adoption=20PR?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The trusted-base reduction policy's migration table cited 3 Admitteds
in ephapax/formal/Semantics.v. Actual count on main is 1 — the other
2 (step_preserves_type and step_output_context_eq) were discharged via
ephapax#146 (Path 3 at-pre helper landing) before the policy doc was
filed.

Also adds:
- Link to formal/PRESERVATION-DESIGN.md (four-layer redesign on branch
  proof/l1-region-threading-design) as the principled closure plan.
- Forward link to ephapax#164 (the P0 migration PR adopting this
  policy in ephapax/docs/proof-debt.adoc).

No semantic change to the policy itself — just keeping the migration
table accurate as repos adopt the schema.
---
 docs/TRUSTED-BASE-REDUCTION-POLICY.adoc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc b/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc
index 5f490088..15672cf8 100644
--- a/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc
+++ b/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc
@@ -191,7 +191,7 @@ first (rough P0/P1/P2 ordering):
 |===
 | Priority | Repo | Why this one first
 
-| P0 | `ephapax`             | 3 `Admitted`s in `formal/Semantics.v` already have a discharge plan (memory: `project_ephapax_preservation_closure_plan`); annotate while closing.
+| P0 | `ephapax`             | 1 `Admitted` in `formal/Semantics.v` (`preservation`); was 3 at audit time, 2 discharged via https://github.com/hyperpolymath/ephapax/pull/146[ephapax#146]. Discharge plan in `ROADMAP.adoc` § "Preservation closure plan" + `formal/PRESERVATION-DESIGN.md` (four-layer redesign on branch `proof/l1-region-threading-design`). Migration filed: https://github.com/hyperpolymath/ephapax/pull/164[ephapax#164].
 | P0 | `boj-server`          | Reference implementation — formalise the existing harness as the canonical example.
 | P1 | `absolute-zero`       | 72 Coq + 315 Lean markers across 6638 proof files; needs the schema before any single-repo close-out is tractable.
 | P1 | `maa-framework`       | 134 markers in 25 files (high density); investigate whether vendored or original.