fix(proofs): establish semantic evidence and require continuity checks

.github/workflows/actions.lock

@@ -0,0 +1,28 @@
+# This file is machine-generated by `gh actions-lock`.
+# Do not edit by hand; run `gh actions-lock` to update.
+# Docs: https://gh.io/actions-lockfile
+version: 'v0.0.2'
+workflows:
+    '.github/workflows/agda.yml':
+        - 'actions/checkout@v6.0.3'
+    '.github/workflows/codeql.yml':
+        - 'actions/checkout@v6.0.3'
+        - 'github/codeql-action@v4.36.2'
+    '.github/workflows/push-email-notify.yml':
+        - 'hyperpolymath/smtp-notify-action@v0.2.0'
+dependencies:
+    'actions/checkout@v6.0.3':
+        ref: 'v6.0.3'
+        commit: 'sha1-df4cb1c069e1874edd31b4311f1884172cec0e10'
+        owner_id: 44036562
+        repo_id: 197814629
+    'github/codeql-action@v4.36.2':
+        ref: 'v4.36.2'
+        commit: 'sha1-8aad20d150bbac5944a9f9d289da16a4b0d87c1e'
+        owner_id: 9919
+        repo_id: 259445878
+    'hyperpolymath/smtp-notify-action@v0.2.0':
+        ref: 'v0.2.0'
+        commit: 'sha1-ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7'
+        owner_id: 6759885
+        repo_id: 1352485172

.github/workflows/agda.yml

@@ -1,54 +1,72 @@
+# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-# Agda — typecheck the epistemic-types proof suite.
-#
-# The repo is deliberately stdlib-free (built with --no-libraries; only
-# Agda.Primitive / Agda.Builtin.*), so no standard-library setup is needed
-# and the apt-packaged Agda suffices. The canonical aggregator is
-# src/EpistemicTypes/All.agda, which transitively imports every module and
-# carries {-# OPTIONS --safe --without-K #-} per module. This is the proof
-# verification the repo previously lacked entirely.
-name: Agda
+# This workflow is managed by gh actions-lock.
+
+name: Proof Safety
 
 on:
-  # Direct pushes only on integration branches; PRs cover feature branches.
   push:
-    branches: [main, master]
+    branches: [main]
   pull_request:
+  merge_group:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+env:
+  LANG: C.UTF-8
+  LC_ALL: C.UTF-8
 
-# Estate guardrail: cancel superseded runs. Safe — read-only typecheck,
-# no publish or mutation.
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
-permissions:
-  contents: read
-
 jobs:
-  check:
-    runs-on: ubuntu-latest
-    timeout-minutes: 20
+  core:
+    name: Proof core and rejection controls
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    container: debian:13-slim@sha256:d7e12182ce18b85b93007c1dedf31f2d29e01ccf3182cc4017c709b6259bc132
     steps:
-      - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
-
-      - name: Install Agda
+      - name: Install authenticated Debian toolchain packages
         run: |
-          sudo apt-get update
-          sudo apt-get install -y agda
-
-      - name: Toolchain provenance
-        run: agda --version | head -n1
-
-      - name: Typecheck canonical target (stdlib-free)
+          apt-get update
+          apt-get install --no-install-recommends -y ca-certificates git ripgrep agda-bin=2.6.4.3-1+b2
+      - uses: actions/checkout@v6.0.3
+        with:
+          persist-credentials: false
+      - name: Verify toolchain and proof constructions
         run: |
-          set -e
-          agda --no-libraries -i src src/EpistemicTypes/All.agda
-          echo "epistemic-types: src/EpistemicTypes/All.agda typechecks (exit 0)."
+          test "$(agda --version)" = 'Agda version 2.6.4.3'
+          bash tests/check-proofs.sh
+          bash tests/check-rejections.sh
 
-      - name: Re-check with warnings promoted to errors (no unsolved metas)
+  echo:
+    name: Canonical Echo correspondence
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    container: debian:13-slim@sha256:d7e12182ce18b85b93007c1dedf31f2d29e01ccf3182cc4017c709b6259bc132
+    steps:
+      - name: Install authenticated Debian toolchain packages
+        run: |
+          apt-get update
+          apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4
+      - uses: actions/checkout@v6.0.3
+        with:
+          persist-credentials: false
+      - name: Checkout reviewed canonical Echo source
+        uses: actions/checkout@v6.0.3
+        with:
+          repository: hyperpolymath/echo-types
+          ref: 46cd1a32d4dcf1020f01dd1aab41f816742da10e
+          path: .ci-deps/echo-types
+          persist-credentials: false
+      - name: Prove representation round trips and lowering agreement
         run: |
