Add integration bridge, next-question backlog, and robust CI stdlib resolution

Author: hyperpolymath

.github/workflows/agda.yml

@@ -18,17 +18,21 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y agda agda-stdlib
 
-      - name: Configure Agda standard library
+      - name: Locate Agda standard library
+        id: stdlib
         run: |
-          STDLIB_LIB="$(find /usr/share -name 'standard-library.agda-lib' | head -n 1)"
-          if [ -z "$STDLIB_LIB" ]; then
-            echo "Could not locate standard-library.agda-lib"
+          STDLIB_DIR="$(
+            find /usr/share /usr/lib -type f -path '*/Data/Nat/Base.agda' 2>/dev/null \
+            | head -n 1 \
+            | sed 's#/Data/Nat/Base.agda##'
+          )"
+
+          if [ -z "$STDLIB_DIR" ]; then
+            echo "Could not locate Agda standard library directory"
             exit 1
           fi
 
-          mkdir -p "$HOME/.agda"
-          printf '%s\n' "$STDLIB_LIB" > "$HOME/.agda/libraries"
-          printf '%s\n' "standard-library" > "$HOME/.agda/defaults"
+          echo "stdlib_dir=$STDLIB_DIR" >> "$GITHUB_OUTPUT"
 
       - name: Typecheck full suite
-        run: agda -i proofs/agda proofs/agda/All.agda
+        run: agda -i proofs/agda -i "${{ steps.stdlib.outputs.stdlib_dir }}" proofs/agda/All.agda

docs/next-questions.adoc

@@ -0,0 +1,104 @@
+= Next Questions
+
+Date: 2026-04-18
+
+This file records the highest-value open problems after the current
+echo/choreo/epistemic/linear/graded/tropical integration pass.
+
+== Q1. Unified Dependent Linear + Choreographic + Epistemic Calculus
+
+Why it matters:
+
+* This is the main synthesis target for "structured loss with controlled use."
+
+Current gap:
+
+* We have bridges between parts, but not one single typed calculus enforcing all
+  constraints simultaneously.
+
+Needed:
+
+* A core syntax/judgment layer with usage discipline + role projection +
+  knowledge operators, and preservation/progress-style metatheory.
+
+Difficulty:
+
+* Extremely hard.
+
+== Q2. Quotient/Cubical Treatment of Indistinguishability
+
+Why it matters:
+
+* Current indistinguishability is set-level/propositional.
+* Rich observational equivalence classes need better identity handling.
+
+Current gap:
+
+* No cubical/quotient formalization of observational collapse classes.
+
+Needed:
+
+* A quotient-aware or cubical extension with proofs that echo constructions
+  commute with equivalence-class semantics.
+
+Difficulty:
+
+* Very hard.
+
+== Q3. Probabilistic Epistemic Echoes
+
+Why it matters:
+
+* Many realistic systems are stochastic; evidence is weighted, not binary.
+
+Current gap:
+
+* No probability/distribution layer over echoes.
+
+Needed:
+
+* Distribution-valued observation semantics and posterior-style residue objects,
+  plus stability/transport theorems.
+
+Difficulty:
+
+* Very hard.
+
+== Q4. Tropical Optimization Semantics Beyond Toy Candidate Sets
+
+Why it matters:
+
+* Current tropical development is finite/toy-level.
+
+Current gap:
+
+* No general optimization framework (argmin sets, ties, compositionality across
+  larger structures).
+
+Needed:
+
+* Scalable tropical witness/certificate framework with composition laws and
+  integration with graded degradation.
+
+Difficulty:
+
+* Hard.
+
+== Q5. Automation and Regression Guardrails
+
+Why it matters:
+
+* Scope has grown quickly; regressions become expensive.
+
+Current gap:
+
+* CI gate existed but failed due environment assumptions.
+
+Needed:
+
+* Robust CI with full-suite typecheck, plus optional lightweight proof-smoke
+  checks for future PRs.
+
+Difficulty:
+
+* Moderate.

proofs/agda/All.agda

@@ -12,6 +12,7 @@ open import EchoEpistemic
 open import EchoLinear
 open import EchoGraded
 open import EchoTropical
