ci(agda): install absolute-zero + fix ModeGrade typo so the suite typechecks (#31)

## Summary

Fixes two latent CI breakages so Agda goes green again.

### 1. Install absolute-zero library (`agda.yml`)

`echo-types.agda-lib` declares `depend: standard-library absolute-zero`,
but the workflow only registered `standard-library`. Agda CI has been
red on `main` since `3f654ef` (2026-04-30) added the dep without a
workflow update. Adds a fetch step that shallow-clones
`hyperpolymath/absolute-zero`, then registers it alongside
`standard-library` in `~/.agda/libraries`.

### 2. Fix `ModeGrade` -> `ModeGraded` import typo
(`characteristic/RecipeNonTriviality.agda`)

`RecipeNonTriviality.agda` imports `characteristic.ModeGrade` (no `d`)
which doesn't exist; the actual file is `characteristic.ModeGraded`.
Renames cleanly: `MGEcho` -> `ModeGEcho`, `applyGrade` -> `applyGradeM`.
The body uses (`modegrade-cell-action` and friends) reduce
definitionally as before because `applyMode/applyGrade` at `(linear,
keep)` are identity in the existing `ModeGraded.agda`.

This bug was latent since the characteristic lane was added in #27
(2026-04-29), masked by the absolute-zero env break that (1) fixes.

## Local verification

```
agda -i proofs/agda proofs/agda/All.agda                       # exit 0
agda -i proofs/agda proofs/agda/Smoke.agda                     # exit 0
agda -i proofs/agda proofs/agda/characteristic/All.agda        # exit 0
agda -i proofs/agda proofs/agda/examples/All.agda              # exit 0
```

All under `--safe --without-K`. No postulates introduced.

## Effect on other PRs

After merge, #28, #29, #30 should re-run with the env in place. They may
need rebases onto the new `main`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

.github/workflows/agda.yml

@@ -30,7 +30,14 @@ jobs:
           git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR"
           echo "stdlib_dir=$STDLIB_DIR" >> "$GITHUB_OUTPUT"
 
-      - name: Register standard library for Agda
+      - name: Fetch absolute-zero library
+        id: absz
+        run: |
+          ABSZ_DIR="$RUNNER_TEMP/absolute-zero"
+          git clone --depth 1 https://github.com/hyperpolymath/absolute-zero.git "$ABSZ_DIR"
+          echo "absz_dir=$ABSZ_DIR" >> "$GITHUB_OUTPUT"
+
+      - name: Register libraries for Agda
         run: |
           mkdir -p "$HOME/.agda"
 
@@ -40,7 +47,13 @@ jobs:
           include: ${{ steps.stdlib.outputs.stdlib_dir }}/src
           EOF
 
-          printf '%s\n' "$STDLIB_LIB" > "$HOME/.agda/libraries"
+          ABSZ_LIB="$RUNNER_TEMP/absolute-zero.agda-lib"
+          cat > "$ABSZ_LIB" <<EOF
+          name: absolute-zero
+          include: ${{ steps.absz.outputs.absz_dir }}/proofs/agda
+          EOF
+
+          printf '%s\n%s\n' "$STDLIB_LIB" "$ABSZ_LIB" > "$HOME/.agda/libraries"
           printf '%s\n' "standard-library" > "$HOME/.agda/defaults"
 
       - name: Typecheck full suite

proofs/agda/characteristic/RecipeNonTriviality.agda

@@ -141,12 +141,12 @@ open import characteristic.RoleMode               using
   ( applyRole to applyRoleM
   ; applyMode to applyModeRM
   )
-open import characteristic.ModeGrade              using
-  ( ModeGEcho
-  ; applyMode
+open import characteristic.ModeGraded             using
+  ( applyMode
   )
   renaming
-  ( applyGrade to applyGradeM
+  ( MGEcho     to ModeGEcho
+  ; applyGrade to applyGradeM
   )
 
 ------------------------------------------------------------------------