Pillar E primer + related work + estate PMPL→MPL-2.0 sweep (harden integration)

.editorconfig

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 root = true
 
 [*]

.envrc

@@ -1,2 +1,2 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 use flake

.github/workflows/agda.yml

@@ -1,5 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
-# (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)
+# SPDX-License-Identifier: MPL-2.0
 
 name: Agda
 
@@ -199,3 +198,28 @@ jobs:
           agda --ignore-interfaces -i proofs/agda proofs/agda/Smoke.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/characteristic/All.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda
+
+  flake-check:
+    # Foundation P1: the reproducible, exactly-pinned toolchain.
+    # `nix flake check` runs flake.nix's hermetic `checks.suite`
+    # (flake-pinned Agda + PINNED stdlib v2.3 + PINNED absolute-zero
+    # @3ff5cee, guardrail + 4 roots + N5 xfail). ADDITIVE: the apt
+    # `check` and `cold-check` jobs remain the gate, so a version
+    # delta surfaced here (e.g. 2.7.0.1 vs verified 2.8.0) is
+    # informative, not a regression. Its first green run IS the P1
+    # verification (the dev env has no nix; CI is the verifier).
+    # Flip continue-on-error to false once it is first green.
+    runs-on: ubuntu-latest
+    continue-on-error: true
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+
+      - name: Install Nix (pinned action)
+        uses: cachix/install-nix-action@08dcb3a5e62fa31e2da3d490afc4176ef55ecd72  # v30
+        with:
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+
+      - name: nix flake check (hermetic, reproducible)
+        run: nix flake check --print-build-logs

.github/workflows/governance.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # governance.yml — single wrapper calling the shared estate governance bundle
 # in hyperpolymath/standards instead of carrying per-repo copies.
 #

.github/workflows/hypatia-scan.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # Hypatia Neurosymbolic CI/CD Security Scan
 name: Hypatia Security Scan
 

.github/workflows/mirror.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
 name: Mirror to Git Forges
 

.github/workflows/scorecard.yml

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 name: OSSF Scorecard
 on:
   push:

.machine_readable/6a2/AGENTIC.a2ml

@@ -14,7 +14,7 @@
 ;;; closed questions, redo superseded work, or violate forbidden
 ;;; rebrandings.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types agentic)

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -13,7 +13,7 @@
 ;;; session understands echo-types' position in the constellation
 ;;; without re-deriving it.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types ecosystem)
@@ -101,10 +101,11 @@
      (source . "Standing decision sd-003 in STATE.scm")
      (artefacts . (".github/workflows/mirror.yml" "MIRROR_SETUP.adoc")))
 
-    ((convention . "License: PMPL-1.0-or-later for code and docs")
-     (source . "META.scm SPDX header pattern; constellation default")
-     (artefacts . ("LICENSE-PMPL-1.0.txt" ; if present
-                   "SPDX headers in all .scm files")))
+    ((convention . "License: MPL-2.0 for code (PMPL retained as narrative/cultural overlay only; see docs/PMPL-NARRATIVE.adoc — owner direction 2026-05-20)")
+     (source . "META.scm SPDX header pattern; owner direction 2026-05-20 supersedes PMPL-1.0-or-later policy")
+     (artefacts . ("LICENSE" ; MPL-2.0
+                   "docs/PMPL-NARRATIVE.adoc" ; cultural overlay
+                   "SPDX headers in all .a2ml files")))
 
     ((convention . "Cross-platform builds: Linux primary, Windows secondary")
      (source . "Standing decision sd-004 in STATE.scm")

.machine_readable/6a2/META.a2ml

@@ -6,7 +6,7 @@
 ;;; Schema reference:
 ;;;   github.com/hyperpolymath/standards/blob/main/meta-a2ml/spec/abnf/meta.abnf
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types meta)

.machine_readable/6a2/NEUROSYM.a2ml

@@ -13,7 +13,7 @@
 ;;; it implies, and what was deliberately NOT proved (PATH B
 ;;; obligations).
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types neurosym)

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -14,7 +14,7 @@
 ;;; (architectural decisions) and gated by AGENTIC.scm. PLAYBOOKs
 ;;; introduce no new authority; they execute permitted plans.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types playbook)

