docs: canonicalise the preservation closure plan in ROADMAP (#117)

After PR #116 brought preservation to 12 open goals (from 910 at session
start), this PR sets the 5-phase closure plan as the canonical path in
ROADMAP.adoc. Any session picking up the proof work follows this.

## Plan summary

Full detail in ROADMAP §"Preservation closure plan". 5 phases:

1. **Lemma B** (linearity-context invariance for siblings) — ~3-4h
2. **Apply Lemma B** → close 11 congruence cases — ~2h, parallelizable
3. **Region-env weakening lemma** for non-values — 1-2 days
4. **Apply Phase 3** → close S_Region_Step — ~1h
5. **`Admitted.` → `Qed.`** + docs sweep — ~1h

Total: 3 sessions / ~10 hours wall-clock with fan-out.

## Other docs updated

- `PROOF-NEEDS.md` — points at ROADMAP plan + lists 5 phases
- `formal/PRESERVATION-HANDOFF.md` — header redirects to ROADMAP;
state-at-a-glance extended through 2026-05-21

No proof changes. Phase 1 commences in a follow-up PR on top of this.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -7,10 +7,22 @@
 - `src/formal/Ephapax/Formal/RegionLinear.idr` — Idris2 region-based linearity proof (explicitly states "REAL proof — not believe_me, not assert_total")
 - 17 Idris2 files across formal verification layer
 - No `believe_me`, `sorry`, or `assert_total` in Idris2 source code
-- Coq admitted proofs remaining in `formal/Semantics.v`: 1 (`preservation`)
+- Coq admitted proofs remaining in `formal/Semantics.v`: 1 (`preservation` — 12 open goals, plan below)
 
 ## What needs proving
