Merge main into session-2026-05-20/buchholz-budgeted-plus

Resolves conflicts in 4 files (CLAUDE.md, docs/echo-types/roadmap.md,
proofs/agda/All.agda, proofs/agda/Smoke.agda) by integrating main's
Wave-3 axis-8 closure work with this branch's ω-power rank-mono
unblock.

* `CLAUDE.md` — keep both session-arc sections.  Main's "2026-05-20
  daytime (theory closure waves 1+2+3)" stays; this branch's
  "2026-05-20 evening — ω-power rank-mono unblock (read this first)"
  is the new primary handoff.
* `docs/echo-types/roadmap.md` — take main's "Axis 2 + Axis 8 four
  refinements landed" entries (canonical).
* `proofs/agda/All.agda` — drop my stale `EchoExampleSignAnalysis`,
  `EchoExampleTruncation`, `EchoSearchExample` imports.  Those
  files depended on the early thin-slice `EchoCost`/`EchoSearch`
  interfaces; main's PRs #80/#85 replaced those with the abstract-
  algebra `CostAlgebra` shape, breaking the dependents.  Stale
  files left on disk for later triage (delete-or-update is a
  separate slice).
* `proofs/agda/Smoke.agda` — take main's `EchoSearch` /
  `EchoSearchInstance` / `EchoAccess` headline pins (canonical
  shape with `SearchStrategy`, `EchoS`, `Access` 5-grade enum, etc.).
* `flake.nix`, `proofs/agda/EchoAccess.agda`, `EchoCost.agda`,
  `EchoSearch.agda` — take main's versions (PRs #80/#85 canonical).

Build invariant restored: `agda proofs/agda/All.agda` and
`agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`.
No postulates, no escape pragmas.  All Ordinal/Buchholz path-1
work from this session (Slices 1-5 + Items 1-3) intact.

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

Author: hyperpolymath

.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,14 +1,26 @@
-# 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
 
 on:
+  # Direct pushes only on the integration branches. Feature-branch
+  # validation is fully covered by the pull_request trigger below —
+  # gating WIP pushes to no-PR branches with a full multi-minute Agda
+  # build was the dominant self-inflicted load on the shared estate
+  # Actions concurrency pool, and also double-fired (push + PR) on PR
+  # branches. No proof coverage is lost: PRs and post-merge main still
+  # run the full suite.
   push:
-    branches:
-      - "**"
+    branches: [main, master]
   pull_request:
 
+# Estate guardrail: cancel superseded runs so re-pushes / rebased PR
+# updates don't pile up queued full-suite builds. Safe here — this
+# workflow only typechecks (read-only, no publish or mutation).
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions: read-all
 
 jobs:
@@ -18,6 +30,13 @@ jobs:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
 
+      # Fast static gate (no Agda): enforce the EchoKernel funext-free
+      # certificate and that every Echo*.agda is classified in
+      # docs/echo-types/echo-kernel-note.adoc. Fails the run before the
+      # multi-minute typecheck if the kernel cone or the note drifts.
+      - name: Kernel funext-free certificate + classification guard
+        run: sh scripts/kernel-guard.sh
+
       - name: Install Agda and standard library
         run: |
           sudo apt-get update

.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.
 #
@@ -18,6 +18,13 @@ on:
   pull_request:
   workflow_dispatch:
 
+# Estate guardrail: cancel superseded runs so re-pushes / rebased PR
+# updates don't pile up queued runs. Safe — governance is read-only
+# policy linting with no publish or mutation.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

.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
+# 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
+# SPDX-License-Identifier: MPL-2.0
 name: OSSF Scorecard
 on:
   push:
@@ -7,6 +7,13 @@ on:
     - cron: '0 4 * * *'
   workflow_dispatch:
 
+# Estate guardrail: cancel superseded runs so re-pushes don't pile up
+# queued analyses. Safe — Scorecard is read-only supply-chain analysis
+# with no publish or mutation (SARIF upload is idempotent).
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

.gitignore

@@ -1,3 +1,11 @@
 *.agdai
 arghda-core/target/
 .claude/
+.agda/
+
+# direnv / nix local cache
+.direnv/
+
+# editor / tooling backup files
+*.bak
+*~

.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")