chore: rename k9 directories to self-validating for clarity
chore: migrate license from PMPL-1.0-or-later to MPL-2.0
wiki: refresh 22 → 12 preservation count + extended reduction story Mirrors the companion repo PR #122. After PR #116 closed 10 more preservation goals (22 → 12) and PR #121 landed the Phase 1 scaffold (Lemma B stated), updates the wiki to reflect: Home.md — 22 → 12 in proof-status-at-a-glance table; reduction-story bullets extended through PR #114, #116, #121; new pointer to ROADMAP §'Preservation closure plan' as the canonical 12 → 0 path. Proof-status.md — date updated to 2026-05-21; preservation row says '12 open goals'; reduction story now has five passes (was three): added region-invariance lemma (#114), per-case closures (#116), and Phase 1 scaffold (#121); '22 → 0' section replaced with '12 → 0 (canonical closure plan -- see ROADMAP)' summarising the 5-phase plan. What-can-go-wrong.md — '22 open / 910 closed' → '12 open / 910 closed' in the closing paragraph. Comparison-to-other-languages.md — '910 closed, 22 open' → '910 closed, 12 open'. Glossary.md — '22 open / 910 closed' → '12 open / 910 closed' in the preservation entry. One occurrence of '29 → 22 goals' is retained in Home.md as intentional reduction-step history.
wiki: correct Idris2 region-linearity theorem names The 2026-05-20 wiki refresh used the wrong names for two region-linearity theorems: regionSafetyTheorem -> regionSafetyExtract (actual name) noGCTheorem -> noGCExtract (actual name) Also corrected file paths: all four theorems live in `Ephapax/Formal/RegionLinear.idr` (not separate `RegionSafety.idr`/`NoGC.idr`/`NoEscape.idr`/`Orthogonality.idr` files, which don't exist). Files updated: - Home.md (1 occurrence each) - Region-calculus.md (5 occurrences across 2 sections) - Proof-status.md (5-row table — names and paths corrected; line numbers added per-theorem for direct navigation)
wiki: refresh for 2026-05-20 state — add Proof-status page + sidebar nav Home.md rewritten as a navigation hub for outside readers: - 'Start here, by audience' table routes new readers to the right quickstart per role. - 'What is Ephapax?' summary positioned for an outside observer. - Proof status at a glance with the preservation reduction story (910 -> 22) and the Idris2 totality campaign outcome. - 'Documentation by topic' indexes every other repo .adoc/.md. - 'Highest-leverage open work' prioritised contribution roadmap. - 'Related projects' updated to include echo-types and corrected links. New Proof-status.md is the canonical 'what's proven / what's open' page with per-lemma table for Coq (Qed list + the 22-goal preservation breakdown) and per-file table for the Idris2 frontend totality campaign. Links every relevant PR (#89-#100 Idris2 + #92/#102/#104/#106 Coq preservation chain). New _Sidebar.md provides persistent navigation across wiki pages.
Create wiki Home page with project overview