fix(characteristic): correct ModeGrade -> ModeGraded import typo

RecipeNonTriviality.agda imports `characteristic.ModeGrade` (no `d`)
which doesn't exist; the actual file is `characteristic.ModeGraded`.
The required names line up with a small renaming:

  MGEcho     -> ModeGEcho
  applyMode  -> applyMode  (unchanged)
  applyGrade -> applyGradeM

The body uses (`modegrade-cell-action`, `-is-identity`,
`ModeGrade-no-non-identity-cell`) reduce definitionally as before,
because ModeGraded.agda's `applyMode {g = keep} linear≤linear e = e`
and `applyGrade {m = linear} keep≤keep e = e` are identity at exactly
the cell RecipeNonTriviality inspects.

The bug has been latent on main since the characteristic lane was
added in #27 (2026-04-29), masked by the absolute-zero CI break the
parent commit fixes.

Author: hyperpolymath

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
   )
 
 ------------------------------------------------------------------------