-          set -e
-          agda --no-libraries -i src -W error src/EpistemicTypes/All.agda
-          echo "epistemic-types: clean under -W error (no unsolved metas/constraints/termination issues)."
+          test "$(agda --version)" = 'Agda version 2.6.4.3'
+          agda --no-libraries --safe --without-K --double-check --ignore-interfaces \
+            -W error -W noUnsupportedIndexedMatch -i src -i tests/integration \
+            -i .ci-deps/echo-types/proofs/agda -i /usr/share/agda-stdlib/src \
+            tests/integration/CanonicalEcho.agda

.github/workflows/codeql.yml

@@ -1,3 +1,4 @@
+# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 name: CodeQL Security Analysis
@@ -41,15 +42,15 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+        uses: actions/checkout@v6.0.3
 
       - name: Initialize CodeQL
-        uses: github/codeql-action/init@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3
+        uses: github/codeql-action/init@v4.36.2
         with:
           languages: ${{ matrix.language }}
           build-mode: ${{ matrix.build-mode }}
 
       - name: Perform CodeQL Analysis
-        uses: github/codeql-action/analyze@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3
+        uses: github/codeql-action/analyze@v4.36.2
         with:
           category: "/language:${{ matrix.language }}"

.github/workflows/governance.yml

@@ -1,3 +1,4 @@
+# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 name: Governance
 
@@ -9,8 +10,9 @@ on:
   workflow_dispatch:
 
 permissions:
+  actions: read
   contents: read
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@81dbf2dd854b1444fd6236fa2352474383b2c2b9
+    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@a26cc7479b14cdf70433919bfc228625f1c5c6f2

.github/workflows/label-triage.yml

@@ -1,3 +1,4 @@
+# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 name: Label Triage
 

.github/workflows/labels.yml

@@ -1,3 +1,4 @@
+# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 name: Labels
 

.github/workflows/push-email-notify.yml

@@ -1,3 +1,4 @@
+# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 # Dormant push-email notification. ARMED by setting the repo variable
 # PUSH_EMAIL_ENABLED=true (the single on/off switch). Addresses are pre-filled;
@@ -39,7 +40,7 @@ jobs:
     timeout-minutes: 5
     steps:
       - name: Send push notification email
-        uses: hyperpolymath/smtp-notify-action@ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7 # v0.2.0
+        uses: hyperpolymath/smtp-notify-action@v0.2.0
         with:
           server_address: ${{ secrets.SMTP_HOST }}
           server_port: ${{ secrets.SMTP_PORT }}

.github/workflows/secret-scanner.yml

@@ -1,3 +1,4 @@
+# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 # Calls the estate's shared secret scanner (gitleaks + rust-secrets +
 # shell-secrets). Added because this repository had NO leak scanning at all.

.gitignore

@@ -2,3 +2,6 @@
 _build/
 *~
 .DS_Store
+
+# Ephemeral canonical-integration checkout
+/.ci-deps/

.machine_readable/6a2/0-AI-MANIFEST.a2ml → .machine_readable/descriptiles/0-AI-MANIFEST.a2ml

@@ -1,4 +1,4 @@
-# 0-AI-MANIFEST.a2ml — AI-assistant context for the 6a2 directory
+# 0-AI-MANIFEST.a2ml — AI-assistant context for the descriptiles directory
 # epistemic-types: directory manifest, modeling rules, and the typecheck command.
 
 [manifest]
@@ -22,20 +22,20 @@ mathematical_honesty = "Do not postulate laws silently. No Agda postulates; laws
 factivity = "Separate factive knowledge from non-factive belief."
 warrants = "Use explicit warrant objects where possible."
 scope = "Keep modules small and type-check frequently; keep to a single-tool Agda library checked by 'just check'."
