proof(SafeArchive): DISCHARGE max{CompressionRatio,TotalSize} via Refl (proven#90, #107) (#109)

Per [proven#107](#107)
"overly cautious OWED" pattern — Nat-literal-vs-literal variant.

\`\`\`idris
public export
maxCompressionRatioAnchor : maxCompressionRatio = 1000
maxCompressionRatioAnchor = Refl

public export
maxTotalSizeAnchor : maxTotalSize = 1073741824
maxTotalSizeAnchor = Refl
\`\`\`

Both `public export` (SafeArchive.idr L64-66 + L77-79). Idris2 compares
Nat literals via Integer representation without unary expansion — Refl
closes even for large literals like 1073741824.

OWED's "Nat literal opacity" only applies to REDUCING the named constant
to a SMALLER literal (e.g. for arithmetic). Here both sides are the SAME
literal so no reduction is needed.

Refs #90 #107

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

Author: hyperpolymath

src/Proven/SafeArchive/Proofs.idr

@@ -107,17 +107,24 @@ entryOKNotNullByteInPath = Refl
 -- Spec-anchor constants
 --------------------------------------------------------------------------------
 
-||| OWED: `maxCompressionRatio` is exactly 1000:1. Blocked on Nat-literal
-||| opacity (standards#128 "Nat literal opacity").
-public export
-0 maxCompressionRatioAnchor : maxCompressionRatio = 1000
-
-||| OWED: `maxTotalSize` is exactly 1 GiB (2^30 bytes = 1073741824).
-||| Idris2 0.8.0 cannot Refl-reduce large `Nat` literals (unary
-||| representation, standards#128 "Nat literal opacity"); needs a
-||| reflective tactic.
-public export
-0 maxTotalSizeAnchor : maxTotalSize = 1073741824
+||| DISCHARGED: `maxCompressionRatio = 1000`. `maxCompressionRatio` is
+||| `public export` with body `1000` (SafeArchive.idr L64-66). Both
+||| sides are the same `Nat` literal — Idris2 compares literals as
+||| their `Integer` representation without unary expansion, so `Refl`
+||| closes regardless of literal magnitude.
+public export
+maxCompressionRatioAnchor : maxCompressionRatio = 1000
+maxCompressionRatioAnchor = Refl
+
+||| DISCHARGED: `maxTotalSize = 1073741824` (1 GiB). Same literal-vs-
+||| literal pattern as `maxCompressionRatioAnchor` — `maxTotalSize` is
+||| `public export` with body `1073741824` (SafeArchive.idr L77-79).
+||| The "Nat literal opacity" blocker only applies to attempts to
+||| convert this value to a SMALLER literal — here both sides are the
+||| same literal so `Refl` closes.
+public export
+maxTotalSizeAnchor : maxTotalSize = 1073741824
+maxTotalSizeAnchor = Refl
 
 --------------------------------------------------------------------------------
 -- `isZipBomb` corner cases (compressedSize = 0)