check-trusted-base.sh: Lean `\bsorry\b` matches string literals and keyword tables

[hyperpolymath]

Summary

scripts/check-trusted-base.sh detects Lean escape hatches with a purely textual
grep -nE '\bsorry\b|^[[:space:]]*axiom[[:space:]]'. The \bsorry\b half matches any
occurrence of the word, including string literals, keyword tables and test inputs. Repos
whose subject matter is Lean (parsers, lexers, proof tooling) therefore carry permanent
phantom entries that can only be silenced by documenting non-existent debt.

Low severity — the check is doing its job overall, and this does not produce false
passes. Filing because the fix is small and the false positives dilute a document whose
value depends on being exactly true.

Evidence

From hyperpolymath/gnpl (19 detected, 16 real). The 3 phantoms:

Location	What it is
src/GqlDt/TypeInference.lean:179	| .admit => "sorry" — a string literal returned by a pretty-printer
src/GqlDt/Lexer.lean:230	("sorry", .kwSorry) — a keyword-table entry; the language being lexed has a sorry token
test/LexerTest.lean:147	runTest "sorry" (firstType "sorry" == some .kwSorry) — a test input

The existing is_comment_line filter already handles the fourth textual hit
(a commented-out := by sorry), so the comment case is covered — it is string literals
that leak through.

Suggested fix

Strip string literals before matching, as the comment filter already strips comments. A
minimal improvement that removes all three above:

• skip a match whose sorry occurrence lies inside a double-quoted string on that line;
• optionally exclude test/ from the Lean sweep, or require sorry to be preceded by
  by , :=, or line-start whitespace (proof positions).

For reference, hyperpolymath/gnpl scripts/check-lean-proofs.sh takes the
strip-then-match approach (awk removes /- -/ blocks, "strings" and -- comments before
the regex runs) and is canary-tested against seeded sorry/admit in real proof position.
Happy to upstream that awk pre-pass if useful.

Note

Not asking for a workaround on our side — gnpl has seeded docs/proof-debt.md and the
check passes. The 3 phantoms are recorded there in an explicit "detector false positives"
section so the count reconciles (19 = 16 real + 3).