proof(SafeGit): DISCHARGE forbiddenRefCharsAnchor via Refl (proven#90) (#102)

Yet another "OWED comment was overly cautious" discharge in the
[proven#90 Phase 3](#90)
campaign.

## What it does

\`\`\`idris
public export
forbiddenRefCharsAnchor :
forbiddenRefChars = [' ', '~', '^', ':', '?', '*', '[', '\\\\', '\\x7F']
forbiddenRefCharsAnchor = Refl
\`\`\`

## Why it works

\`forbiddenRefChars\` is \`public export\` in SafeGit.idr L24-26 with
this exact list literal as its body. The elaborator unfolds the LHS to
the RHS for \`Refl\`. No "Char-list reduction" is needed — both sides
are the same literal after the standard \`public export\` unfolding.

## Out of scope

The other 2 SafeGit OWEDs have real blockers:
- \`emptyRefNameInvalid\` — String-FFI (\`unpack\`, \`length\` on
\`""\`)
- \`refNameExtracts\` — auto-implicit elaboration

Refs #90

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

Author: hyperpolymath

src/Proven/SafeGit/Proofs.idr

@@ -12,11 +12,15 @@ import Proven.SafeGit
 
 %default total
 
-||| OWED: spec anchor — 9 ref characters are forbidden by
-||| git-check-ref-format. Blocked on Char-list reduction.
+||| DISCHARGED: spec anchor — the 9 ref characters forbidden by
+||| git-check-ref-format. `forbiddenRefChars` is `public export` with
+||| this exact list literal as its body (SafeGit.idr L24-26), so the
+||| elaborator unfolds the LHS to the RHS for `Refl`. No "Char-list
+||| reduction" is needed — both sides are the same list literal.
 public export
-0 forbiddenRefCharsAnchor :
+forbiddenRefCharsAnchor :
   forbiddenRefChars = [' ', '~', '^', ':', '?', '*', '[', '\\', '\x7F']
+forbiddenRefCharsAnchor = Refl
 
 --------------------------------------------------------------------------------
 -- OWED postulates