proof(SafeHex): TENTATIVE DISCHARGE nonHexCharRejected via Refl on literal char (proven#90, #107) (#116)

MEDIUM-confidence experiment per
[proven#107](#107).

\`\`\`idris
public export
nonHexCharRejected : hexToNibble 'g' = Nothing
nonHexCharRejected = Refl
\`\`\`

The Char-FFI opacity blocker the OWED cited applies primarily to
ABSTRACT chars. For a LITERAL char like 'g', the `Ord Char` primitives
MAY reduce at the type level for Idris2 0.8.0 — this PR tests that
hypothesis.

If CI rejects the proof, close the PR and reinstate the OWED stub. The
session has been validating 16+ similar "the OWED was overly cautious"
hypotheses today; this one is genuinely uncertain.

Refs #90 #107

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

Author: hyperpolymath

src/Proven/SafeHex/Proofs.idr

@@ -10,7 +10,12 @@ import Proven.SafeHex
 
 %default total
 
-||| OWED: invalid character rejected (e.g. 'g' is not a hex digit).
-||| Blocked on Char FFI (`ord`, `>=`).
+||| TENTATIVE-DISCHARGE: invalid character rejected. The if-chain in
+||| `hexToNibble` (SafeHex.idr L66-71) tests `'g' >= '0' && 'g' <= '9'`,
+||| `'g' >= 'a' && 'g' <= 'f'`, `'g' >= 'A' && 'g' <= 'F'` — for a
+||| LITERAL Char like 'g' the `Ord Char` primitives may reduce at the
+||| type level (the FFI opacity the OWED cited applies primarily to
+||| ABSTRACT chars). If CI rejects this, fall back to the OWED stub.
 public export
-0 nonHexCharRejected : hexToNibble 'g' = Nothing
+nonHexCharRejected : hexToNibble 'g' = Nothing
+nonHexCharRejected = Refl