Reconcile Echo identity evidence and record Agda checks

.github/workflows/agda.yml

@@ -45,6 +45,12 @@ jobs:
       - name: Kernel funext-free certificate + classification guard
         run: sh scripts/kernel-guard.sh
 
+      - name: Check experimental aggregate covers its direct modules
+        run: bash scripts/check-experimental-aggregate.sh
+
+      - name: Check Agda invocation profiles (static)
+        run: python3 scripts/check-agda-invocations.py
+
       - name: Install Agda and standard library
         run: |
           sudo apt-get update
@@ -73,6 +79,7 @@ jobs:
         run: |
           STDLIB_DIR="$HOME/agda-stdlib"
           git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR"
+          test "$(git -C "$STDLIB_DIR" rev-parse HEAD)" = 8326c7475af1fa456ca04a0203c168d5d7ff842b
           echo "stdlib_dir=$STDLIB_DIR" >> "$GITHUB_OUTPUT"
 
       - name: Fetch absolute-zero library (PINNED)
@@ -138,24 +145,24 @@ jobs:
             agdai-${{ runner.os }}-stdlib2.3-
 
       - name: Typecheck full suite
-        run: agda -i proofs/agda proofs/agda/All.agda
+        run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda
 
       - name: Smoke-check headline theorems
-        run: agda -i proofs/agda proofs/agda/Smoke.agda
+        run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Smoke.agda
 
       - name: Typecheck characteristic lane (Gate #2 audit modules)
-        run: agda -i proofs/agda proofs/agda/characteristic/All.agda
+        run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/characteristic/All.agda
 
       - name: Typecheck examples lane (Gate #3 canonical examples)
-        run: agda -i proofs/agda proofs/agda/examples/All.agda
+        run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/examples/All.agda
 
       # Cubical lane: the (epi, mono) truncation discharge. A --cubical
       # --safe island (zero postulates) that CONSTRUCTS ∥_∥ as a HIT —
       # it cannot be imported by the --safe --without-K All.agda, so it
       # is typechecked directly here. Its --without-K-profile shadow is
       # EchoImageFactorizationPropPostulated (proof-debt (a)/(c)).
       - name: Typecheck cubical lane (epi/mono truncation discharge)
-        run: agda -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda
+        run: agda --safe --cubical -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda
 
       # Experimental lane: the echo-additive grade tree, typechecked through
       # its own aggregate root (--safe --without-K from the pragmas);
@@ -165,7 +172,11 @@ jobs:
       # that vendor Grade.agda (choreographic-types) learn here, not
       # in their own CI, when an edit breaks it.
       - name: Typecheck experimental echo-additive lane (standalone, not in the closure)
-        run: agda -i proofs/agda proofs/agda/experimental/echo-additive/All.agda
+        run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/experimental/echo-additive/All.agda
+
+      # A separate entrypoint, not evidence about the shipped closure.
+      - name: Typecheck bit-narrowing exhibit
+        run: agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/NarrowingSmoke.agda
 
   cold-check:
     # Belt-and-braces: NO interface cache, --ignore-interfaces cold
@@ -195,9 +206,11 @@ jobs:
         run: |
           STDLIB_DIR="$HOME/agda-stdlib"
           git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR"
+          test "$(git -C "$STDLIB_DIR" rev-parse HEAD)" = 8326c7475af1fa456ca04a0203c168d5d7ff842b
           ABSZ_DIR="$HOME/absolute-zero"
           git clone https://github.com/hyperpolymath/absolute-zero.git "$ABSZ_DIR"
           git -C "$ABSZ_DIR" checkout --quiet "$ABSZ_REF"
+          test "$(git -C "$ABSZ_DIR" rev-parse HEAD)" = "$ABSZ_REF"
           mkdir -p "$HOME/.agda"
           printf 'name: standard-library\ninclude: %s/src\n' "$STDLIB_DIR" > "$RUNNER_TEMP/sl.agda-lib"
           printf 'name: absolute-zero\ninclude: %s/proofs/agda\n' "$ABSZ_DIR" > "$RUNNER_TEMP/az.agda-lib"
@@ -206,9 +219,10 @@ jobs:
 
       - name: Cold typecheck (--ignore-interfaces, no cache)
         run: |
-          agda --ignore-interfaces -i proofs/agda proofs/agda/All.agda
-          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
-          agda --ignore-interfaces -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda
-          agda --ignore-interfaces -i proofs/agda proofs/agda/experimental/echo-additive/All.agda
+          agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda
+          agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Smoke.agda
+          agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/characteristic/All.agda
+          agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/examples/All.agda
+          agda --ignore-interfaces --safe --cubical -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda
+          agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/experimental/echo-additive/All.agda
+          agda --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/NarrowingSmoke.agda

AFFIRMATION.adoc

@@ -237,6 +237,9 @@ we name them as three.
 * *The retracted "graded comonad" reading stands retracted* (R-2026-05-18):
   echo-types is a loss-graded _reindexing modality_ (thin-poset action); the
   experimental `echo-additive/` tree is not wired into the shipped closure.
+  The current Agda workflow invokes its separate aggregate as a step in
+  both jobs, not as an independently named job; see `PROOF-STATUS.adoc`
+  for the coverage and verification limits.
 
 [#reproduce]
 == Reproduce it yourself

CLAUDE.md

@@ -1,14 +1,25 @@
 <!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+# Proof policy
+
+The normative estate policy is
+https://github.com/hyperpolymath/standards/blob/main/3-practice/PROOF-POLICY.adoc.
+Its default Agda theory profile is `--safe --without-K --cubical-compatible`;
+full Cubical proofs require a separate reviewed profile. Record toolchain,
+assumptions, results and exact source revisions; historical checks do not
+prove the new profile. Mathesis grades are theorem- and receipt-specific.
+
 # Ecosystem context
 
 This repo (echo-types) is one node in the hyperpolymath / PanLL ecosystem.
 Adjacent projects, in one line each, for session bootstrapping:
 
 - echo-types — constructive Agda formalization of fiber-based structured
   loss ("echo types"); `Echo f y := Σ (x : A) , (f x ≡ y)`. Gated
-  identity-claim development; `--safe --without-K` throughout. The
-  ordinal-notation / Buchholz lane moved out on 2026-10-20 (see below).
+  identity-claim development; ordinary proof roots use `--safe --without-K
+  --cubical-compatible`. The full-cubical island is a separate profile;
+  the postulated shadow remains quarantined. The ordinal-notation /
+  Buchholz lane moved out on 2026-10-20 (see below).
   https://github.com/hyperpolymath/echo-types
 - PanLL — three-pane cognitive-relief HTI; Ambient/Symbolic/Neural/World panes.
   https://github.com/hyperpolymath/panll

Justfile

@@ -5,13 +5,13 @@
 # Build all echo type modules
 build-echo:
 	@echo "Building echo type modules..."
-	agda -i proofs/agda proofs/agda/All.agda
+	agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda
 	@echo "✅ All echo modules built successfully"
 
 # Build stability tests
 build-tests:
 	@echo "Building stability tests..."
-	agda -i proofs/agda proofs/agda/Echo/Bridges/EchoStabilityTests.agda
+	agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoStabilityTests.agda
 	@echo "✅ Stability tests built successfully"
 
 # Run comprehensive build
@@ -25,31 +25,31 @@ build-all:
 
 test-core:
 	@echo "Testing core echo type properties..."
-	agda -i proofs/agda proofs/agda/Echo/Core.agda
+	agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Echo.agda
 	@echo "✅ Core tests passed"
 
 # Test CNO bridge
 test-cno:
 	@echo "Testing CNO bridge..."
-	agda -i proofs/agda proofs/agda/Echo/Bridges/EchoCNOBridge.agda
+	agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoCNOBridge.agda
 	@echo "✅ CNO bridge tests passed"
 
 # Test thermodynamic bridge
 test-thermo:
 	@echo "Testing thermodynamic bridge..."
-	agda -i proofs/agda proofs/agda/Echo/Bridges/EchoThermodynamics.agda
+	agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoThermodynamics.agda
 	@echo "✅ Thermodynamic tests passed"
 
 # Test categorical bridge
 test-cat:
 	@echo "Testing categorical bridge..."
-	agda -i proofs/agda proofs/agda/Echo/Bridges/EchoCategorical.agda
+	agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoCategorical.agda
 	@echo "✅ Categorical tests passed"
 
 # Test stability suite
 test-stability:
 	@echo "Testing stability suite..."
-	agda -i proofs/agda proofs/agda/Echo/Bridges/EchoStabilityTests.agda
+	agda --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/EchoStabilityTests.agda
 	@echo "✅ Stability tests passed"
 
 # Run all tests