ci(agda): drop N5Falsifier xfail gate — module now typechecks

The "Expected-failure gate (N5Falsifier is known-broken)" step was
asserting that proofs/agda/characteristic/N5Falsifier.agda fails the
typechecker (per the 2026-05-18 foundation audit). That hold no longer
holds: the module was resolved 2026-05-27 by pinning the implicit r /
grade at the four applyRole / applyGrade call sites, and is already
imported by characteristic/All.agda (line 33). The xfail step's own
self-disclosed instructions fired in the previous CI run, telling us to
"register it in characteristic/All.agda and remove this xfail gate".

In-source bookkeeping is already complete on this branch:
- N5Falsifier.agda banner rewritten as "HISTORICAL BROKEN BANNER
  (resolved 2026-05-27)" with the resolution narrative.
- characteristic/All.agda has the import (line 33).
- The previous CI run confirmed N5Falsifier typechecks (the xfail
  gate failed precisely because it succeeded) and that
  characteristic/All.agda typechecks WITH the import.

Net diff: -17 lines from .github/workflows/agda.yml. No Agda code
changed by this commit.

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

Author: hyperpolymath

.github/workflows/agda.yml

@@ -142,23 +142,6 @@ jobs:
       - name: Typecheck examples lane (Gate #3 canonical examples)
         run: agda -i proofs/agda proofs/agda/examples/All.agda
 
-      # Disclosed known-broken module (foundation audit 2026-05-18):
-      # characteristic/N5Falsifier.agda has unsolved metas and is NOT
-      # in any green closure. This gate ASSERTS it still fails, so the
-      # hole stays monitored: if it ever typechecks, this step fails
-      # loudly and tells us to register it + drop the xfail.
-      - name: Expected-failure gate (N5Falsifier is known-broken)
-        run: |
-          if agda -i proofs/agda proofs/agda/characteristic/N5Falsifier.agda \
-               > /tmp/n5.log 2>&1; then
-            echo "::error::N5Falsifier now typechecks — register it in"
-            echo "::error::characteristic/All.agda and remove this xfail gate."
-            exit 1
-          else
-            echo "N5Falsifier fails as expected (disclosed in its banner"
-            echo "and the proof-debt ledger). Hole monitored, not hidden."
-          fi
-
   cold-check:
     # Belt-and-braces: NO interface cache, --ignore-interfaces cold
     # build. A green here cannot be a stale-.agdai artefact (matters