docs: refresh stale "22 open" → "12 open" + CHANGELOG closure entry (#122)

Closure sweep after PR #116 took preservation from 22 → 12 open goals
and PR #121 landed Phase 1 scaffold. Updates the preservation-count
claims across docs to reflect 12, and adds a CHANGELOG entry summarising
the full 2026-05-20 → 2026-05-21 reduction campaign.

## Files updated

| File | What changed |
|---|---|
| `README.adoc` | Coq formal-foundations paragraph; reduction chain now
lists all 8 PRs through #121; clear pointer to ROADMAP closure plan |
| `ROADMAP.adoc` | Formal-proof status table row (`12 open goals`); v0.1
blocker entry; v1.0 status; 97.6% → 98.7% reduction figure |
| `EXPLAINME.adoc` | Coq theorem table; reduction-story bullets extended
through #114, #116, #121 |
| `CHANGELOG.md` | New "Proof state" + "Documentation" sections under
`[Unreleased]` tracking the full PR chain (#92, #102, #104, #106, #114,
#115, #116, #117, #121) + the Idris2 totality campaign (#89–#100) +
doc/wiki refresh (#113 + wiki) |

## Companion wiki update

`Home.md`, `Proof-status.md`, `What-can-go-wrong.md` updated in the wiki
repo with the same 22 → 12 figures + extended reduction story. Pushed
separately to wiki master.

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

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

Author: hyperpolymath

CHANGELOG.md

@@ -5,6 +5,25 @@ All notable changes to Ephapax are documented here.
 
 ## [Unreleased]
 
+### Proof state (2026-05-20 → 2026-05-21)
+- **Coq `preservation` reduction campaign**: 910 open goals → 12 (98.7% reduction). PR chain:
+  - **#92** — honest framing: replaced unsubstantiated "Qed 2026-04-27" claim with `Admitted.`
+  - **#102** — 910 → 29: standard preservation pattern (`remember (mu, R, e) as cfg`)
+  - **#104** — quantitative status correction in docs
+  - **#106** — 29 → 22: universal-IH revert (`revert mu R e mu' R' e' Hcfg Hcfg'` before `induction Hstep`)
+  - **#114** — region-invariance lemma `step_R_eq_or_touches_region` (Qed-closed; infrastructure)
+  - **#115** — corrected Idris2 region-linearity theorem names in docs
+  - **#116** — 22 → 12: per-case manual closures of 10 β-reduction / value-step constructors
+  - **#117** — canonicalised 5-phase closure plan in ROADMAP §"Preservation closure plan"
+  - **#121** — Phase 1 scaffold: `step_output_context_eq` (Lemma B) stated with induction skeleton
+
+- **Idris2 `%default partial → total` campaign** (2026-05-20): merged 9 PRs (#89, #90, #91, #93, #94, #96, #97, #99, #100) tightening totality across the parser / typechecker / IR-codec layer. 80+ atomic functions now provably total; zero `assert_total` / `believe_me` / `assert_smaller` introduced; 14 retained `covering` markers for documented Idris2 0.8.0 SCT limits.
+
+### Documentation
+- **#113** — README + ROADMAP + EXPLAINME refactored for outside readers; documentation map; quickstart-by-audience; proof status tables.
+- Wiki refresh — `Home.md` rewritten as nav hub; new `Proof-status.md`; 6 topic guides added (Linear-and-affine, Region-calculus, Two-phase-compiler, What-can-go-wrong, Comparison-to-other-languages, Glossary); `_Sidebar.md` for persistent nav.
+- Repo description + topics — added `agda`, `idris2`, `webassembly`, `formal-verification`, `affine-types`, `region-calculus`, `compiler`, `operational-semantics`, `programming-language`.
+
 ### Added
 - **typed-wasm L7+L10 integration** (closes the typed-wasm-verify loop for ephapax):
   - **C6 (#70)** — `ephapax-wasm` emits an `affinescript.ownership` custom section on every compile when any user fn has a Linear parameter. Section format and encoder come from the new `typed-wasm-verify` Rust crate (`hyperpolymath/typed-wasm:crates/typed-wasm-verify/`, rev `e11bb985` at C6, bumped to `67006edd` at C7). Driven by `Ty::is_linear()`; entries sorted by `func_idx` for deterministic output. 4 new unit tests; `cargo test --workspace` clean.

EXPLAINME.adoc

@@ -176,7 +176,7 @@ calculus over the Tofte-Talpin region-linear type system.
 
 | **`preservation`**
 | 🟡 Admitted
-| `formal/Semantics.v` (Theorem at line 3207). **22 open goals** as of 2026-05-20 (was 910). See `formal/PRESERVATION-HANDOFF.md`.
+| `formal/Semantics.v` (Theorem at line 3207). **12 open goals** as of 2026-05-21 (was 910). See ROADMAP §"Preservation closure plan" + `formal/PRESERVATION-HANDOFF.md`.
 |===
 
 The `preservation` reduction story is recent and load-bearing:
@@ -188,11 +188,22 @@ The `preservation` reduction story is recent and load-bearing:
   `induction Hstep`, so each case's IH carries clean universal
   quantification over the inner step's config rather than the
   inconsistent outer-cfg equation. Lands as PR #106.
-* The remaining 22 need (a) region invariance for non-region step
-  constructors, (b) linearity-context preservation for sibling
-  premises in congruence cases, (c) the documented region-env
-  weakening lemma for non-values (the S_Region_Step + T_Region_Active
-  case the in-file comment originally identified as "the one open").
+* **22 → 12 goals** via per-case manual proofs using the new
+  `step_R_eq_or_touches_region` region-invariance lemma (PR #114
+  for the lemma, PR #116 for the 10 case closures: β-reduction,
+  value-step, and atomic cases like `S_Let_Val`, `S_App_Fun`,
+  `S_If_True/False`, `S_Fst`, `S_Snd`, `S_Case_Inl/Inr`, `S_Copy`).
+* **Phase 1 scaffold landed** (PR #121): `step_output_context_eq`
+  (Lemma B) stated with induction-on-step skeleton. Per-case
+  discharges are the next session's substantive work.
+* The remaining 12 are 11 congruence cases blocked on Lemma B
+  (linearity-context drift between IH's output context and
+  sibling's pre-context) + 1 `S_Region_Step + T_Region_Active`
+  case blocked on the documented region-env weakening lemma for
+  non-values.
+
+The canonical closure path is **`ROADMAP.adoc` §"Preservation
+closure plan"** — 5 phases, ~3 sessions of focused work.
 
 An earlier in-file comment (corrected by PR #92, 2026-05-20) claimed
 preservation was Qed-closed on 2026-04-27. That claim was

README.adoc

@@ -209,14 +209,18 @@ Currently `Qed`-closed: `no_leaks`, `subst_preserves_typing`,
 `typing_ctx_transfer`, `region_env_perm_typing`, `region_add_typing`,
 `region_shrink_preserves_typing`, plus 70+ supporting lemmas.
 
-Currently `Admitted`: `preservation`. **22 open goals remain** after
-the in-flight reduction chain — down from **910** at the start of the
-campaign (PRs #92 / #102 / #104 / #106, 2026-05-20). The remaining 22
-need (a) a region-invariance lemma for non-region step constructors,
-(b) a linearity-context preservation lemma for sibling premises in
-congruence cases, and (c) the documented S_Region_Step language-design
-item (region-env weakening for non-values). See
-`formal/PRESERVATION-HANDOFF.md` for the per-case checklist.
+Currently `Admitted`: `preservation`. **12 open goals remain** after
+the reduction chain — down from **910** at the start of the campaign
+(98.7% reduction across PRs #92 / #102 / #104 / #106 / #114 / #116 /
+#117 / #121, 2026-05-20 → 2026-05-21). Phase 1 scaffold of the
+closure plan (Lemma B `step_output_context_eq`) landed; per-case
+discharges next. The remaining 12 are 11 congruence cases (blocked
+on Lemma B's per-case proofs — linearity-context drift between IH
+and sibling) + 1 `S_Region_Step + T_Region_Active` case (blocked on
+region-env weakening for non-values). Canonical closure path:
+**`ROADMAP.adoc` §"Preservation closure plan"** (5 phases, ~3
+sessions of focused work). See also `formal/PRESERVATION-HANDOFF.md`
+for the per-case diagnostic record.
 
 [source,bash]
 ----

ROADMAP.adoc

@@ -55,7 +55,7 @@ substitution semantics:
 
 | **`preservation`**
 | 🟡 Admitted
-| **22 open goals** after the in-flight reduction chain (PRs #92 / #102 / #104 / #106). Started at 910 cross-case open goals; reduced by 97.6% via standard preservation pattern + universal-IH revert. Remaining 22 need region-invariance + linearity-context preservation lemmas + the documented S_Region_Step language-design item (region-env weakening for non-values). See `formal/PRESERVATION-HANDOFF.md` for per-case checklist.
+| **12 open goals** after the reduction chain (PRs #92 / #102 / #104 / #106 / #114 / #116 / #117 / #121). Started at 910; 98.7% reduced. Phase 1 scaffold (Lemma B `step_output_context_eq`) landed; per-case discharges next. Remaining 12 = 11 congruence cases (blocked on Lemma B per-case closure) + 1 region case (`S_Region_Step + T_Region_Active`, blocked on region-env weakening). Canonical closure path: ROADMAP §"Preservation closure plan" below.
 |===
 
 **Historical note**: an earlier in-file comment claimed `preservation`
@@ -398,7 +398,8 @@ audio buffer management:
 == v1.0.0 — Production ready
 
 * [ ] **All Coq `Admitted` proofs closed in `formal/Semantics.v`**
-      (currently 1: `preservation` with 22 open goals; see Status above)
+      (currently 1: `preservation` with 12 open goals; see
+      <<preservation-closure-plan,Preservation closure plan>>)
 * [ ] Idris2 `Parse/Parser.idr` upgraded from `%default covering` to
       `%default total` (LL(k) fuel-refactor; deferred separate campaign)
 * [ ] Stable surface syntax (already locked, but confirm no changes needed)