proof(SafePassword): DISCHARGE withMinLengthCorrect via nested constructor case-split (#143)

## Summary

Discharge \`Proven.SafePassword.Proofs.withMinLengthCorrect\` via double
constructor case-split.

The OWED comment correctly suggested case-split on \`b = MkPolicyBuilder
_\`. **Empirically verified** that DOUBLE case-split is needed — both
the outer \`MkPolicyBuilder\` AND the inner \`MkPolicy\` constructor
must be exposed for the projection \`({ minLength := n } p).minLength\`
to reduce.

## Discharge

\`\`\`idris
withMinLengthCorrect n (MkPolicyBuilder (MkPolicy _ _ _ _ _ _ _ _ _ _))
= Refl
\`\`\`

The 10 underscores correspond to PasswordPolicy's 10 fields
(\`minLength\` through \`forbiddenWords\`).

## Why double case-split

Tested at \`/tmp/charrefl/src/TestPolicyBuilder.idr\`:
- Single case-split on \`MkPolicyBuilder _\` alone: **fails** —
\`{minLength := n} p\` doesn't reduce through abstract \`p\`
- Double case-split exposing both constructors: **succeeds** — the
record-update + projection chain reduces fully

## Sister OWED not addressed

\`chainedBuildersCompose\` (Proofs.idr:430) is **NOT** discharged here.
It requires reducing \`Policy.policyBuilder\` (a top-level constant).
Same blocker family as SafeCSV's \`defaultDelimiterIsComma\` — top-level
\`public export\` constants don't reduce for downstream record
projection. Discharge waits for either an Idris2 0.8.0 fix or a
named-constant-bridge lemma technique.

## Verification

- \`idris2 --check src/Proven/SafePassword/Proofs.idr\` → Exit 0
- \`/tmp/charrefl/src/TestPolicyBuilder.idr\` prototype confirms double
case-split is necessary and sufficient
- Zero \`believe_me\` / \`postulate\` / \`idris_crash\`

Refs proven#90 (Phase 3 OWED triage), proven#107 (overly-cautious OWED
meta).

## Test plan

- [x] Local type-check clean
- [x] /tmp/charrefl test harness
- [ ] CI \`idris2 --check proven.ipkg\` green
- [ ] CI test suite green

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

Author: hyperpolymath

src/Proven/SafePassword/Proofs.idr

@@ -402,18 +402,19 @@ public export
 public export
 0 builderProducesPolicy : build Policy.policyBuilder = Policy.defaultPolicy
 
-||| OWED: `withMinLength n` followed by `build` yields a policy whose
-||| `minLength` field equals `n`. The implementation is
-||| `withMinLength n (MkPolicyBuilder p) = MkPolicyBuilder ({minLength
-||| := n} p)`, so the equation is true by record-update normalisation
-||| — but Idris2 0.8.0 does not reduce the record-update through the
-||| `MkPolicyBuilder` wrapper for an abstract starting builder
-||| `b : PolicyBuilder`. Discharge by case-splitting on
-||| `b = MkPolicyBuilder _` plus `Refl`, or by marking `build` and
-||| `withMinLength` `%inline`.
+||| DISCHARGED: `withMinLength n` followed by `build` yields a policy
+||| whose `minLength` field equals `n`. The OWED comment suggested the
+||| pattern: case-split on `b = MkPolicyBuilder _` to expose the
+||| constructor. Verified empirically that a DOUBLE case-split
+||| (`MkPolicyBuilder (MkPolicy _ _ _ _ _ _ _ _ _ _)`) is needed —
+||| the inner `PasswordPolicy` constructor also has to be exposed for
+||| the record-update projection `({ minLength := n } p).minLength`
+||| to reduce. Once both are exposed, the chain collapses to `Refl`.
+||| Test at `/tmp/charrefl/src/TestPolicyBuilder.idr`.
 public export
-0 withMinLengthCorrect : (n : Nat) -> (b : PolicyBuilder) ->
-                         minLength (build (withMinLength n b)) = n
+withMinLengthCorrect : (n : Nat) -> (b : PolicyBuilder) ->
+                       minLength (build (withMinLength n b)) = n
+withMinLengthCorrect n (MkPolicyBuilder (MkPolicy _ _ _ _ _ _ _ _ _ _)) = Refl
 
 ||| OWED: chained builder calls compose correctly — `withMinLength n
 ||| (withUppercase policyBuilder)` then `build`'s `minLength` is `n`.