-- **`preservation`**: Close the remaining ~29 open goals in the proof script at `formal/Semantics.v` L3215–L3339 so the `Qed` lands and the file builds without `Admitted.` Down from 910 open goals (full 35×26 cross-case combinatorial) after introducing the standard preservation pattern (`remember (mu, R, e) as cfg eqn:Hcfg` + symmetric for cfg', then `inversion Hcfg; subst; inversion Hcfg'; subst;` inside each case). The remaining 29 are real diagonal cases — see `formal/PRESERVATION-HANDOFF.md` for the per-case checklist. Supporting lemmas already Qed (`subst_preserves_typing`, `region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`, `values_dont_step`). The S_Region_Step + T_Region_Active case still blocks on a region-env *weakening* lemma for non-values, which does not yet exist. An earlier ~40-goal diagnostic (PR #104) measured the PRE-`remember-cfg`-pattern state and is superseded.
+- **`preservation`**: Close the remaining **12 open goals** in `formal/Semantics.v` so the `Qed` lands. Down from 910 at session start (98.7% reduction). Reduction story: 910 → 29 via remember-cfg (PR #102) → 22 via universal-IH revert (PR #106) → 12 via per-case manual closures (PR #116). The remaining 12 are 11 congruence cases (`S_*_Step` variants) + 1 region case (`S_Region_Step + T_Region_Active`).
+
+  **Canonical closure path: `ROADMAP.adoc` § Preservation closure plan** — 5 phases:
+
+  1. **Lemma B (linearity-context invariance for siblings)** — closes the IH-vs-sibling context mismatch blocking the 11 congruence cases. ~3–4 hours.
+  2. **Apply Lemma B → close 11 congruence cases** — per-case manual proof scripts (PR #116 pattern). ~2 hours, parallelizable.
+  3. **Region-env weakening lemma for non-values** — defines `safe_for_region_weakening` predicate + proves the weakening lemma. 1–2 days, genuine metatheoretic work.
+  4. **Apply Phase 3 lemma → close S_Region_Step** — ~1 hour.
+  5. **`Admitted.` → `Qed.` + docs sweep** — mechanical, ~1 hour.
+
+  Total: 3 sessions / ~10 hours wall-clock with fan-out. See ROADMAP for full effort estimates and risk-adjusted forecast.
+
+  Supporting lemmas already Qed: `subst_preserves_typing`, `region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`, `values_dont_step`, and **`step_R_eq_or_touches_region`** (PR #114, the region-invariance lemma used by the per-case closures and required by Phase 2).
 - **Linear type consumption**: Prove resources with linear types are consumed exactly once across all execution paths (region boundaries, exception handlers)
 - **Effect system soundness**: Prove the effect type system correctly tracks side effects and that effect-free terms are truly pure
 - **Region safety**: Prove that region-based memory management prevents use-after-free and dangling references across region boundaries

ROADMAP.adoc

@@ -150,11 +150,220 @@ All four headline theorems complete with **zero `believe_me` /
 * [ ] Type checker completion (`ephapax-typing`)
 * [ ] WASM code generation: lambda/app compilation (closure conversion)
 * [x] Coq: `subst_preserves_typing` (Qed)
-* [ ] **Coq: close `preservation` to Qed** — the v0.1 blocker. 22 open
-      goals remain (down from 910); needs region-invariance + context-
-      preservation lemmas + the documented region-env weakening lemma
-      for non-values. Multi-day proof engineering. Tracked in
-      `formal/PRESERVATION-HANDOFF.md`.
+* [ ] **Coq: close `preservation` to Qed** — the v0.1 blocker. **12
+      open goals remain** as of 2026-05-21 (down from 910 at session
+      start). Full closure plan in
+      <<preservation-closure-plan,Preservation closure plan>> below.
+
+[#preservation-closure-plan]
+== Preservation closure plan (current canonical path)
+
+The 5-phase plan to close `formal/Semantics.v` `preservation` to
+`Qed.` Each phase has a concrete deliverable, time estimate, and
+dependency chain. This is the **rightful path** any session picking
+up the proof should follow.
+
+=== Reduction story so far
+
+[cols="3,1,2"]
+|===
+| Stage | Open goals | Mechanism
+
+| Pre-campaign (in-file "Qed 2026-04-27" claim was unsubstantiated)
+| 910
+| Documented honestly by PR #92.
+
+| After `remember (mu, R, e) as cfg`
+| 29
+| Standard preservation pattern. PR #102.
+
+| After `revert mu R e mu' R' e' Hcfg Hcfg'` (universal-IH)
+| 22
+| Clean IH quantification across congruence cases. PR #106.
+
+| After region-invariance lemma `step_R_eq_or_touches_region`
+| 22
+| Infrastructure landed; no goals closed alone. PR #114.
+
+| After per-case manual closures
+| **12**
+| 10 β-reduction / value-step cases discharged. PR #116.
+|===
+
+98.7% reduction across one day. Remaining 12 = 11 congruence cases
+(`S_*_Step` variants) + 1 region case (`S_Region_Step + T_Region_Active`).
+
+=== Phase 1 — Lemma B: linearity-context invariance for siblings
+
+**Goal**: a Coq lemma that lets `T_StringConcat`-style reconstruction
+succeed in congruence cases.
+
+**Statement (sketch)**:
+
+[source,coq]
+----
+Lemma sibling_typing_transfers_across_step :
+  forall mu R e mu' R' e' G G_end T G_out,
+    (mu, R, e) -->> (mu', R', e') ->
+    R; G |- e : T -| G_end ->            (* original typing *)
+    R'; G |- e' : T -| G_out ->          (* stepped typing from IH *)
+    G_end = G_out.                       (* linearity contexts coincide *)
+----
+
+The linearity-context evolution induced by `e` is invariant under
+step. With this, sibling typing premises like
+`H6 : R; G' |- e2 : ...` become typable at `R; G_out |- e2 : ...`
+via `G' = G_out`.
+
+**Approach**: induction on `step` with `type_determinacy` per case.
+Same pattern as `step_R_eq_or_touches_region`.
+
+**Effort**: 3–4 hours focused session.
+
+**Risk**: `G_end = G_out` may need weakening to "context-equivalent up
+to flag positions" via the existing `types_agree` machinery. If so,
+the lemma is slightly harder but still tractable.
+
+=== Phase 2 — Apply Lemma B → close 11 congruence cases
+
+**Goal**: 12 → 1 open goals.
+
+**Approach**: extend the PR #116 per-case manual proof pattern to the
+11 `S_X_Step` cases. Each:
+
+. `pose proof (step_R_eq_or_touches_region ... Hstep)` → dispatch
+  the `R = R'` branch via `subst`.
+. `edestruct (IHHstep ...)` → get `Hout : R'; G0 |- e1' : T -| Gout`.
+. `pose proof (sibling_typing_transfers_across_step ...)` → get
+  `Gout = G'` (or the context-equivalence variant).
+. `rewrite <- (sibling lemma result) in H6` or equivalent.
+. `eexists; eapply T_Foo; [exact Hout | exact H6]`.
+
+**Effort**: ~2 hours (11 near-identical bullets).
+
+**Parallelizable**: yes — one agent per typing-constructor cluster
+(string ops, let / app, conditionals, products, sums).
+
+=== Phase 3 — Region-env weakening for non-values
+
+**Goal**: discharge the language-design item documented since the
+start of the campaign.
+
+**Statement (sketch)**:
+
+[source,coq]
+----
+Lemma region_add_typing_for_non_values :
+  forall R e G G' T r,
+    R; G |- e : T -| G' ->
+    ~ In r R ->
+    safe_for_region_weakening e ->       (* new predicate *)
+    (r :: R); G |- e : T -| G'.
+----
+
+**The hard part**: defining `safe_for_region_weakening`. Naive
+weakening is unsound for `EBorrow` (borrows whose region escape the
+weakened scope), `EDrop` of a region-bound resource, `EStringNew r' s`
+where `r' = r` (shadowing). The predicate rules these out
+syntactically.
+
+**Approach**:
+
+. Define the predicate (~30 LOC).
+. Prove the lemma by induction on `has_type` (~80–150 LOC).
+. Cross-check that the step rule `S_Region_Step + T_Region_Active`
+  produces an `e'` satisfying the predicate, given the typing
+  derivation.
+
+**Effort**: 1–2 days. Genuine metatheoretic work.
+
+**Risk**: may need predicate to depend on typing derivation, not just
+expression shape. Mitigation: start with the simplest possible
+predicate (no `ERegion r` or `EStringNew r` syntactically anywhere);
+check if it passes the S_Region_Step case. Refine only if it fails.
+
+=== Phase 4 — Close S_Region_Step + T_Region_Active
+
+**Goal**: 1 → 0 open goals.
+
+**Approach**: replace `apply region_add_typing` with
+`apply region_add_typing_for_non_values` in the existing
+`T_Region_Active` `try solve` block at `formal/Semantics.v:3300`-ish.
+
+**Effort**: ~1 hour.
+
+=== Phase 5 — `Admitted.` → `Qed.` + docs sweep
+
+**Goal**: campaign closure. Mechanical (~1 hour).
+
+. **`formal/Semantics.v`** — replace `Admitted.` at the end of
+  `Theorem preservation` with `Qed.` Remove the PROOF STATUS
+  comment block.
+. **`formal/PRESERVATION-HANDOFF.md`** — collapse to a one-line
+  "preservation is Qed as of YYYY-MM-DD" tombstone.
+. **`PROOF-NEEDS.md`** — flip "Coq admitted proofs remaining: 1" to
+  "0". Drop the "what needs proving" entry for `preservation`.
+. **`ROADMAP.adoc`** — flip the v0.1 checkbox; update the Coq table
+  row; remove this entire "Preservation closure plan" section
+  (replace with a 1-line "completed" note).
+. **`README.adoc`** — flip the Component status table row; remove
+  the "22 open / 910 closed" qualifiers in Formal foundations.
+. **`EXPLAINME.adoc`** — flip Coq theorem table; remove reduction
+  story.
+. **`CHANGELOG.md`** — entry: "Coq `preservation` closed to `Qed.`
+  via the 910 → 0 reduction chain (PRs #92, #102, #104, #106,
+  #114, #116, [Phase 1 PR], [Phase 2 PR], [Phase 3 PR],
+  [Phase 4 PR])".
+. **Wiki `Proof-status.md`** + **`Home.md`** — flip preservation
+  row to ✅ Qed; replace the reduction story with a one-line
+  "fully discharged" note.
+. **Memory** —
+  `project_ephapax_preservation_closure_plan.md` → mark CAMPAIGN
+  COMPLETE.
+. **`standards#124`** — post closure comment with full PR chain.
+. **GitHub repo description** — drop "preservation 22 open"
+  qualifier.
+
+=== Effort + parallelization summary
+
+[cols="1,2,2"]
+|===
+| Phase | Solo effort | Parallelizable?
+
+| 1 (Lemma B)
+| 3–4 hours
+| Single agent task.
+
+| 2 (Apply Lemma B)
+| 2 hours
+| 4 agents × ~30 min (one per typing-constructor cluster).
+
+| 3 (Region-env weakening)
+| 1–2 days
+| Single agent (research-level).
+
+| 4 (Close S_Region_Step)
+| 1 hour
+| No.
+
+| 5 (Qed flip + docs)
+| 1 hour
+| 2 agents (repo docs + wiki).
+|===
+
+**Sequential ceiling**: ~3 days of focused work.
+**With fan-out**: ~5–7 calendar hours over 2–3 sessions.
+
+=== Risk-adjusted forecast
+
+* **80% likely**: Phases 1+2 land in one session. Phase 3 takes ~1
+  day. Total: 3 sessions, ~10 hours wall-clock.
+* **15% likely**: Lemma B needs context-equivalence (not equality);
+  phase 1 spills into a refinement session.
+* **5% likely**: Phase 3 hits a language-design issue (e.g., need to
+  add a syntactic invariant to the typing rules). If so, the rules
+  get amended and all earlier `Qed`-proofs need re-checking (~1 day
+  detour).
 
 == v0.2.0 — Backend maturity
 

formal/PRESERVATION-HANDOFF.md

@@ -2,18 +2,26 @@
 
 # Hand-off: closing `preservation` in `formal/Semantics.v`
 
-Diagnostic + remediation log. The proof is still `Admitted.`, but as of
-2026-05-20 it's **down from 910 open goals to ~29 real ones** via the
-standard preservation pattern. This file tells whoever picks it up
-next exactly what's open and why.
+Diagnostic + remediation log. The proof is still `Admitted.`, but as
+of **2026-05-21** it's **down from 910 open goals to 12** via four
+landed PRs. This file tells whoever picks it up next exactly what's
+open and what the canonical closure path is.
+
+> **The canonical closure plan is now in `ROADMAP.adoc` §
+> "Preservation closure plan".** This file remains as the per-case
+> diagnostic record. Read ROADMAP first; come back here for case
+> detail.
 
 ## State at a glance
 
 | Date | Open goals | Notes |
 |------|-----------:|-------|
 | 2026-04-27 | "fully closed" | In-file comment — but `coqc` rejected the `Qed.`. The claim was unsubstantiated; the proof never closed. |
 | 2026-05-20 (am) | 910 | Discovered via `Show. Show Existentials.` before the `Admitted.`. Exactly 35 (step rules) × 26 (typing rules). The existing `try solve [...]` chain closes ZERO. |
-| 2026-05-20 (pm) | **29** | After the standard preservation pattern (`remember (mu, R, e) as cfg` + symmetric for cfg', then `inversion Hcfg; subst; inversion Hcfg'; subst;` inside each case). 97% reduction. |
+| 2026-05-20 (pm) | 29 | After the standard preservation pattern (`remember (mu, R, e) as cfg` + symmetric for cfg', then `inversion Hcfg; subst; inversion Hcfg'; subst;` inside each case). 97% reduction. PR #102. |
+| 2026-05-20 (eve) | 22 | After `revert mu R e mu' R' e' Hcfg Hcfg'` before `induction Hstep` so each case's IH carries universal quantification over the inner step's config. PR #106. |
+| 2026-05-20 (eve) | 22 | Region-invariance lemma `step_R_eq_or_touches_region` landed as infrastructure (no goal closures). PR #114. |
+| 2026-05-20 (night) | **12** | 10 β-reduction / value-step cases discharged via per-case manual proofs using the lemma. PR #116. **98.7% reduction across one day.** |
 
 ## What the 910 → 29 fix did