+open import EchoIntegration
 
 open import EchoIndexed
 open import EchoEpistemicResidue

proofs/agda/EchoIntegration.agda

@@ -0,0 +1,48 @@
+{-# OPTIONS --safe --without-K #-}
+
+module EchoIntegration where
+
+open import EchoChoreo
+open import EchoEpistemic
+open import EchoGraded
+open import EchoCharacteristic using (echo-true; echo-false; echo-true≢echo-false)
+open import EchoResidue using (no-section-collapse-to-residue)
+
+open import Data.Bool.Base using (Bool)
+open import Data.Product.Base using (Σ; _×_; _,_; proj₁)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+open import Relation.Nullary using (¬_)
+
+-- Choreographic observation-preserving steps preserve any epistemic predicate
+-- that is stable under the hidden-state update.
+knowledge-preserved-under-choreo :
+  ∀ {y : Bool} {P : Global → Set} →
+  (∀ g → P g → P (scramble-server g)) →
+  Knows Client P y →
+  ∀ e → P (proj₁ (client-stability e))
+knowledge-preserved-under-choreo = knowledge-along-client-stability
+
+-- Controlled degradation in graded echoes:
+-- distinct keep-grade witnesses become identified at residue grade.
+distinct-at-keep : echo-true ≢ echo-false
+distinct-at-keep = echo-true≢echo-false
+
+merged-at-residue :
+  degrade keep≤residue echo-true ≡ degrade keep≤residue echo-false
+merged-at-residue = refl
+
+no-recovery-after-residue-degrade :
+  ¬ (Σ (GEcho residue → GEcho keep)
+       (λ raise → ∀ e → raise (degrade keep≤residue e) ≡ e))
+no-recovery-after-residue-degrade = no-section-collapse-to-residue
+
+-- Integration witness: choreography can preserve knowledge while graded
+-- degradation still loses discriminating power in a controlled way.
+knowledge-and-controlled-degradation :
+  ∀ {y : Bool} {P : Global → Set} →
+  (∀ g → P g → P (scramble-server g)) →
+  Knows Client P y →
+  (∀ e → P (proj₁ (client-stability e)))
+  × (degrade keep≤residue echo-true ≡ degrade keep≤residue echo-false)
+knowledge-and-controlled-degradation inv k =
+  knowledge-preserved-under-choreo inv k , merged-at-residue

readme.adoc

@@ -35,6 +35,7 @@ Current formal foundation is in:
 * `proofs/agda/EchoLinear.agda`
 * `proofs/agda/EchoGraded.agda`
 * `proofs/agda/EchoTropical.agda`
+* `proofs/agda/EchoIntegration.agda`
 
 with constructive proofs (safe Agda, no postulates):
 
@@ -58,6 +59,7 @@ Scope-broadening stages now include:
 * affine/linear bridge (strict weakening from full echoes to residues)
 * graded bridge (grade order and compositional degradation law)
 * tropical bridge (argmin-style witness residues under tropical collapse)
+* integration bridge (knowledge preservation under choreography plus controlled graded degradation)
 
 == What Echo Types Are For
 
@@ -111,3 +113,7 @@ agda -i proofs/agda proofs/agda/All.agda
 Proof milestones and decision gates are in:
 
 * `roadmap.adoc`
+
+Open hard questions are tracked in:
+
+* `docs/next-questions.adoc`

roadmap.adoc

@@ -292,6 +292,21 @@ cd proofs/agda
 for f in *.agda; do agda -i . "$f"; done
 ----
 
+M12. Cross-bridge integration:
+
+* add `proofs/agda/EchoIntegration.agda`
+* prove a theorem combining choreographic knowledge preservation with graded
+  controlled degradation behavior
+
+Status: DONE (2026-04-18)
+
+Delivered in `proofs/agda/EchoIntegration.agda`:
+
+* `knowledge-preserved-under-choreo`
+* `merged-at-residue`
+* `no-recovery-after-residue-degrade`
+* `knowledge-and-controlled-degradation`
+
 == Operating Rules
 
 * No postulates unless explicitly isolated and justified.