-echo_distinction = "Echo-types are min-plus-graded loss/residue modalities; epistemic types are standpoint/warrant/access modalities."
-no_collapse = "Do not collapse Echo r A and E κ A. Their composition is meaningful, but they are not the same modality."
+echo_distinction = "Echo values have explicit retention certificates; resource bounds are separate; epistemic types are standpoint/warrant/access modalities."
+no_collapse = "Do not collapse Echo C y and E κ A. Their composition is meaningful, but they are not the same modality."
 
 [typecheck]
-command = "agda --no-libraries -i src src/EpistemicTypes/All.agda"
+command = "bash tests/check-proofs.sh && bash tests/check-rejections.sh"
 just-target = "just check"
-agda-version = "2.8.0"
+agda-version = "2.6.4.3"
 
 [canonical-locations]
-# The 6a2 directory is authoritative for this repo's machine-readable metadata.
+# The descriptiles directory is authoritative for this repo's machine-readable metadata.
 # Present in this directory (right-sized for a small formal-methods prototype):
-present = [ "0-AI-MANIFEST.a2ml", "STATE.a2ml", "README.adoc" ]
+present = ["0-AI-MANIFEST.a2ml", "AGENTIC.a2ml", "ECOSYSTEM.a2ml", "META.a2ml", "NEUROSYM.a2ml", "PLAYBOOK.a2ml", "README.adoc", "STATE.a2ml"]
 
 [invariants]
 single-source-of-truth = "This directory is authoritative; no duplicate metadata in the root directory."
 no-stale-metadata = true
-ci = "Not enabled (see AUDIT.adoc)."
+ci = "Proof and security workflows configured; see docs/ci-safety.adoc."

.machine_readable/6a2/AGENTIC.a2ml → .machine_readable/descriptiles/AGENTIC.a2ml

@@ -11,8 +11,8 @@ last-updated = "2026-06-15"
 
 [agent-permissions]
 can-edit-source = true        # Agda modules under src/EpistemicTypes/
-can-edit-docs = true          # readme.adoc, explainme.adoc, AsciiDoc docs
-can-edit-machine-readable = true  # .machine_readable/ (6a2, proof-transport)
+can-edit-docs = true          # README.adoc, explainme.adoc, AsciiDoc docs
+can-edit-machine-readable = true  # .machine_readable/ (descriptiles, proof-transport)
 can-edit-build = true         # Justfile, epistemic-types.agda-lib, .gitignore
 can-create-files = true
 can-edit-license = false      # LICENSE / SPDX are owner-manual — agents MUST NOT touch
@@ -29,20 +29,20 @@ can-add-spdx-headers = false  # repo is intentionally SPDX-free; keep it consist
 #   is a plain indexed endofunctor (map only). Do NOT add a generic return,
 #   reflect, join, or extract that is not justified by an explicit field or proof.
 #   Laws appear as fields when not derivable; they are never assumed silently.
-# - Never collapse Echo r A (min-plus graded loss/residue) into E κ A. Their
+# - Never collapse Echo C y (certified residue and separately measured bounds) into E κ A. Their
 #   composition is meaningful; they are not the same modality.
 # - Never break the ProofTransport no-smuggling discipline: verify upgrades
 #   Data -> Proof only with the receiver's OWN checker + evidence; transmit
 #   downgrades a sender's Proof to a receiver's Receipt; receipt-only never
 #   certifies. Do not weaken proofNeedsChecker.
 # Repository hygiene:
 # - Never place state files in the repository root. Machine-readable state lives
-#   under .machine_readable/ (6a2, proof-transport).
+#   under .machine_readable/ (descriptiles, proof-transport).
 # - Never edit LICENSE or add SPDX-License-Identifier / copyright headers.
 #   Licensing (classified MPL-2.0 as the owner's sole repo) is owner-manual only.
 # - Never commit secrets or credentials.
-# - Keep docs in AsciiDoc; do not rename or duplicate readme.adoc / explainme.adoc.
-# - Do not add CI / GitHub Actions workflows or badges (not enabled; see AUDIT.adoc).
+# - Keep docs in AsciiDoc; do not rename or duplicate README.adoc / explainme.adoc.
+# - Maintain the owner-authorized proof and security CI gates; never bypass failing checks.
 
 [maintenance-integrity]
 fail-closed = true
@@ -55,8 +55,8 @@ release-claim-requires-hard-pass = true
 [verification]
 # The single source of truth for "does it hold".
 command = "just check"
