Merge main into proofs/p43 — resolve Print Assumptions block conflict (#270 audit + this PR's canonical_*_l1_m blocks)

# Conflicts:
#	formal/Semantics_L1.v

Author: hyperpolymath

.github/workflows/coq-build.yml

@@ -84,25 +84,30 @@ jobs:
     needs: detect-relevant-changes
     if: needs.detect-relevant-changes.outputs.relevant == 'true'
     runs-on: ubuntu-latest
-    # coq:8.18 matches the toolchain pinned by formal/Justfile and the
-    # local developer setup. Pin to a digest later once a stable
-    # known-good image is decided on; for now the floating tag mirrors
-    # `make` semantics — "what the maintainer's machine has".
-    container:
-      image: coqorg/coq:8.18
-      # actions/checkout's post-step writes to /__w/_temp/_runner_file_commands
-      # via Node fs.writeFileSync. The coqorg/coq image defaults to the
-      # non-root `coq` user (UID 1000), but the runner mounts /__w as the
-      # host runner user — EACCES until checkout's saveState. Running the
-      # container as root keeps the workspace-shared paths writable while
-      # leaving the in-container build untouched (root in container is
-      # still mapped to the runner host's runner user, not host-root).
-      options: --user root
+    # Coq 8.18 via Ubuntu 24.04 noble apt (coq 8.18.0+dfsg) exactly
+    # matches the toolchain pinned by formal/Justfile and the local
+    # developer setup.
+    #
+    # Why not the `coqorg/coq:8.18` container? Previously this job ran
+    # it with `--user root` to dodge the EACCES from checkout writing
+    # to a runner-user-owned /__w mount. But the image only configures
+    # `coqc` on the non-root `coq` user's PATH (via opam env in their
+    # .profile). With `--user root`, no opam env → `coqc: not found` →
+    # exit 127 immediately at the version step. Several proof PRs were
+    # silently blocked while main stayed green (path-filter skipped
+    # main pushes that didn't touch formal/). See the proven 37s
+    # pattern in [[reference_coqorg_image_apt_coq_simpler]] used by
+    # verisimdb#87.
 
     steps:
       - name: Checkout repository
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
 
+      - name: Install Coq 8.18 (noble apt)
+        run: |
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends coq
+
       - name: Coq version (provenance)
         run: |
           coqc --version

.github/workflows/governance.yml

@@ -22,4 +22,4 @@ permissions:
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@d3f799c639420ac68ac7ed83d2166b625b4b73f0
+    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@bf406d6f95c5212c34c30f6629be93d08c076339 # main 2026-06-01 (R5b version-string drift — standards#329)

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
 

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

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
 

Cargo.lock

@@ -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

Cargo.toml

@@ -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
 

EXPLAINME.adoc

@@ -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:

Justfile

@@ -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 |