hyperpolymath · hyperpolymath · Jun 1, 2026 · Jun 1, 2026
diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
@@ -13,13 +13,14 @@ This is the AI manifest for **ephapax**. It declares:
 
 ### Machine-Readable Metadata: `.machine_readable/6a2/` ONLY
 
-These 6 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY:
+These 7 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY:
 1. **STATE.a2ml** - Project state, progress, blockers
 2. **META.a2ml** - Architecture decisions, governance
 3. **ECOSYSTEM.a2ml** - Position in ecosystem, relationships
 4. **AGENTIC.a2ml** - AI agent interaction patterns
 5. **NEUROSYM.a2ml** - Neurosymbolic integration config
 6. **PLAYBOOK.a2ml** - Operational runbook
+7. **ANCHOR.a2ml** - Canonical authority + project recalibration trigger (SSG / cartridge / parent-relationship metadata; template from `hyperpolymath/standards`)
 
 ## CORE INVARIANTS
 

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,18 +1,46 @@
-<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 # Changelog
 
 All notable changes to Ephapax are documented here.
 
 ## [Unreleased]
 
+### Phase 3b Stage 1a + 1b — L2 effect-typed TFun + L3 wiring conditional preservation (2026-05-30 → 2026-05-31)
+
+- **Stage 1a (PR #252, merged 2026-05-30 17:42Z)**: `tfuneff_lambda_free`
+  + `Counterexample_L2_nested.v`. Admin-merged after local build oracle
+  GREEN with no axiom slippage (only the known-good
+  `region_liveness_at_split_l1_gen` axiom).
+- **Stage 1b (PR #253)**: L1/L2 plumbing for the effect-typed `TFun` track —
+  `expr_closed_below` + closure helpers (Syntax.v), body-transfer + closed-
+  value G-poly helpers, `subst_typing_gen_l1_m_tfuneff` Qed (zero axioms),
+  and `preservation_l2` β-case for closed `TFunEff` substituents. Builds
+  toward the unconditional `preservation_l2` track per
+  `PRESERVATION-DESIGN.md §12.x`.
+
+### L3 wiring + L4 Phase A scaffold (2026-05-27 → 2026-05-28)
+
+- **L3 wiring (slice 4, 2026-05-27)**: `preservation_l3_region_active_echo`,
+  `preservation_l3_drop_echo`, and the `preservation_l3` umbrella all Qed in
+  `formal/Semantics_L1.v` — each conditional on the
+  `region_shrink_preserves_typing_l1_gen_m` L1 structural admit. The
+  avoidable `T_Region_L1_Echo` mirror was closed in the same slice. Zero new
+  admits introduced.
+- **L4 Phase A scaffold (2026-05-28)**: `formal/L4.v` lands with `ProgramMode`
+  (`PModeLinear` / `PModeAffine` / `PModeBoundaryMix`) and
+  `program_mode_to_modality` round-trip. Definitions only by design — no
+  theorems, no admits, no axioms.
+
 ### Four-layer preservation redesign (2026-05-26 → 2026-05-27)
 
 - **L1 — region capabilities** (PRs #153-line, integration branch
   `proof/l1-region-threading-design`): introduces `has_type_l1` with
   R-threading in `formal/TypingL1.v`. Supporting lemmas in
   `formal/Semantics_L1.v`. Counterexample regression (`bad_input_untypable_l1`)
-  Qed in `formal/Counterexample.v`. `preservation_l1` Admitted with 4
-  residual admits in R-weakening territory.
+  Qed in `formal/Counterexample.v`. `preservation_l1` Admitted with 1
+  residual inner `admit.` covering App / Pair / StringConcat (lambda-
+  rigidity gap per `PRESERVATION-DESIGN.md §4.8`).
 - **L2 — Linear/Affine modality** (PR #176, this entry): `has_type_l1`
   carries `m : Modality` parameter so a single judgment specialises to
   ephapax-linear AND ephapax-affine. New `formal/Modality.v` with K-free

diff --git a/CLAUDE.md b/CLAUDE.md
@@ -1,5 +1,7 @@
 <!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- SPDX-License-Identifier: MPL-2.0 -->
 <!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+<!-- Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
 # CLAUDE.md — Ephapax repo agent guidance
 
@@ -36,14 +38,15 @@ https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation
 
 ## Machine-readable artefacts
 
-Structured project metadata lives in `.machine_readable/6a2/`:
+Structured project metadata lives in `.machine_readable/6a2/` (7 files):
 
 - `STATE.a2ml` — current project state and progress.
 - `META.a2ml` — architecture decisions and development practices.
 - `ECOSYSTEM.a2ml` — position in the ecosystem and related projects.
 - `AGENTIC.a2ml` — AI agent interaction patterns (also carries an `@disambiguation` block).
 - `NEUROSYM.a2ml` — neurosymbolic integration config.
 - `PLAYBOOK.a2ml` — operational runbook.
+- `ANCHOR.a2ml` — canonical authority and project recalibration trigger (template from `hyperpolymath/standards`); declares SSG / cartridge / parent-relationship metadata.
 
 ## The four orthogonal layers
 

diff --git a/Cargo.toml b/Cargo.toml
@@ -52,9 +52,11 @@ ephapax-package = { path = "src/ephapax-package" }
 ephapax-vram-cache = { path = "src/ephapax-vram-cache" }
 
 # Sibling-repo crates.
-# NOTE: rev pin currently points at typed-wasm#65 branch HEAD for the
-# `typedwasm.ownership` section rename. RE-BUMP to the post-merge SHA
-# on `origin/main` before this PR merges.
+# NOTE: rev pin is the post-merge SHA of typed-wasm#65 on
+# `hyperpolymath/typed-wasm:origin/main` (renames the custom section
+# `affinescript.ownership` → `typedwasm.ownership`). This is the
+# canonical C7 pin (cf. CHANGELOG.md "Added" / "C7 (#72)"). Re-bump
+# only if a newer `typed-wasm-verify` API change is needed.
 typed-wasm-verify = { git = "https://github.com/hyperpolymath/typed-wasm", rev = "a1935c16176567e0470de2feedf9c37a87dc0158" }
 
 # External dependencies

diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
@@ -1,4 +1,5 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = Ephapax — Show Me The Receipts
 :toc:
 :toclevels: 3
@@ -98,13 +99,15 @@ soundness invariant the legacy judgment was missing.
   carries the R-threading directly. Step relation at
   `formal/Semantics_L1.v`.
 * Design rationale at `formal/PRESERVATION-DESIGN.md §3-§4`.
-* Status: judgment landed; 9 L1 supporting-lemma admits remain as
-  L2-integration debt (tracked in `PROOF-NEEDS.md`).
+* Status: judgment landed; `Semantics_L1.v` carries 3 outer
+  `Admitted.` markers covering 5 inner `admit.` cases — pre-existing
+  L1 structural debt + parallel mirrors (file:line breakdown in
+  `PROOF-NEEDS.md §4`).
 
-== Claim: Irreversibility residue is first-class (L3, planned)
+== Claim: Irreversibility residue is first-class (L3, wired)
 
-*Evidence (planned)*: Operations that erase information (region
-exit, drop) will produce typed residue witnesses, following the
+*Evidence*: Operations that erase information (region exit, drop)
+produce typed residue witnesses, following the
 https://github.com/hyperpolymath/echo-types[echo-types]
 formulation. Linear mode requires the residue to be observed;
 Affine mode permits silent lowering.
@@ -115,9 +118,13 @@ Affine mode permits silent lowering.
 * Local mirror at `formal/Echo.v` — the L3 calculus is mechanised
   here (modes, `LEcho`, `weaken`, `degrade_mode`, all `Qed`).
 * Forward-looking design at `formal/PRESERVATION-DESIGN.md §6`.
-* Status: **planned** integration — `Echo.v` is wired up
-  internally, but no ephapax typing rule yet introduces `TEcho`.
-  The L3 extension follows L1's residual admit closure.
+* Status: **wiring landed** (slice 4, 2026-05-27).
+  `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`,
+  and the `preservation_l3` umbrella in `Semantics_L1.v` are all
+  Qed, each conditional on the
+  `region_shrink_preserves_typing_l1_gen_m` L1 structural admit.
+  Remaining L3 work is unconditional `preservation_l3` (Phase 3b
+  Stage 2).
 
 == Claim: Dyadic mode is project-level only (L4)
 
@@ -242,33 +249,37 @@ theorem.
 | `formal/TypingL1.v` — modality-indexed, R-threaded
 
 | L1 semantics
-| 🟡 15 Qed, 9 admits (L2-integration debt)
-| `formal/Semantics_L1.v` — 9 admits are bullet-structure rewrites for new Affine-only constructors, *not* legacy patching
+| 🟡 37 Qed, 3 Admitted (5 inner admits — pre-existing L1 structural debt + parallel mirrors)
+| `formal/Semantics_L1.v` — 3 outer `Admitted.` markers cover 5 internal `admit.` cases. Per `PROOF-NEEDS.md §4`: pre-existing L1 structural debt (multiset/list-perm bridge + L2 effect-typed `TFun` per PRESERVATION-DESIGN.md §5.1 + lambda-rigidity at `preservation_l1` body) and two parallel mirrors that close mechanically when their originals close.
 
 | L2 modality (`Modality.v`)
 | ✅ Core landed (1 Qed, 0 axioms)
 | `formal/Modality.v` + `m : Modality` in `has_type_l1`. PRs #176 + #177. `linear_to_affine` Qed with zero axioms.
 
 | L3 echo / residue calculus
-| ✅ 12 Qed, 0 admits (calculus); ⏳ integration pending
-| `formal/Echo.v` — one type former (fiber `Echo f y := Σ x. f x ≡ y`) + degrade map + no-section-collapse-to-residue proof. Not yet wired into `has_type_l1` or step rules.
+| ✅ Calculus 12 Qed + wiring landed (slice 4, 2026-05-27)
+| `formal/Echo.v` — one type former (fiber `Echo f y := Σ x. f x ≡ y`) + degrade map + no-section-collapse-to-residue proof. Wiring lemmas (`preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, `preservation_l3` umbrella) in `Semantics_L1.v` — all Qed, conditional on `region_shrink_preserves_typing_l1_gen_m`.
 
 | L4 dyadic interaction
-| 🔲 Not started
-| Design in `formal/PRESERVATION-DESIGN.md §7`.
+| ✅ Phase A scaffold landed (`formal/L4.v`, 2026-05-28); definitions only
+| `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` enum + `program_mode_to_modality` round-trip. No theorems by design. Design in `formal/PRESERVATION-DESIGN.md §7`.
 
 | Legacy `Theorem preservation` (`formal/Semantics.v`)
 | 🛑 Provably false (Admitted)
 | Pinned by `Counterexample.v`. **Do not attempt closure.** Archaeology.
 |===
 
 What's done = `Modality.linear_to_affine` (Linear ⇒ Affine weakening,
-zero axioms), the L1 judgment, L3 fiber + degrade calculus, and the
-counterexample regression witness. What's todo = close the 9
-Semantics_L1 admits (L2-integration debt), wire L3 into the typing
-judgment + step rules, then state per-layer preservation. What's
-banned = closing the legacy theorem, adding new `Axiom` declarations
-to discharge L1/L2 gaps, conflating `ephapax-affine` (this repo's
+zero axioms), the L1 judgment, L3 fiber + degrade calculus, L3
+wiring into the L1 step rules (slice 4 — `preservation_l3` umbrella
+Qed conditional on the L1 structural admit), L4 Phase A scaffold
+(definitions only), and the counterexample regression witness.
+What's todo = close the 3 Semantics_L1 outer Admitteds (pre-existing
+L1 structural debt: multiset/list-perm bridge + L2-effect-typed
+`TFun` + lambda-rigidity at `preservation_l1`), then state
+unconditional `preservation_l3` (Phase 3b Stage 2). What's banned =
+closing the legacy theorem, adding new `Axiom` declarations to
+discharge L1/L2 gaps, conflating `ephapax-affine` (this repo's
 sublanguage) with `AffineScript` (a separate language at
 `hyperpolymath/affinescript`). Full per-sublanguage breakdown in
 `PROOF-NEEDS.md`.
@@ -341,7 +352,9 @@ total`.
 
 == Test Evidence
 
-~229 tests across ~19 crates, 0 failures. Key test categories:
+357 tests across 17 active workspace crates + `tests/fuzz`, 0
+failures (per `cargo test --all-targets`; see `TEST-NEEDS.md` for
+the per-crate breakdown). Key test categories:
 
 * *Type checker dyadic tests*: `let` vs `let!` semantics, branch
   agreement, region exit (`ephapax-typing`)
@@ -352,8 +365,8 @@ total`.
 * *Discipline tests*: linear vs affine checker divergence
   (`ephapax-linear`)
 * *Integration tests*: parse → desugar → typecheck end-to-end
-* *Conformance tests*: `conformance/pass/` programs must type-check,
-  `conformance/fail/` programs must be rejected
+* *Conformance tests*: `conformance/valid/` programs must type-check,
+  `conformance/invalid/` programs must be rejected
 
 == Design Documents
 

diff --git a/Justfile b/Justfile
@@ -47,7 +47,7 @@ lint:
 
 # Run panic-attacker pre-commit scan
 assail:
-    @command -v panic-attack >/dev/null 2>&1 && panic-attack assail . || echo "panic-attack not found — install from https://github.com/hyperpolymath/panic-attacker"
+    @command -v panic-attack >/dev/null 2>&1 && panic-attack assail . || echo "panic-attack not found — install from https://github.com/hyperpolymath/panic-attack"
 
 # Format code
 fmt:

diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
@@ -1,4 +1,4 @@
-<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- SPDX-License-Identifier: MPL-2.0 -->
 <!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
 # Proof needs — Ephapax (linear + affine sublanguages)
@@ -233,6 +233,15 @@ to the owner**:
 
 ## §4. Counts + file-by-file map
 
+<!-- status-gate marker: do not move. scripts/status-gate.sh reads this line. -->
+Coq admitted proofs remaining: 4
+
+(1 outer `Admitted.` in `formal/Semantics.v` — sacrosanct legacy
+preservation, provably false per `Counterexample.v` + 3 outer
+`Admitted.` markers in `formal/Semantics_L1.v` covering 5 internal
+`admit.` cases — all pre-existing L1 structural debt + parallel
+mirrors. See the per-file table and seam audit below.)
+
 ### Per-file Qed / Admitted summary (as of 2026-05-28)
 
 | File | Qed | Admitted | Disposition |

diff --git a/README.adoc b/README.adoc
@@ -4,8 +4,8 @@ image:https://img.shields.io/badge/Philosophy-Palimpsest-indigo.svg[Palimpsest,l
 image:https://github.com/hyperpolymath/ephapax/actions/workflows/codeql.yml/badge.svg?branch=main[CodeQL,link="https://github.com/hyperpolymath/ephapax/actions/workflows/codeql.yml"]
 image:https://api.thegreenwebfoundation.org/greencheckimage/ephapax.org[Green Hosting,link="https://www.thegreenwebfoundation.org/green-web-check/?url=ephapax.org"]
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
-// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :toc: macro
 :toclevels: 3
 :icons: font
@@ -62,10 +62,13 @@ link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`]
 
 Quick read: **L1** (region capabilities) substantially complete;
 **L2** (Linear/Affine modality) core landed with zero axioms; **L3**
-(echo / residue) calculus done locally, integration into the typing
-judgment is the next-block work; **L4** (dyadic mode) mechanical
-scaffold landed (`formal/L4.v` — definitions only by design; no proof
-obligations).
+(echo / residue) wiring landed (slice 4, 2026-05-27): `preservation_l3`
++ `preservation_l3_region_active_echo` + `preservation_l3_drop_echo`
+all Qed (conditional on L1 structural admits — see PROOF-NEEDS.md §4);
+**L4** (dyadic mode) Phase A scaffold landed 2026-05-28 (`formal/L4.v`
+— `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + the
+`program_mode_to_modality` round-trip; definitions only by design, no
+proof obligations).
 ====
 
 Ephapax is a research language for **principled handling of
@@ -278,7 +281,7 @@ system can *prove* properties about:
   (affine-ish, with linearisation via `Drop`). Ephapax separates the
   two disciplines explicitly: `let` is affine, `let!` is linear, and
   the user chooses per-binding.
-* **Not a research vapourware.** ~19 Rust crates exist; the lexer,
+* **Not a research vapourware.** 17 active Rust workspace crates + `tests/fuzz` (with `src/ephapax-tools/` outside the workspace and `src/ephapax-vram-cache/` explicitly disabled — needs `hyperpolymath/ephapax-proven`); the lexer,
   parser, interpreter, REPL, CLI, S-expression IR, two-phase pipeline,
   Zig FFI, and conformance test suite are complete. Type checker and
   WASM codegen are in progress. See `ROADMAP.adoc`.
@@ -325,7 +328,7 @@ fn process(input: i32) -> i32 {
 }
 ----
 
-More examples in `examples/` and `conformance/pass/`.
+More examples in `examples/` and `conformance/valid/`.
 
 == Quickstart
 
@@ -416,9 +419,11 @@ based calculus. Post-2026-05-26 the formalisation is layered:
   `formal/Semantics_L1.v`). The new judgment is modality-indexed
   (`has_type_l1 m : ...`) and threads a capability environment `R`
   through compound rules. Judgment 100% (0 admits, 2 Qed); semantics
-  carries 9 supporting-lemma admits that are *L2-integration debt*
-  (bullet-structure rewrites for new Affine-only constructors), not
-  legacy patching.
+  carries 3 outer `Admitted.` markers covering 5 internal `admit.`
+  cases — pre-existing L1 structural debt (multiset / list-perm bridge
+  + L2 effect-typed `TFun` per PRESERVATION-DESIGN.md §5.1) and two
+  parallel mirrors, not legacy patching. See PROOF-NEEDS.md §4 for the
+  file:line classification.
 
 * **Layer 2 — structural modality** (`formal/Modality.v`). Linear
   vs Affine as a K-free thin-poset decoration. `linear_to_affine`
@@ -429,13 +434,17 @@ based calculus. Post-2026-05-26 the formalisation is layered:
   `no-section-collapse-to-residue` irreversibility theorem (mirrors
   the upstream Agda development at
   https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`]).
-  Calculus is done; *wiring into the typing rules* (`T_Observe`,
-  collapse-function emission on irreversible steps,
-  `G`-context threading) is the next-block work.
-
-* **Layer 4 — dyadic interaction**. Design in
-  link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md §7`].
-  Not started.
+  Wiring into the L1 typing rules landed via slice 4 (2026-05-27):
+  `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`,
+  and the `preservation_l3` umbrella are all Qed (conditional on the
+  `region_shrink_preserves_typing_l1_gen_m` L1 structural admit).
+
+* **Layer 4 — dyadic interaction**. Phase A scaffold landed
+  2026-05-28: `formal/L4.v` defines `ProgramMode`
+  (`PModeLinear` / `PModeAffine` / `PModeBoundaryMix`) and the
+  `program_mode_to_modality` round-trip. No theorems by design
+  (definitions only — labelling discipline, not a proof layer). Design
+  in link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md §7`].
 
 Per-sublanguage proof debt with explicit do-not-do list lives in
 link:PROOF-NEEDS.md[`PROOF-NEEDS.md`]. The four-layer architecture
@@ -582,20 +591,20 @@ generics, effects, traits, comptime, contracts) lives on
 | Counterexample at `formal/Counterexample.v` (5 Qed). Not closable. Archaeology.
 
 | Coq L1 (region capabilities)