-underlying = "agda --no-libraries -i src src/EpistemicTypes/All.agda"
-agda-version = "2.8.0"
+underlying = "bash tests/check-proofs.sh && bash tests/check-rejections.sh"
+agda-version = "2.6.4.3"
 entrypoint = "src/EpistemicTypes/All.agda"
 expected = "type-checks clean, no postulates, no warnings"
 

.machine_readable/6a2/ECOSYSTEM.a2ml → .machine_readable/descriptiles/ECOSYSTEM.a2ml

@@ -12,13 +12,13 @@ type = "formal-methods-library"
 purpose = "A small, deliberately honest Agda formalization of standpoint-indexed modal / epistemic / echo-like type formers. Favours mathematical honesty over a large API: constructive, no postulates, no standard library."
 
 [stack]
-language = "Agda 2.8.0"
+language = "Agda 2.6.4.3"
 options = "--safe --without-K"
 libraries = "none — built with 'agda --no-libraries' against Agda.Builtin.* and Agda.Primitive only"
 machine-readable = "a2ml + Nickel/k9"
 docs = "AsciiDoc"
 check = "just check  ==  agda --no-libraries -i src src/EpistemicTypes/All.agda"
-notes = "Single-tool Agda library. No JS/TS/Python, no containers, no CI (see AUDIT.adoc)."
+notes = "Single-tool Agda library. The core has no runtime dependencies; CI uses a pinned Debian verification container."
 
 [core]
 form = "E : K -> Set ℓ -> Set ℓ   (E κ A = 'A is epistemically available at standpoint κ')"
