trustfile.yml 'Check believe_me audit trail' cannot fail — three independent defects

[hyperpolymath]

.github/workflows/trustfile.yml step "Check believe_me audit trail" (lines 102–111) cannot
produce a red result under any input.

BELIEVE_ME_COUNT=$(grep -r "believe_me" src/ --include="*.idr" 2>/dev/null | wc -l)
UNJUSTIFIED=$(grep -r "believe_me" src/ --include="*.idr" -B1 2>/dev/null | \
             grep -c "believe_me" 2>/dev/null || true)
echo "believe_me instances: $BELIEVE_ME_COUNT"
if [ "$BELIEVE_ME_COUNT" -gt 300 ]; then
  echo "WARNING: believe_me count ($BELIEVE_ME_COUNT) exceeds threshold (300)"
fi

Three independent defects, any one of which alone would void the check:

1. UNJUSTIFIED is computed and never read. It is the only variable that could express the
   step's stated purpose — verifying justification comments — and its value is discarded.
2. UNJUSTIFIED would not measure justification anyway. It re-greps its own -B1 context for
   the same pattern, so it counts the matches again rather than inspecting the preceding line.
3. The only branch echos and does not exit 1. Even at 10,000 instances the step is green.

And the threshold is unreachable in practice: the repo's own badge reports believe_me = 0, so the
-gt 300 branch has never been entered.

Contrast — e2e.yml does this correctly

.github/workflows/e2e.yml:65-77 excludes lines whose first non-whitespace is ||| or --
before failing, so it distinguishes a marker in code from a mention in a comment:

DANGEROUS=$(grep -rn 'believe_me\|assert_total\|really_believe_me' src/ 2>/dev/null \
            | grep -v test \
            | grep -vE '^[^:]+:[0-9]+:[[:space:]]*(\|\|\||--)' \
            || true)

That is the pattern to adopt.

Why it matters

A gate that cannot fail is as defective as one that cannot pass. It occupies a required-looking
slot in the workflow while carrying zero information, and its presence is read by everyone
downstream as evidence the property is enforced. This one has been green for its entire life
without ever having been able to be anything else.

Scope note, verified

Every marker grep in both workflows is src/-scoped (trustfile.yml additionally --include="*.idr").
No workflow greps docs/, so documentation may name these tokens freely — relevant when writing
about the trusted base.

Context: docs/IDRIS2-BUILD-WORK-PACKAGE.adoc §9.