ci: extend agda typecheck to characteristic + examples lanes (#27)

Adds proofs/agda/characteristic/All.agda as a CI-seam aggregator for the
12 gate-2 characteristic-lane modules (ChoreoInjective,
IntegrationAudit, InteractionTest, ModeGraded, RecipeNonTriviality,
RecipeSpec, RecipeTheorem, RoleGraded, RoleMode, RoleModeGrade,
RoleRole, VisibleConstraintAudit). Mirrors the existing
proofs/agda/examples/All.agda for the gate-3 lane.

Extends .github/workflows/agda.yml with two additional typecheck steps
that run characteristic/All.agda and examples/All.agda. The top-level
proofs/agda/All.agda does not import either lane; without these
aggregators the 12 characteristic modules + the 3 examples modules are
CI orphans (sit in the repo but never typechecked).

This unblocks future set-N work on machines without local Agda:
typecheck verification happens in CI on every push to every branch and
on every PR. New characteristic modules register by adding one import
line to characteristic/All.agda.

Author: hyperpolymath

.github/workflows/agda.yml

@@ -48,3 +48,9 @@ jobs:
 
       - name: Smoke-check headline theorems
         run: agda -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
+
+      - name: Typecheck examples lane (Gate #3 canonical examples)
+        run: agda -i proofs/agda proofs/agda/examples/All.agda

proofs/agda/characteristic/All.agda

@@ -0,0 +1,29 @@
+{-# OPTIONS --safe --without-K #-}
+
+------------------------------------------------------------------------
+-- Aggregator for the Gate #2 characteristic-lane modules.  Compile with:
+--
+--   agda -i proofs/agda proofs/agda/characteristic/All.agda
+--
+-- Forces every characteristic-lane module through the typechecker so CI
+-- can catch breakage. Mirrors `proofs/agda/examples/All.agda` for the
+-- gate-3 lane. The top-level `proofs/agda/All.agda` does not import
+-- these modules; this file is the CI seam for the lane.
+--
+-- New characteristic modules should register here.
+------------------------------------------------------------------------
+
+module characteristic.All where
+
+import characteristic.ChoreoInjective
+import characteristic.IntegrationAudit
+import characteristic.InteractionTest
+import characteristic.ModeGraded
+import characteristic.RecipeNonTriviality
+import characteristic.RecipeSpec
+import characteristic.RecipeTheorem
+import characteristic.RoleGraded
+import characteristic.RoleMode
+import characteristic.RoleModeGrade
+import characteristic.RoleRole
+import characteristic.VisibleConstraintAudit