`experimental/echo-additive` (7 modules incl. the `Grade` dioid) is in no CI lane; 'typechecks standalone' is unmeasured on main

[hyperpolymath]

Measured (2026-09-22, main = 9c4b72b)

• 7 .agda files under proofs/agda/experimental/echo-additive/ (Grade, GradedAdjunction, GradedCarrier, GradedCarrierFaithful, GradedComonad, and two more).
• proofs/agda/All.agda has 0 references to the directory; .github/workflows/agda.yml has no step naming it.
• The repo already says so: AFFIRMATION.adoc:239 "experimental echo-additive/ tree is not wired into the shipped closure"; docs/proof-debt.adoc:141 and :156 call it "the orphaned experimental/echo-additive/ track". AFFIRMATION.adoc:177 records that Grade.agda "typechecks standalone".
• Same shape as Preserved: 4 bit-narrowing Agda modules (36d04b5) on preserve/bit-narrowing-agda-2026-09-11, in no CI lane #320 (4 bit-narrowing modules in no CI lane). choreographic-types' README borrows the Grade dioid from this track.

Why it matters

"Typechecks standalone" is a claim about a workstation on a date. A module in no lane can rot silently while a downstream repo cites it as checked.

Acceptance criteria

1. A lane type-checks all 7 modules on every push to main: an experimental job in agda.yml (agda --safe --without-K per module, or a separate Experimental.agda closure), or inclusion in All.agda. It must be a separate check name, so its red never masquerades as the main suite's.
2. Watched-failing → green: grep -c echo-additive proofs/agda/All.agda .github/workflows/agda.yml is 0 today, ≥ 1 after, and the wiring commit's run is green.
3. Mutant: replace one refl in Grade.agda with a hole; the lane goes red and the main Agda check stays green.
4. AFFIRMATION.adoc:239 and docs/proof-debt.adoc:141–156 say the track is gated, or the track is deleted with Preserved: 4 bit-narrowing Agda modules (36d04b5) on preserve/bit-narrowing-agda-2026-09-11, in no CI lane #320's disposition matched.

🤖 Generated with Claude Code