.machine_readable/6a2/STATE.a2ml

@@ -12,7 +12,7 @@
 ;;; concluded; the verdict is negative; the documentation cascade has been
 ;;; applied; the recipe is no longer a candidate locus of distinctness.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types ei-2 state)
@@ -36,7 +36,7 @@
     (canonical-host . github)                ; per current forge workflow
     (mirrors        . (gitlab codeberg))
     (version-target . "0.1.1")
-    (license        . "PMPL-1.0-or-later")))
+    (license        . "MPL-2.0")))
 
 ;;; ============================================================
 ;;; Session header

0-AI-MANIFEST.a2ml

@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; 0-AI-MANIFEST.a2ml — echo-types
 
 [ai-contract]

Containerfile

@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # Containerfile — podman-build fallback when stapeln is unavailable.
 
 # TODO(scaffold): pin @sha256

EXPLAINME.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = echo-types: explain me
 :icons: font
 

QUICKSTART-DEV.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-DEV: echo-types
 :toc:
 

QUICKSTART-MAINTAINER.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-MAINTAINER: echo-types
 :toc:
 

QUICKSTART-USER.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-USER: echo-types
 :toc:
 

README.md

@@ -1,10 +1,10 @@
-<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- SPDX-License-Identifier: MPL-2.0 -->
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
 # echo-types
 
 [![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echo-types)
-[![License: PMPL-1.0](https://img.shields.io/badge/License-PMPL--1.0-blue.svg)](https://github.com/hyperpolymath/palimpsest-license)
+[![License: MPL-2.0](https://img.shields.io/badge/License-MPL--2.0-blue.svg)](https://www.mozilla.org/en-US/MPL/2.0/)
 [![Green Web](https://api.thegreenwebfoundation.org/greencheckimage/github.com)](https://www.thegreenwebfoundation.org/green-web-check/?url=github.com)
 
 Constructive Agda development for echo types as a first-class notion of structured loss:

TOPOLOGY.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = echo-types: topology
 :toc:
 

arghda-core/Cargo.toml

@@ -3,7 +3,7 @@ name = "arghda-core"
 version = "0.1.0"
 edition = "2021"
 description = "Lightweight proof-workspace manager for Agda"
-license = "PMPL-1.0-or-later"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/echo-types"
 
 [[bin]]

contractiles/Dustfile.a2ml

@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Dustfile.a2ml — recovery & rollback for echo-types.
 
 (contractile :kind dust :version 1)

contractiles/Intentfile.a2ml

@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Intentfile.a2ml — declared future intent for echo-types.
 
 (contractile :kind intent :version 1)

contractiles/Mustfile.a2ml

@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Mustfile.a2ml — physical state invariants for echo-types.
 
 (contractile :kind must :version 1)

contractiles/Trustfile.a2ml

@@ -1,11 +1,11 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Trustfile.a2ml — integrity & provenance for echo-types.
 
 (contractile :kind trust :version 1)
 
 (trust license-content
   :doc "LICENSE contains expected SPDX identifier."
-  :cmd "grep -q 'PMPL\\|License' LICENSE")
+  :cmd "grep -q 'Mozilla Public License' LICENSE")
 
 (trust no-secrets-committed
   :doc "No credential files committed."

docs/PMPL-NARRATIVE.adoc

@@ -0,0 +1,106 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= PMPL as Narrative Overlay
+:toc: macro
+:toclevels: 2
+:sectnums:
+:icons: font
+
+[.lead]
+This repository is licensed under *MPL-2.0* (see `LICENSE`). The
+*PMPL* (Palimpsest-MPL) name remains as a *narrative / cultural /
+discipline overlay* documented here, NOT as an SPDX identifier and
+NOT as a separate legal text. This file exists to record what the
+PMPL framing contributes that the bare MPL-2.0 identifier does not.
+
+== Policy in one paragraph
+
+*Stated licence (legal):* MPL-2.0. This is the licence the SPDX
+headers carry, the LICENSE file contains, the README badge displays,
+and downstream consumers / registries / scanners see. There is no
+"PMPL-1.0-or-later" SPDX identifier in this repository.
+
+*PMPL (narrative):* the working-discipline framing under which this
+code was developed. Palimpsest-MPL was, in its prior incarnation, an
+overlay licence whose text incorporated MPL-2.0 by reference. The
+owner direction of 2026-05-20 collapsed the overlay into MPL-2.0
+proper and lifted the *posture* it represented into this narrative
+document. No legal content was lost: PMPL's operative legal effect
+*was* MPL-2.0 (lawyer-confirmed). What was discarded is a stated
+SPDX identifier that registries, scanners, and downstream tooling
+treated as foreign.
+
+== What PMPL represented
+
+The Palimpsest framing carried three commitments that survive intact
+under MPL-2.0:
+
+. *Multi-author authorship as the default reading.* "Palimpsest"
+  named the working assumption that a meaningful body of code is
+  *layered*: contributions overwrite, gloss, and re-purpose
+  predecessors, and the licence regime should reflect that no single
+  author owns the latest layer cleanly. MPL-2.0's file-level
+  copyleft realises exactly this: each file is its own unit, and the
+  layering is visible in the file's history.
+. *Source availability as a discipline, not a strategy.* PMPL was
+  written to make source release the *default* rather than an
+  opt-in. MPL-2.0's "any covered file you distribute, you make the
+  source available for" clause is the operative version of the same
+  commitment.
+. *Narrative coherence over registry convenience.* PMPL's text spent
+  prose on the *why* of its terms; MPL-2.0 spends none. This
+  document is where the *why* now lives, divorced from the legal
+  text it used to be attached to.
+
+== What we no longer claim
+
+. *That PMPL is a distinct licence at registries.* It never was at
+  any standard SPDX registry. crates.io, npm, Hackage, Debian's
+  copyright scanners and similar all treated `PMPL-1.0-or-later` as
+  foreign and required an OSI-recognised fallback (which is
+  precisely MPL-2.0). Carrying both identifiers was friction
+  without legal effect.
+. *That there is a separate Palimpsest copyleft regime.* There
+  isn't. The legal regime is MPL-2.0; the working discipline that
+  PMPL named is documented here.
+. *That `palimpsest-license` is a co-licensing dependency.* It is
+  reference-only documentation of the prior framing. Downstream
+  consumers do not need to read it.
+
+== Header convention going forward
+
+Source files carry exactly:
+
+[source]
+----
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+----
+
+No `PMPL-1.0-or-later`, no compound `MPL-2.0 OR …` clauses, no
+inline comment explaining "MPL-2.0 is the legal fallback for PMPL".
+The header is the legal statement; this document is the narrative.
+Authoring new files: use the two lines above verbatim (substitute
+copyright holder as appropriate); do not invent overlays.
+
+== History
+
+* *Prior to 2026-05-20*: `PMPL-1.0-or-later` was the stated SPDX
+  identifier across this and ~69 other repositories in the estate.
+  MPL-2.0 was named as the automatic legal fallback (lawyer-confirmed).
+* *2026-05-20 (owner direction)*: collapse the SPDX identifier to
+  MPL-2.0; preserve the PMPL framing as this narrative document.
+* *Drift note*: SPDX headers across the wider estate may still carry
+  `PMPL-1.0-or-later` and will be migrated in their own time. The
+  legal effect is unchanged (MPL-2.0 is the operative licence in
+  either case); the stated identifier is the only thing that
+  differs. Migration is owner-paced and manual.
+
+== References
+
+* `LICENSE` (MPL-2.0 full text, this repository).
+* `LICENSE-docs` (CC-BY-4.0 full text for documentation, this
+  repository).
+* Mozilla Public License v2.0 — https://www.mozilla.org/en-US/MPL/2.0/
+* SPDX licence list — https://spdx.org/licenses/MPL-2.0.html

docs/echidna-design-search-2026-04-28.adoc

@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = Echidna design-search findings — Phase 1.3 + unbudgeted wf-<ᵇʳᶠ_
 :date: 2026-04-28
 :toc:

docs/echo-types/MAP.adoc

@@ -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>
 = echo-types: Master Map
 :toc: macro

docs/echo-types/echo-kernel-note.adoc

@@ -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>
 = echo-types: kernel vs derived (one-page note)
 :toc: macro