-| ✅ Judgment 100%; 🟡 semantics 9 admits
-| 9 admits = L2-integration debt. See `PROOF-NEEDS.md`.
+| ✅ Judgment 100%; 🟡 semantics 3 Admitted (5 inner admits)
+| 3 outer `Admitted.` markers cover 5 internal `admit.` cases — pre-existing L1 structural debt + parallel mirrors. Refresh PROOF-NEEDS.md §4 for the file:line breakdown.
 
 | Coq L2 (modality)
 | ✅ Core landed (PRs #176 + #177); 0 axioms
 | `linear_to_affine` Qed. Integration debt absorbed by L1 admits above.
 
 | Coq L3 (echo / residue calculus)
-| ✅ 12 Qed, 0 admits
-| Calculus done locally; integration into typing rules pending.
+| ✅ Wiring landed (slice 4, 2026-05-27); 0 admits in `Echo.v`
+| `preservation_l3` (umbrella) + `preservation_l3_region_active_echo` + `preservation_l3_drop_echo` all Qed (conditional on `region_shrink_preserves_typing_l1_gen_m` L1 structural admit). 12 Qed in `Echo.v` for the underlying calculus.
 
 | Coq L4 (dyadic interaction)
-| 🔲 Not started
-| Design in `formal/PRESERVATION-DESIGN.md §7`.
+| ✅ Phase A scaffold landed (`formal/L4.v`, 2026-05-28); definitions only
+| `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + `program_mode_to_modality` round-trip. No theorems by design; design in `formal/PRESERVATION-DESIGN.md §7`.
 
 | Idris2 region-linearity theorems
 | ✅ Complete (zero unsafe)