@@ -27,7 +27,7 @@ modules = [
   "EpistemicTypes.Base — Modality / LawfulModality / FactiveModality / BeliefModality / ReturnModality",
   "EpistemicTypes.Warrant — Warrant / Epi / SoundWarrant",
   "EpistemicTypes.Access — Preorder + AccessibleModality transport 'increase'",
-  "EpistemicTypes.EchoBridge — min-plus graded loss/residue 'Echo r A', kept distinct from E κ A",
+  "EpistemicTypes.EchoBridge — certified residue and separately measured bounds 'Echo C y', kept distinct from E κ A",
   "EpistemicTypes.SurrealBridge — SurrealAccess carrier + GradedSurrealModality + daySurrealAccess finite birthday tower",
   "EpistemicTypes.Examples",
   "EpistemicTypes.ProofTransport — standpoint-indexed proof transport across trust boundaries",
@@ -43,8 +43,8 @@ no-smuggling = "proofNeedsChecker: no checker-free Proof -> Proof transport is e
 
 [related-projects]
 projects = [
-  { name = "echo-types", relationship = "sibling-formalism", notes = "Agda loss-with-residue (min-plus graded) formalism. EpistemicTypes.EchoBridge's 'Echo r A' composes with it; kept deliberately distinct from the epistemic E κ A modality (no collapse)." },
+  { name = "echo-types", relationship = "sibling-formalism", notes = "Agda loss-with-residue (min-plus graded) formalism. EpistemicTypes.EchoBridge's 'Echo C y' composes with it; kept deliberately distinct from the epistemic E κ A modality (no collapse)." },
   { name = "ephapax", relationship = "sibling-formal-language", notes = "Sibling formal language; its four-layer redesign carries echo obligations. Echo / standpoint vocabulary is shared at the conceptual level, not via a code dependency." },
-  { name = "standards", relationship = "estate-foundation", notes = "Estate RSR / standards repo plus k9-svc and a2ml tooling. Supplies the 6a2 layout and the contractile / k9 rendering conventions this repo's .machine_readable mirrors." },
+  { name = "standards", relationship = "estate-foundation", notes = "Estate RSR / standards repo plus k9-svc and a2ml tooling. Supplies the descriptiles layout and the contractile / k9 rendering conventions this repo's .machine_readable mirrors." },
   { name = "a2ml + k9", relationship = "rendering-target", notes = "Machine-readable a2ml + Nickel/k9 contractile tooling. The engineering rendering target for ProofTransport: the standpoint-indexed proof-transport core is rendered to a2ml/k9 under .machine_readable/proof-transport/." }
 ]

.machine_readable/6a2/META.a2ml → .machine_readable/descriptiles/META.a2ml

@@ -22,7 +22,7 @@ adrs = [
   { id = "ADR-002", title = "Separate FactiveModality from BeliefModality; no generic reflect/return", status = "accepted", date = "2026-06-15" },
   { id = "ADR-003", title = "Compile under --safe --without-K", status = "accepted", date = "2026-06-15" },
   { id = "ADR-004", title = "No Agda standard library; build with agda --no-libraries", status = "accepted", date = "2026-06-15" },
-  { id = "ADR-005", title = "Keep Echo grades distinct from epistemic standpoints", status = "accepted", date = "2026-06-15" },
+  { id = "ADR-005", title = "Keep certified residues and resource bounds distinct from epistemic standpoints", status = "accepted", date = "2026-06-15" },
   { id = "ADR-006", title = "ProofTransport: no smuggling by construction", status = "accepted", date = "2026-06-15" }
 ]
 
@@ -55,10 +55,10 @@ decision = "Build with `agda --no-libraries`, using only `Agda.Builtin.*` and `A
 consequence = "The project is self-contained and reproducible with just an Agda binary, at the cost of re-deriving small primitives in-tree."
 
 [architecture-decisions.ADR-005]
-title = "Keep Echo grades distinct from epistemic standpoints"
+title = "Keep certified residues and resource bounds distinct from epistemic standpoints"
 status = "accepted"
-context = "`EchoBridge` provides a min-plus-graded loss/residue modality `Echo r A`. It is tempting to identify the grade `r` with an epistemic standpoint `κ`, collapsing two different ideas."
-decision = "`Echo r A` (graded loss/residue) and `E κ A` (standpoint-indexed epistemic availability) are kept as separate type formers. Their composition is meaningful and intended, but they are never the same modality."
+context = "Echo C y packages a residue certified by Retention.Cert. Measured resource bounds are separate; the epistemic index κ denotes a standpoint."
+decision = "Preserve the distinction between certified Echo residues, measured bounds, and E κ A. Compose them only with explicit laws."
 consequence = "The echo bridge can be extended without dragging in a full graded comonad, and standpoint reasoning stays independent of loss accounting."
 
 [architecture-decisions.ADR-006]
@@ -72,7 +72,7 @@ consequence = "No-smuggling holds structurally rather than by side-condition. Th
 build-tool = "just"
 build-command = "just check"
 check-command = "agda --no-libraries -i src src/EpistemicTypes/All.agda"
-agda-version = "2.8.0"
+agda-version = "2.6.4.3"
 package-manager = "none (single agda-lib; no external Agda dependencies)"
 ci-platform = "none (billing wall; see AUDIT.adoc)"
 container-runtime = "none"
@@ -82,7 +82,7 @@ posture = "Mathematical honesty over API size. The library is small on purpose:
 base-interface = "`E : K -> Set ℓ -> Set ℓ`, read `E κ A` = 'A is epistemically available at standpoint κ'. The base is a plain indexed endofunctor (map only) — not a monad or comonad — so no return/reflect is assumed for free."
 factivity = "Factive knowledge and non-factive belief are distinct interfaces (FactiveModality vs BeliefModality), preventing belief from being read as knowledge."
 access = "`Access` adds a preorder over standpoints and an `AccessibleModality` whose `increase` transports availability along the preorder."
-echo = "`EchoBridge` supplies a min-plus-graded loss/residue modality `Echo r A`, kept structurally distinct from epistemic availability; the two compose but never collapse (see ADR-005)."
+echo = "`EchoBridge` supplies a min-plus-graded loss/residue modality `Echo C y`, kept structurally distinct from epistemic availability; the two compose but never collapse (see ADR-005)."
 surreal = "`SurrealBridge` offers an abstract `SurrealAccess` carrier with a `GradedSurrealModality` and a finite-birthday tower `daySurrealAccess`, as instances of the abstract access interface rather than a full surreal-number library."
 proof-transport = "`ProofTransport` formalizes standpoint-indexed proof transport across trust boundaries with statuses Data/Code/Claimed/Receipt/Proof/ProofUnder and modes Public/Designated/IssuerMediated/EnvironmentMediated/OpaqueReceipt; no-smuggling is by construction (see ADR-006)."
 modules = "Base, Warrant, Access, EchoBridge, SurrealBridge, Examples, ProofTransport, ProofTransportExample, with All re-exporting the development."