Add headline-theorem smoke gate and graduate next-questions to roadmap

Smoke.agda pins load-bearing names per bridge module via `using` clauses,
wired into All.agda plus a dedicated CI step so silent renames or deletions
fail CI fast even if the rest of the suite still typechecks.

CI hardening: SHA-pin checkout to v6.0.2, add SPDX header, set
workflow-level `permissions: read-all`.

Open synthesis questions (unified linear+choreo+epistemic calculus,
cubical/quotient indistinguishability, probabilistic epistemic echoes,
scalable tropical optimisation) move from `docs/next-questions.adoc`
to a new `Deferred Research Track` section in `roadmap.adoc`. The
next-questions file is deleted.

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

Author: hyperpolymath

.github/workflows/agda.yml

@@ -1,3 +1,6 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)
+
 name: Agda
 
 on:
@@ -6,12 +9,14 @@ on:
       - "**"
   pull_request:
 
+permissions: read-all
+
 jobs:
   check:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
 
       - name: Install Agda and standard library
         run: |
@@ -40,3 +45,6 @@ jobs:
 
       - name: Typecheck full suite
         run: agda -i proofs/agda proofs/agda/All.agda
+
+      - name: Smoke-check headline theorems
+        run: agda -i proofs/agda proofs/agda/Smoke.agda

docs/next-questions.adoc

@@ -19,3 +19,5 @@ open import EchoEpistemicResidue
 open import EchoRelational
 open import EchoCategorical
 open import EchoScope
+
+open import Smoke

proofs/agda/All.agda

@@ -0,0 +1,64 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Headline-theorem manifest. Pins the load-bearing names from each bridge
+-- module via `using` clauses so a silent rename or deletion fails CI fast,
+-- even if the rest of the suite still typechecks.
+
+module Smoke where
+
+open import Echo using (Echo; echo-intro; map-over; map-over-id; map-over-comp; map-square)
+open import EchoCharacteristic using (collapse; echo-true; echo-false; echo-true≢echo-false)
+open import EchoResidue using (EchoR; collapse-to-residue; strict-weakening-collapse; no-section-collapse-to-residue)
+open import EchoExamples using (square9; visible; quot; collapse-residue-identifies)
+
+open import EchoChoreo using
+  ( Role
+  ; Global
+  ; obs
+  ; RoleEcho
+  ; client-non-injective
+  ; server-non-injective
+  ; client-to-server
+  ; client-stability
+  ; client-preimage-class
+  )
+
+open import EchoEpistemic using
+  ( Indist
+  ; Knows
+  ; knowledge-monotone
+  ; not-knows-server-true-at-client-true
+  ; shared-echo-from-indist
+  ; indist-from-two-echoes
+  )
+
+open import EchoLinear using
+  ( Mode
+  ; LEcho
+  ; weaken
+  ; strict-linear-example
+  ; no-section-weaken
+  )
+
+open import EchoGraded using
+  ( Grade
+  ; degrade
+  ; degrade-comp
+  ; ⊔g-assoc
+  )
+
+open import EchoTropical using
+  ( Candidate
+  ; score
+  ; tropical-non-injective
+  ; IsArgmin
+  ; TropEcho
+  ; distinct-candidates-same-visible-distinct-echo
+  )
+
+open import EchoIntegration using
+  ( knowledge-preserved-under-choreo
+  ; merged-at-residue
+  ; no-recovery-after-residue-degrade
+  ; knowledge-and-controlled-degradation
+  )

proofs/agda/Smoke.agda

@@ -307,6 +307,62 @@ Delivered in `proofs/agda/EchoIntegration.agda`:
 * `no-recovery-after-residue-degrade`
 * `knowledge-and-controlled-degradation`
 
+M13. Headline-theorem smoke gate:
+
+* add `proofs/agda/Smoke.agda` pinning load-bearing names per bridge module
+  via `using` clauses
+* wire it into `All.agda` and a dedicated CI step so silent renames or
+  deletions fail CI fast even if the rest of the suite still typechecks
+* harden `.github/workflows/agda.yml`: SHA-pin checkout, add SPDX header,
+  set workflow-level `permissions: read-all`
+
+Status: DONE (2026-04-19)
+
+== Deferred Research Track
+
+These are open synthesis problems graduated from `docs/next-questions.adoc`.
+They are dissertation-scale or require extensions beyond the current
+`--safe --without-K` core, so they sit on the roadmap rather than on the
+near-term backlog. Each entry records the gap, what would close it, and
+why it is parked.
+
+R1. Unified dependent linear + choreographic + epistemic calculus
+
+* Gap: bridges exist pairwise but not as one typed calculus enforcing
+  usage discipline + role projection + knowledge operators simultaneously.
+* Closure: a core syntax/judgment layer with preservation/progress-style
+  metatheory tying the three disciplines together.
+* Difficulty: extremely hard. Parked: this is the main synthesis target;
+  not advanced in single sessions.
+
+R2. Cubical or quotient treatment of indistinguishability
+
+* Gap: indistinguishability is currently set-level/propositional; rich
+  observational equivalence classes need first-class identity handling.
+* Closure: a quotient-aware or cubical extension with proofs that echo
+  constructions commute with equivalence-class semantics.
+* Difficulty: very hard. Parked: requires moving off plain
+  `--safe --without-K` into cubical agda or a heavy quotient layer.
+
+R3. Probabilistic epistemic echoes
+
+* Gap: no probability/distribution layer over echoes; evidence is
+  binary, not weighted.
+* Closure: distribution-valued observation semantics, posterior-style
+  residue objects, plus stability/transport theorems.
+* Difficulty: very hard. Parked: needs a measure/distribution
+  formalisation that the current core deliberately avoids.
+
+R4. Tropical optimization beyond toy candidate sets
+
+* Gap: tropical development is finite/toy-level (3-element `Candidate`
+  set, hand-built `IsArgmin`).
+* Closure: scalable tropical witness/certificate framework with
+  composition laws and integration with graded degradation, generalised
+  over arbitrary finite candidate sets.
+* Difficulty: hard. Smallest-step start: lift `IsArgmin` over an
+  arbitrary `Fin n`-indexed score family; compose with `degrade`.
+
 == Operating Rules
 
 * No postulates unless explicitly isolated and justified.